2607.19283v1 / ENOTV/SourceComparison.lean

all files

import ENOTV.Localization

/-!
# Exact source localization and comparison with `Eₖ`

Assuming only the earlier FMT termwise sign theorem, the ENO interface
source is rewritten as a sum indexed by the unique owner of each highest
difference.  The local-amplitude lemma then gives the comparison with the
selection-free energy.
-/

noncomputable section

open scoped BigOperators

namespace ENOTV

local instance selectedIntervalDecidable (k : ℕ) (u : CSeq) (i j : ℤ) :
    Decidable (selectedInterval k (u : Seq) i j) :=
  Classical.propDecidable _

def rawSourceTerm (k : ℕ) (u : CSeq) (i j : ℤ) : ℝ :=
  if selectedInterval k (u : Seq) i j then
    cdiff u i *
      (gamma k (Int.toNat (i - j)) *
        cdiffIter (k - 1) (cdiff u) j)
  else 0

def positiveSourceTerm (k : ℕ) (u : CSeq) (i j : ℤ) : ℝ :=
  if selectedInterval k (u : Seq) i j then
    |cdiff u i| * |gamma k (Int.toNat (i - j))| *
      |cdiffIter (k - 1) (cdiff u) j|
  else 0

theorem rawSourceTerm_eq_positive
    (hFMT : FMTReconstructionTheorem) {k : ℕ} (hk : 2 ≤ k)
    (u : CSeq) (i j : ℤ) :
    rawSourceTerm k u i j = positiveSourceTerm k u i j := by
  by_cases hj : selectedInterval k (u : Seq) i j
  · rw [rawSourceTerm, positiveSourceTerm, if_pos hj, if_pos hj]
    have hnon := hFMT.2 k hk u i j hj
    rw [← abs_of_nonneg hnon, abs_mul, abs_mul]
    ring
  · simp [rawSourceTerm, positiveSourceTerm, hj]

