2607.19283v1 / ENOTV/Counterexample.lean

all files

import ENOTV.Energy
import ENOTV.Euler

/-!
# Compact Euler-block data

This file constructs the compact two-block building block used in the
even-order obstruction.  We first work on `ℕ`, where prefix sums have clean
index arithmetic, and then embed the result in the integer lattice.
-/

noncomputable section

open scoped BigOperators

namespace ENOTV

abbrev NSeq := ℕ →₀ ℝ

/-- Extend a compact sequence on `ℕ` by zero to the negative integers. -/
def liftNat (f : NSeq) : CSeq :=
  Finsupp.onFinset
    (f.support.map ⟨Int.ofNat, Int.ofNat_injective⟩)
    (fun i => if 0 ≤ i then f i.toNat else 0)
    (by
      intro i hi
      split_ifs at hi with h
      · rw [Finset.mem_map]
        refine ⟨i.toNat, Finsupp.mem_support_iff.mpr hi, ?_⟩
        simpa using (Int.toNat_of_nonneg h).symm
      · exact (hi rfl).elim)

@[simp] theorem liftNat_apply_of_nonneg (f : NSeq) {i : ℤ} (hi : 0 ≤ i) :
    liftNat f i = f i.toNat := by
  simp [liftNat, hi]

@[simp] theorem liftNat_apply_nat (f : NSeq) (n : ℕ) :
    liftNat f n = f n := by simp [liftNat]

@[simp] theorem liftNat_apply_of_neg (f : NSeq) {i : ℤ} (hi : i < 0) :
    liftNat f i = 0 := by simp [liftNat, not_le_of_gt hi]

/-- Real-valued sample of the rational block polynomial. -/
def realBlock (d L t : ℕ) : ℝ := (blockPoly d L t : ℚ)

/-- Prefix sum of one positive Euler block. -/
def blockPrefix (d L r : ℕ) : ℝ :=
  ∑ t ∈ Finset.range r, realBlock d L t

@[simp] theorem blockPrefix_zero (d L : ℕ) : blockPrefix d L 0 = 0 := by
  simp [blockPrefix]

theorem blockPrefix_succ (d L r : ℕ) :
    blockPrefix d L (r + 1) = blockPrefix d L r + realBlock d L r := by
  simp [blockPrefix, Finset.sum_range_succ]

/-- Cell-average profile for a positive block followed by a negative copy.
It starts and ends at zero. -/
def pairDatumNat (d L : ℕ) : NSeq :=
  Finsupp.onFinset (Finset.range (4 * L + 1))
    (fun r =>
      if r ≤ 2 * L then blockPrefix d L r
      else if r ≤ 4 * L then blockPrefix d L (2 * L) - blockPrefix d L (r - 2 * L)
      else 0)
    (by
      intro r hr
      simp only [Finset.mem_range]
      by_contra h
      have h4 : 4 * L < r := by omega
      simp [show ¬r ≤ 2 * L by omega, show ¬r ≤ 4 * L by omega] at hr)

/-- The corresponding positive/negative pair of jump blocks. -/
def pairJumpNat (d L : ℕ) : NSeq :=
  Finsupp.onFinset (Finset.range (4 * L))
    (fun r =>
      if r < 2 * L then realBlock d L r
      else if r < 4 * L then -realBlock d L (r - 2 * L)
      else 0)
    (by
      intro r hr
      simp only [Finset.mem_range]
      by_contra h
      have h4 : 4 * L ≤ r := by omega
      simp [show ¬r < 2 * L by omega, show ¬r < 4 * L by omega] at hr)

@[simp] theorem pairDatumNat_apply (d L r : ℕ) :
    pairDatumNat d L r =
      if r ≤ 2 * L then blockPrefix d L r
      else if r ≤ 4 * L then blockPrefix d L (2 * L) - blockPrefix d L (r - 2 * L)
      else 0 := rfl

@[simp] theorem pairJumpNat_apply (d L r : ℕ) :
    pairJumpNat d L r =
      if r < 2 * L then realBlock d L r
      else if r < 4 * L then -realBlock d L (r - 2 * L)
      else 0 := rfl

/-- The prefix construction has exactly the desired jumps on `ℕ`. -/
theorem pairDatumNat_diff (d L r : ℕ) :
    pairDatumNat d L (r + 1) - pairDatumNat d L r = pairJumpNat d L r := by
  by_cases h₁ : r < 2 * L
  · have hr : r ≤ 2 * L := by omega
    have hrs : r + 1 ≤ 2 * L := by omega
    simp [pairDatumNat_apply, pairJumpNat_apply, h₁, hr, hrs, blockPrefix_succ]
  · by_cases hEq : r = 2 * L
    · subst r
      by_cases hL : L = 0
      · simp [hL, pairDatumNat_apply, pairJumpNat_apply]
      · have h2 : ¬2 * L < 2 * L := lt_irrefl _
        have h4 : 2 * L < 4 * L := by omega
        simp [pairDatumNat_apply, pairJumpNat_apply, h2, h4,
          blockPrefix_succ]
    · by_cases h₄ : r < 4 * L
      · have hr2 : 2 * L < r := by omega
        have hr2not : ¬r ≤ 2 * L := by omega
        have hrs2 : ¬r + 1 ≤ 2 * L := by omega
        have hr4 : r ≤ 4 * L := by omega
        have hrs4 : r + 1 ≤ 4 * L := by omega
        have hsub : r + 1 - 2 * L = (r - 2 * L) + 1 := by omega
        simp [pairDatumNat_apply, pairJumpNat_apply, h₁, h₄, hr2not,
          hrs2, hr4, hrs4, hsub, blockPrefix_succ]
      · have hr4 : 4 * L ≤ r := by omega
        have hr2 : ¬r ≤ 2 * L := by omega
        have hrs2 : ¬r + 1 ≤ 2 * L := by omega
        -- At and beyond the right endpoint both data values vanish.  The
        -- endpoint `r=4L` is already zero by construction.
        by_cases heq : r = 4 * L
        · subst r
          have hL : 0 < L := by omega
          have h42 : ¬4 * L ≤ 2 * L := by omega
          have h412 : ¬4 * L + 1 ≤ 2 * L := by omega
          have h414 : ¬4 * L + 1 ≤ 4 * L := by omega
          have hsub : 4 * L - 2 * L = 2 * L := by omega
          simp [pairDatumNat_apply, pairJumpNat_apply, h₁, h₄, h42, h412, h414, hsub]
        · have hr4' : ¬r ≤ 4 * L := by omega
          have hrs4 : ¬r + 1 ≤ 4 * L := by omega
          simp [pairDatumNat_apply, pairJumpNat_apply, h₁, h₄, hr2, hrs2,
            hr4', hrs4]

/-- Integer-lattice compact datum consisting of one positive and one
negative Euler block. -/
def pairDatum (d L : ℕ) : CSeq := liftNat (pairDatumNat d L)

def pairJumps (d L : ℕ) : CSeq := liftNat (pairJumpNat d L)

theorem cdiff_pairDatum (d L : ℕ) :
    cdiff (pairDatum d L) = pairJumps d L := by
  ext i
  by_cases hi : 0 ≤ i
  · obtain ⟨r, rfl⟩ := Int.eq_ofNat_of_zero_le hi
    have hcast : (r : ℤ) + 1 = ((r + 1 : ℕ) : ℤ) := by omega
    rw [cdiff_apply, hcast]
    simp only [pairDatum, pairJumps, liftNat_apply_nat]
    exact pairDatumNat_diff d L r
  · have hineg : i < 0 := lt_of_not_ge hi
    by_cases him1 : i = -1
    · subst i
      simp [pairDatum, pairJumps, cdiff_apply]
    · have hisucc : i + 1 < 0 := by omega
      simp [pairDatum, pairJumps, cdiff_apply, hineg, hisucc]

/-! ## Concatenating block pairs -/

/-- Translate a compact integer sequence to the right by `c`. -/
def translate (c : ℤ) : CSeq ≃+ CSeq :=
  Finsupp.domCongr (Equiv.addRight c)

@[simp] theorem translate_apply (c : ℤ) (f : CSeq) (i : ℤ) :
    translate c f i = f (i - c) := by
  simp [translate, sub_eq_add_neg]

theorem cdiff_translate (c : ℤ) (f : CSeq) :
    cdiff (translate c f) = translate c (cdiff f) := by
  ext i
  simp [cdiff_apply]
  congr 1
  omega

/-- `P` consecutive positive/negative pairs, i.e. `2P` alternating
Euler-polynomial blocks. -/
def multiDatum (d L P : ℕ) : CSeq :=
  ∑ p ∈ Finset.range P, translate (4 * L * p) (pairDatum d L)

def multiJumps (d L P : ℕ) : CSeq :=
  ∑ p ∈ Finset.range P, translate (4 * L * p) (pairJumps d L)

theorem cdiff_multiDatum (d L P : ℕ) :
    cdiff (multiDatum d L P) = multiJumps d L P := by
  ext i
  simp only [multiDatum, multiJumps, Finsupp.finsetSum_apply, cdiff_apply]
  rw [← Finset.sum_sub_distrib]
  apply Finset.sum_congr rfl
  intro p hp
  rw [← cdiff_apply, cdiff_translate, cdiff_pairDatum]

theorem pairJumps_support (d L : ℕ) :
    (pairJumps d L).support ⊆ Finset.Ico 0 (4 * L) := by
  intro i hi
  have hval := Finsupp.mem_support_iff.mp hi
  by_cases hi0 : 0 ≤ i
  · obtain ⟨r, rfl⟩ := Int.eq_ofNat_of_zero_le hi0
    simp only [pairJumps, liftNat_apply_nat, pairJumpNat_apply] at hval
    simp only [Finset.mem_Ico]
    constructor
    · omega
    · by_contra h
      simp [show ¬r < 2 * L by omega, show ¬r < 4 * L by omega] at hval
  · have hineg : i < 0 := lt_of_not_ge hi0
    simp [pairJumps, liftNat_apply_of_neg _ hineg] at hval

/-- Different translated pairs have disjoint jump supports. -/
theorem pairJumps_translate_disjoint {d L p q : ℕ} (hpq : p ≠ q) :
    Disjoint (translate (4 * L * p) (pairJumps d L)).support
      (translate (4 * L * q) (pairJumps d L)).support := by
  rw [Finset.disjoint_left]
  intro i hip hiq
  have hip' : i - (4 * L * p : ℕ) ∈ (pairJumps d L).support := by
    simpa [Finsupp.mem_support_iff] using hip
  have hiq' : i - (4 * L * q : ℕ) ∈ (pairJumps d L).support := by
    simpa [Finsupp.mem_support_iff] using hiq
  have bp := pairJumps_support d L hip'
  have bq := pairJumps_support d L hiq'
  simp only [Finset.mem_Ico] at bp bq
  by_cases hpq' : p < q
  · have hL : 0 < L := by
      by_contra h
      have : L = 0 := by omega
      subst L
      norm_num at bp
      omega
    have hpq1 : p + 1 ≤ q := by omega
    have hsepNat : 4 * L * p + 4 * L ≤ 4 * L * q := by
      calc
        4 * L * p + 4 * L = 4 * L * (p + 1) := by ring
        _ ≤ 4 * L * q := Nat.mul_le_mul_left (4 * L) hpq1
    have hsep :
        4 * (L : ℤ) * (p : ℤ) + 4 * (L : ℤ) ≤
          4 * (L : ℤ) * (q : ℤ) := by
      exact_mod_cast hsepNat
    push_cast at bp bq
    omega
  · have hqp : q < p := by omega
    have hL : 0 < L := by
      by_contra h
      have : L = 0 := by omega
      subst L
      norm_num at bq
      omega
    have hqp1 : q + 1 ≤ p := by omega
    have hsepNat : 4 * L * q + 4 * L ≤ 4 * L * p := by
      calc
        4 * L * q + 4 * L = 4 * L * (q + 1) := by ring
        _ ≤ 4 * L * p := Nat.mul_le_mul_left (4 * L) hqp1
    have hsep :
        4 * (L : ℤ) * (q : ℤ) + 4 * (L : ℤ) ≤
          4 * (L : ℤ) * (p : ℤ) := by
      exact_mod_cast hsepNat
    push_cast at bp bq
    omega

theorem pairDatum_support (d L : ℕ) :
    (pairDatum d L).support ⊆ Finset.Ioo 0 (4 * L) := by
  intro i hi
  have hval := Finsupp.mem_support_iff.mp hi
  by_cases hi0 : 0 ≤ i
  · obtain ⟨r, rfl⟩ := Int.eq_ofNat_of_zero_le hi0
    simp only [pairDatum, liftNat_apply_nat, pairDatumNat_apply] at hval
    simp only [Finset.mem_Ioo]
    constructor
    · by_contra hr0
      have : r = 0 := by omega
      subst r
      simp at hval
    · by_contra hr4
      have hge : 4 * L ≤ r := by omega
      by_cases heq : r = 4 * L
      · subst r
        by_cases hL : L = 0
        · simp [hL] at hval
        · have h42 : ¬4 * L ≤ 2 * L := by omega
          have hsub : 4 * L - 2 * L = 2 * L := by omega
          simp [h42, hsub] at hval
      · have h2 : ¬r ≤ 2 * L := by omega
        have h4 : ¬r ≤ 4 * L := by omega
        simp [h2, h4] at hval
  · have hineg : i < 0 := lt_of_not_ge hi0
    simp [pairDatum, liftNat_apply_of_neg _ hineg] at hval

theorem pairDatum_translate_disjoint {d L p q : ℕ} (hpq : p ≠ q) :
    Disjoint (translate (4 * L * p) (pairDatum d L)).support
      (translate (4 * L * q) (pairDatum d L)).support := by
  rw [Finset.disjoint_left]
  intro i hip hiq
  have hip' : i - (4 * L * p : ℕ) ∈ (pairDatum d L).support := by
    simpa [Finsupp.mem_support_iff] using hip
  have hiq' : i - (4 * L * q : ℕ) ∈ (pairDatum d L).support := by
    simpa [Finsupp.mem_support_iff] using hiq
  have bp := pairDatum_support d L hip'
  have bq := pairDatum_support d L hiq'
  simp only [Finset.mem_Ioo] at bp bq
  by_cases hpq' : p < q
  · have hL : 0 < L := by
      by_contra h
      have : L = 0 := by omega
      subst L
      norm_num at bp
      omega
    have hpq1 : p + 1 ≤ q := by omega
    have hsepNat : 4 * L * p + 4 * L ≤ 4 * L * q := by
      calc
        4 * L * p + 4 * L = 4 * L * (p + 1) := by ring
        _ ≤ 4 * L * q := Nat.mul_le_mul_left (4 * L) hpq1
    have hsep :
        4 * (L : ℤ) * (p : ℤ) + 4 * (L : ℤ) ≤
          4 * (L : ℤ) * (q : ℤ) := by
      exact_mod_cast hsepNat
    push_cast at bp bq
    omega
  · have hqp : q < p := by omega
    have hL : 0 < L := by
      by_contra h
      have : L = 0 := by omega
      subst L
      norm_num at bq
      omega
    have hqp1 : q + 1 ≤ p := by omega
    have hsepNat : 4 * L * q + 4 * L ≤ 4 * L * p := by
      calc
        4 * L * q + 4 * L = 4 * L * (q + 1) := by ring
        _ ≤ 4 * L * p := Nat.mul_le_mul_left (4 * L) hqp1
    have hsep :
        4 * (L : ℤ) * (q : ℤ) + 4 * (L : ℤ) ≤
          4 * (L : ℤ) * (p : ℤ) := by
      exact_mod_cast hsepNat
    push_cast at bp bq
    omega

theorem multiDatum_pointwise_le_pair (d L P : ℕ) (i : ℤ) :
    |multiDatum d L P i| ≤ camplitude (pairDatum d L) := by
  classical
  simp only [multiDatum, Finsupp.finsetSum_apply]
  by_cases hex : ∃ p ∈ Finset.range P,
      translate (4 * L * p) (pairDatum d L) i ≠ 0
  · obtain ⟨p, hp, hpi⟩ := hex
    rw [Finset.sum_eq_single p _ (fun hnot => (hnot hp).elim)]
    · simpa using abs_le_camplitude (pairDatum d L) (i - (4 * L * p : ℕ))
    · intro q hq hqp
      by_contra hqi
      have hpS : i ∈ (translate (4 * L * p) (pairDatum d L)).support :=
        Finsupp.mem_support_iff.mpr hpi
      have hqS : i ∈ (translate (4 * L * q) (pairDatum d L)).support :=
        Finsupp.mem_support_iff.mpr hqi
      exact Finset.disjoint_left.mp
        (pairDatum_translate_disjoint (d := d) (L := L) (p := p) (q := q) hqp.symm)
        hpS hqS
  · push_neg at hex
    have hz : ∑ p ∈ Finset.range P,
        translate (4 * L * p) (pairDatum d L) i = 0 :=
      Finset.sum_eq_zero hex
    rw [hz]
    simp [camplitude_nonneg]

/-! ## Additivity of moments across disjoint pairs -/

def powerSum (p : ℕ) (f : CSeq) : ℝ :=
  f.sum fun _ x => |x| ^ (p + 1)

theorem powerSum_eq_tsum (p : ℕ) (f : CSeq) :
    powerSum p f = ∑' i : ℤ, |f i| ^ (p + 1) := by
  have hs : Function.support (fun i => |f i| ^ (p + 1)) ⊆ (f.support : Set ℤ) := by
    intro i hi
    by_contra hif
    have hz := Finsupp.notMem_support_iff.mp hif
    exact hi (by simp [hz])
  rw [powerSum, tsum_eq_sum' hs]
  rfl

theorem summable_abs_pow (p : ℕ) (f : CSeq) :
    Summable fun i : ℤ => |f i| ^ (p + 1) := by
  apply summable_of_ne_finset_zero (s := f.support)
  intro i hi
  simp [Finsupp.notMem_support_iff.mp hi]

theorem powerSum_add_of_disjoint (p : ℕ) {f g : CSeq}
    (hfg : Disjoint f.support g.support) :
    powerSum p (f + g) = powerSum p f + powerSum p g := by
  rw [powerSum_eq_tsum, powerSum_eq_tsum, powerSum_eq_tsum,
    ← (summable_abs_pow p f).tsum_add (summable_abs_pow p g)]
  apply tsum_congr
  intro i
  by_cases hfi : f i = 0
  · simp [hfi]
  · have hgi : g i = 0 := by
      by_contra hg
      exact Finset.disjoint_left.mp hfg
        (Finsupp.mem_support_iff.mpr hfi) (Finsupp.mem_support_iff.mpr hg)
    simp [hgi]

theorem powerSum_translate (p : ℕ) (c : ℤ) (f : CSeq) :
    powerSum p (translate c f) = powerSum p f := by
  rw [powerSum_eq_tsum, powerSum_eq_tsum]
  simpa [sub_eq_add_neg] using
    (tsum_add_int (fun i : ℤ => |f i| ^ (p + 1)) (-c))

theorem multiJumps_succ (d L P : ℕ) :
    multiJumps d L (P + 1) =
      multiJumps d L P + translate (4 * L * P) (pairJumps d L) := by
  simp [multiJumps, Finset.sum_range_succ]

theorem multiJumps_new_disjoint (d L P : ℕ) :
    Disjoint (multiJumps d L P).support
      (translate (4 * L * P) (pairJumps d L)).support := by
  rw [Finset.disjoint_left]
  intro i hi hnew
  have hi' := Finsupp.support_finsetSum hi
  simp only [Finset.mem_biUnion, Finset.mem_range] at hi'
  obtain ⟨q, hqP, hqi⟩ := hi'
  exact Finset.disjoint_left.mp
    (pairJumps_translate_disjoint (d := d) (L := L) (p := q) (q := P)
      (by omega))
    hqi hnew

theorem powerSum_multiJumps (p d L P : ℕ) :
    powerSum p (multiJumps d L P) = P * powerSum p (pairJumps d L) := by
  induction P with
  | zero => simp [multiJumps, powerSum]
  | succ P ih =>
      rw [show P + 1 = Nat.succ P by rfl, multiJumps_succ,
        powerSum_add_of_disjoint p (multiJumps_new_disjoint d L P),
        powerSum_translate, ih]
      push_cast
      ring

end ENOTV