theorem cSource_eq_tsum (k : ℕ) (u : CSeq) :
    cSource k u =
      ∑' i : ℤ, cdiff u i * reconstructedJump k (u : Seq) i := by
  have hs : Function.support
      (fun i : ℤ => cdiff u i * reconstructedJump k (u : Seq) i) ⊆
        (cdiff u).support := by
    intro i hi
    by_contra his
    have hz := Finsupp.notMem_support_iff.mp his
    exact hi (by simp [hz])
  rw [cSource, tsum_eq_sum' hs]
  rfl

theorem interface_eq_tsum_raw (k : ℕ) (u : CSeq) (i : ℤ) :
    cdiff u i * reconstructedJump k (u : Seq) i =
      ∑' j : ℤ, rawSourceTerm k u i j := by
  let l := enoLeft (u : Seq) i (k - 1)
  let r := enoLeft (u : Seq) (i + 1) (k - 1)
  have hs : Function.support (rawSourceTerm k u i) ⊆
      (Finset.Ico l r : Set ℤ) := by
    intro j hj
    by_contra hmem
    have hmem' : ¬(l ≤ j ∧ j < r) := by simpa using hmem
    have hnot : ¬ selectedInterval k (u : Seq) i j := by
      simp only [selectedInterval]
      change ¬(l ≤ j ∧ j < r)
      exact hmem'
    exact hj (by simp [rawSourceTerm, hnot])
  rw [tsum_eq_sum' hs, reconstructedJump]
  change cdiff u i *
      (∑ j ∈ Finset.Ico l r,
        gamma k (Int.toNat (i - j)) *
          diffIter (k - 1) (jumps (u : Seq)) j) =
    ∑ j ∈ Finset.Ico l r, rawSourceTerm k u i j
  rw [Finset.mul_sum]
  apply Finset.sum_congr rfl
  intro j hj
  simp only [Finset.mem_Ico] at hj
  have hsel : selectedInterval k (u : Seq) i j := by
    simpa [selectedInterval, l, r] using hj
  rw [rawSourceTerm, if_pos hsel]
  rw [cdiffIter_apply]
  rfl

theorem rawSourceTerm_summable (k : ℕ) (u : CSeq) :
    Summable (Function.uncurry (rawSourceTerm k u)) := by
  let w := cdiffIter (k - 1) (cdiff u)
  apply summable_of_ne_finset_zero
    (s := (cdiff u).support ×ˢ w.support)
  rintro ⟨i, j⟩ hij
  simp only [Finset.mem_product] at hij
  rcases not_and_or.mp hij with hi | hj
  · have hz := Finsupp.notMem_support_iff.mp hi
    unfold Function.uncurry rawSourceTerm
    split_ifs <;> simp [hz]
  · have hz := Finsupp.notMem_support_iff.mp hj
    unfold Function.uncurry rawSourceTerm
    split_ifs <;> simp [w, hz]

/-- Exact positive owner-indexed source furnished by the FMT sign theorem
and the endpoint partition. -/
def ownerSource (k : ℕ) (u : CSeq) : ℝ :=
  (cdiffIter (k - 1) (cdiff u)).sum fun j w =>
    |cdiff u (selectedOwner k (u : Seq) j)| *
      |gamma k (Int.toNat (selectedOwner k (u : Seq) j - j))| * |w|

theorem inner_positive_tsum_eq_owner {k : ℕ} (hk : 1 ≤ k)
    (u : CSeq) (j : ℤ) :
    (∑' i : ℤ, positiveSourceTerm k u i j) =
      |cdiff u (selectedOwner k (u : Seq) j)| *
        |gamma k (Int.toNat (selectedOwner k (u : Seq) j - j))| *
          |cdiffIter (k - 1) (cdiff u) j| := by
  rw [tsum_eq_single (selectedOwner k (u : Seq) j)]
  · rw [positiveSourceTerm,
      if_pos (selectedOwner_mem hk (u : Seq) j)]
  · intro i hne
    by_cases hi : selectedInterval k (u : Seq) i j
    · have heq := selectedInterval_owner_unique hk (u : Seq) i j hi
      exact (hne heq.symm).elim
    · simp [positiveSourceTerm, hi]

theorem ownerSource_eq_tsum (k : ℕ) (u : CSeq) :
    ownerSource k u =
      ∑' j : ℤ,
        |cdiff u (selectedOwner k (u : Seq) j)| *
          |gamma k (Int.toNat (selectedOwner k (u : Seq) j - j))| *
            |cdiffIter (k - 1) (cdiff u) j| := by
  let w := cdiffIter (k - 1) (cdiff u)
  have hs : Function.support
      (fun j : ℤ =>
        |cdiff u (selectedOwner k (u : Seq) j)| *
          |gamma k (Int.toNat (selectedOwner k (u : Seq) j - j))| *
            |w j|) ⊆ w.support := by
    intro j hj
    by_contra hjs
    have hz := Finsupp.notMem_support_iff.mp hjs
    exact hj (by simp [hz])
  rw [ownerSource, tsum_eq_sum' hs]
  rfl

theorem cSource_eq_ownerSource
    (hFMT : FMTReconstructionTheorem) {k : ℕ} (hk : 2 ≤ k)
    (u : CSeq) :
    cSource k u = ownerSource k u := by
  rw [cSource_eq_tsum]
  calc
    (∑' i : ℤ, cdiff u i * reconstructedJump k (u : Seq) i) =
        ∑' i : ℤ, ∑' j : ℤ, rawSourceTerm k u i j := by
          apply tsum_congr
          exact interface_eq_tsum_raw k u
    _ = ∑' i : ℤ, ∑' j : ℤ, positiveSourceTerm k u i j := by
          apply tsum_congr
          intro i
          apply tsum_congr
          exact rawSourceTerm_eq_positive hFMT hk u i
    _ = ∑' j : ℤ, ∑' i : ℤ, positiveSourceTerm k u i j := by
          have hs := rawSourceTerm_summable k u
          have heq : Function.uncurry (rawSourceTerm k u) =
              Function.uncurry (positiveSourceTerm k u) := by
            funext p
            exact rawSourceTerm_eq_positive hFMT hk u p.1 p.2
          rw [heq] at hs
          exact hs.tsum_comm.symm
    _ = ∑' j : ℤ,
        |cdiff u (selectedOwner k (u : Seq) j)| *
          |gamma k (Int.toNat (selectedOwner k (u : Seq) j - j))| *
            |cdiffIter (k - 1) (cdiff u) j| := by
          apply tsum_congr
          exact inner_positive_tsum_eq_owner (by omega) u
    _ = ownerSource k u := (ownerSource_eq_tsum k u).symm

/-! ## Uniform gamma weights -/

def gammaMin (k : ℕ) (hk : 1 ≤ k) : ℝ :=
  Finset.inf' (Finset.range k) (by simp [show k ≠ 0 by omega])
    fun d => |gamma k d|

theorem gamma_ne_zero {k d : ℕ} (hk : 1 ≤ k) (hd : d < k) :
    gamma k d ≠ 0 := by
  unfold gamma
  positivity

theorem gammaMin_pos {k : ℕ} (hk : 1 ≤ k) :
    0 < gammaMin k hk := by
  unfold gammaMin
  apply Finset.inf'_mem (Set.Ioi (0 : ℝ))
  · intro x hx y hy
    simp only [Set.mem_Ioi] at hx hy ⊢
    exact lt_min hx hy
  · intro d hd
    simp only [Finset.mem_range] at hd
    exact abs_pos.mpr (gamma_ne_zero hk hd)

theorem gammaMin_le {k d : ℕ} (hk : 1 ≤ k) (hd : d < k) :
    gammaMin k hk ≤ |gamma k d| := by
  unfold gammaMin
  exact Finset.inf'_le _ (by simpa using hd)

def gammaMax (k : ℕ) (hk : 1 ≤ k) : ℝ :=
  Finset.sup' (Finset.range k) (by simp [show k ≠ 0 by omega])
    fun d => |gamma k d|

theorem gamma_le_gammaMax {k d : ℕ} (hk : 1 ≤ k) (hd : d < k) :
    |gamma k d| ≤ gammaMax k hk := by
  unfold gammaMax
  exact Finset.le_sup' (f := fun d => |gamma k d|) (by simpa using hd)

theorem owner_abs_le_blockAmplitude {k : ℕ} (hk : 1 ≤ k)
    (u : CSeq) (j : ℤ) :
    |cdiff u (selectedOwner k (u : Seq) j)| ≤
      blockAmplitude k (cdiff u : Seq) j := by
  have hm := selectedOwner_mem hk (u : Seq) j
  have hd := mem_selectedInterval_bounds hk hm
  let d := Int.toNat (selectedOwner k (u : Seq) j - j)
  have hdlt : d < k := by
    rw [Int.toNat_lt hd.1]
    omega
  have hcast : j + (d : ℤ) = selectedOwner k (u : Seq) j := by
    rw [show (d : ℤ) = selectedOwner k (u : Seq) j - j by
      exact Int.toNat_of_nonneg hd.1]
    ring
  simpa [hcast] using
    abs_le_blockAmplitude hdlt (cdiff u : Seq) j

theorem ownerSource_le_energy {k : ℕ} (hk : 1 ≤ k) (u : CSeq) :
    ownerSource k u ≤ gammaMax k hk * cEnergy k (cdiff u) := by
  rw [ownerSource, cEnergy, Finsupp.mul_sum]
  apply Finsupp.sum_le_sum
  intro j hj
  let b := |cdiff u (selectedOwner k (u : Seq) j)|
  let g := |gamma k (Int.toNat (selectedOwner k (u : Seq) j - j))|
  let A := blockAmplitude k (cdiff u : Seq) j
  let w := |cdiffIter (k - 1) (cdiff u) j|
  have hm := selectedOwner_mem hk (u : Seq) j
  have hd := mem_selectedInterval_bounds hk hm
  have hdlt : Int.toNat (selectedOwner k (u : Seq) j - j) < k := by
    rw [Int.toNat_lt hd.1]
    omega
  have hb : b ≤ A := owner_abs_le_blockAmplitude hk u j
  have hg : g ≤ gammaMax k hk := gamma_le_gammaMax hk hdlt
  have hw : 0 ≤ w := abs_nonneg _
  have hg0 : 0 ≤ g := abs_nonneg _
  have hA0 : 0 ≤ A := blockAmplitude_nonneg k (cdiff u : Seq) j
  change b * g * w ≤ gammaMax k hk * (A * w)
  calc
    b * g * w ≤ A * g * w := by gcongr
    _ ≤ A * (gammaMax k hk) * w := by gcongr
    _ = gammaMax k hk * (A * w) := by ring

theorem source_le_energy
    (hFMT : FMTReconstructionTheorem) {k : ℕ} (hk : 2 ≤ k)
    (u : CSeq) :
    cSource k u ≤ gammaMax k (by omega) * cEnergy k (cdiff u) := by
  rw [cSource_eq_ownerSource hFMT hk]
  exact ownerSource_le_energy (by omega) u

theorem blockAmplitude_owner_le {k : ℕ} (hk : 1 ≤ k)
    (u : CSeq) (j : ℤ) :
    blockAmplitude k (cdiff u : Seq) j ≤
      localConstant k *
        |cdiff u (selectedOwner k (u : Seq) j)| := by
  have hm := selectedOwner_mem hk (u : Seq) j
  have hseq : (cdiff u : Seq) = jumps (u : Seq) := by
    funext q
    simp [jumps, diff]
  rw [hseq]
  exact local_amplitude_bound hk (u : Seq)
    (selectedOwner k (u : Seq) j) j hm

theorem energy_le_ownerSource {k : ℕ} (hk : 1 ≤ k) (u : CSeq) :
    cEnergy k (cdiff u) ≤
      (localConstant k * (gammaMin k hk)⁻¹) * ownerSource k u := by
  rw [ownerSource]
  rw [Finsupp.mul_sum]
  apply Finsupp.sum_le_sum
  intro j hj
  let A := blockAmplitude k (cdiff u : Seq) j
  let b := |cdiff u (selectedOwner k (u : Seq) j)|
  let g := |gamma k (Int.toNat (selectedOwner k (u : Seq) j - j))|
  let w := |cdiffIter (k - 1) (cdiff u) j|
  have hmem := selectedOwner_mem hk (u : Seq) j
  have hd := mem_selectedInterval_bounds hk (u := (u : Seq))
    (i := selectedOwner k (u : Seq) j) (j := j) hmem
  have hto : Int.toNat (selectedOwner k (u : Seq) j - j) < k := by
    rw [Int.toNat_lt hd.1]
    omega
  have hA : A ≤ localConstant k * b :=
    blockAmplitude_owner_le hk u j
  have hgpos : 0 < gammaMin k hk := gammaMin_pos hk
  have hg : gammaMin k hk ≤ g := gammaMin_le hk hto
  have hb : 0 ≤ b := abs_nonneg _
  have hw : 0 ≤ w := abs_nonneg _
  change A * w ≤
    (localConstant k * (gammaMin k hk)⁻¹) * (b * g * w)
  calc
    A * w ≤ (localConstant k * b) * w := by gcongr
    _ ≤ (localConstant k * (gammaMin k hk)⁻¹) * (b * g * w) := by
      have hone : 1 ≤ (gammaMin k hk)⁻¹ * g := by
        rw [← div_eq_inv_mul]
        exact (le_div_iff₀ hgpos).2 (by simpa using hg)
      have hc := localConstant_nonneg k
      calc
        (localConstant k * b) * w =
            (localConstant k * b * w) * 1 := by ring
        _ ≤ (localConstant k * b * w) *
              ((gammaMin k hk)⁻¹ * g) := by
            exact mul_le_mul_of_nonneg_left hone
              (mul_nonneg (mul_nonneg hc hb) hw)
        _ = (localConstant k * (gammaMin k hk)⁻¹) *
              (b * g * w) := by ring

theorem source_dominates_energy
    (hFMT : FMTReconstructionTheorem) {k : ℕ} (hk : 2 ≤ k) :
    ∃ K : ℝ, 0 < K ∧ ∀ u : CSeq,
      cEnergy k (cdiff u) ≤ K * cSource k u := by
  refine ⟨localConstant k * (gammaMin k (by omega))⁻¹, ?_, ?_⟩
  · have hc : 0 < localConstant k := by
      induction k, hk using Nat.le_induction with
      | base => norm_num [localConstant]
      | succ k hk ih =>
          rw [localConstant_succ (by omega)]
          exact mul_pos (by
            have : (2 : ℝ) ^ 1 ≤ 2 ^ k :=
              pow_le_pow_right₀ (by norm_num) (by omega)
            norm_num at this
            linarith) ih
    exact mul_pos hc (inv_pos.mpr (gammaMin_pos (by omega)))
  · intro u
    rw [cSource_eq_ownerSource hFMT hk]
    exact energy_le_ownerSource (by omega) u

end ENOTV