2607.19283v1 / Core.lean

all files

import Mathlib

/-!
# The hidden-square identity behind odd-order ENO--TV coercivity

This file formalizes Lemma 3.3 of Li--Wu, arXiv:2607.19283v1, for real-valued
bi-infinite sequences with finite support.
-/

open scoped BigOperators
open Function

namespace ENOTVCore

noncomputable section

/-- Unit forward shift on integer-indexed sequences. -/
def shift (f : ℤ → ℝ) : ℤ → ℝ := fun i => f (i + 1)

/-- Unit forward difference. -/
def D (f : ℤ → ℝ) : ℤ → ℝ := fwdDiff 1 f

/-- The `n`-fold forward difference. -/
def Diter (n : ℕ) (f : ℤ → ℝ) : ℤ → ℝ := D^[n] f

/-- The finite pairing of two sequences, at least one of which is finitely supported. -/
def pairing (f g : ℤ → ℝ) : ℝ := ∑ᶠ i, f i * g i

@[simp] theorem shift_apply (f : ℤ → ℝ) (i : ℤ) : shift f i = f (i + 1) := rfl

@[simp] theorem D_apply (f : ℤ → ℝ) (i : ℤ) : D f i = f (i + 1) - f i := rfl

theorem hasFiniteSupport_shift {f : ℤ → ℝ} (hf : f.HasFiniteSupport) :
    (shift f).HasFiniteSupport := by
  change (fun i : ℤ => f (i + 1)).HasFiniteSupport
  simpa [shift, Function.comp_def] using
    hf.comp_of_injective (Equiv.addRight (1 : ℤ)).injective

theorem hasFiniteSupport_D {f : ℤ → ℝ} (hf : f.HasFiniteSupport) :
    (D f).HasFiniteSupport := by
  change (shift f - f).HasFiniteSupport
  exact (hasFiniteSupport_shift hf).sub hf

theorem hasFiniteSupport_Diter {f : ℤ → ℝ} (hf : f.HasFiniteSupport) (n : ℕ) :
    (Diter n f).HasFiniteSupport := by
  induction n with
  | zero => simpa [Diter]
  | succ n ih =>
      simpa [Diter, Function.iterate_succ_apply'] using hasFiniteSupport_D ih

/-- Equation (3.20): summation by parts for finitely supported sequences. -/
theorem summation_by_parts (f g : ℤ → ℝ) (hf : f.HasFiniteSupport)
    (hg : g.HasFiniteSupport) :
    pairing (D f) g = -pairing (shift f) (D g) := by
  have hfshift := hasFiniteSupport_shift hf
  have hgshift := hasFiniteSupport_shift hg
  have hfg : (fun i => f i * g i).HasFiniteSupport := hf.mul_left g
  have hfs_g : (fun i => f (i + 1) * g i).HasFiniteSupport := by
    change (shift f * g).HasFiniteSupport
    exact hfshift.mul_left g
  have hfs_gs : (fun i => f (i + 1) * g (i + 1)).HasFiniteSupport := by
    change (shift f * shift g).HasFiniteSupport
    exact hfshift.mul_left (shift g)
  have hreindex : (∑ᶠ i : ℤ, f (i + 1) * g (i + 1)) = ∑ᶠ i : ℤ, f i * g i := by
    simpa [Function.comp_def] using
      (finsum_comp_equiv (Equiv.addRight (1 : ℤ)) (f := fun i : ℤ => f i * g i))
  rw [pairing, pairing]
  change (∑ᶠ i : ℤ, (f (i + 1) - f i) * g i) =
    -(∑ᶠ i : ℤ, f (i + 1) * (g (i + 1) - g i))
  simp_rw [sub_mul, mul_sub]
  rw [finsum_sub_distrib hfs_g hfg, finsum_sub_distrib hfs_gs hfs_g, hreindex]
  ring

theorem Diter_shift (f : ℤ → ℝ) (n : ℕ) : Diter n (shift f) = shift (Diter n f) := by
  change (fwdDiff (1 : ℤ))^[n] (fun i => f (i + 1)) =
    fun i => (fwdDiff (1 : ℤ))^[n] f (i + 1)
  funext i
  exact fwdDiff_iter_comp_add (1 : ℤ) f 1 n i

theorem Diter_succ_left (f : ℤ → ℝ) (n : ℕ) : Diter (n + 1) f = D (Diter n f) := by
  simp [Diter, Function.iterate_succ_apply']

theorem Diter_succ_right (f : ℤ → ℝ) (n : ℕ) : Diter (n + 1) f = Diter n (D f) := by
  simp [Diter, Function.iterate_succ_apply]

/-- The iterated summation-by-parts formula used in the proof of Lemma 3.3. -/
theorem iterated_summation_by_parts (a h : ℤ → ℝ) (ha : a.HasFiniteSupport)
    (hh : h.HasFiniteSupport) (s : ℕ) :
    pairing (Diter s a) h =
      (-1 : ℝ) ^ s * pairing (fun i => a (i + (s : ℤ))) (Diter s h) := by
  induction s generalizing a h with
  | zero => simp [Diter]
  | succ s ih =>
      rw [show Diter (s + 1) a = D (Diter s a) by simpa using Diter_succ_left a s]
      rw [summation_by_parts (Diter s a) h (hasFiniteSupport_Diter ha s) hh]
      rw [← Diter_shift]
      rw [ih (shift a) (D h) (hasFiniteSupport_shift ha) (hasFiniteSupport_D hh)]
      simp only [shift_apply, Nat.cast_add, Nat.cast_one]
      rw [show Diter s (D h) = Diter (s + 1) h by
        symm
        simpa using Diter_succ_right h s]
      simp only [pow_succ]
      have hfun : (fun i : ℤ => a (i + (s : ℤ) + 1)) =
          fun i : ℤ => a (i + ((s : ℤ) + 1)) := by
        funext i
        congr 1
        omega
      rw [hfun]
      ring

theorem Diter_add (f : ℤ → ℝ) (m n : ℕ) :
    Diter (m + n) f = Diter m (Diter n f) := by
  simp [Diter, Function.iterate_add_apply]

/--
Lemma 3.3, equation (3.18): an even-order forward difference hides a
nonnegative square energy after `s` summation-by-parts steps.
-/
theorem even_difference_energy_identity (a : ℤ → ℝ) (ha : a.HasFiniteSupport) (s : ℕ) :
    (∑ᶠ i : ℤ, |Diter s a i| ^ 2) =
      (-1 : ℝ) ^ s * (∑ᶠ i : ℤ, a (i + (s : ℤ)) * Diter (2 * s) a i) := by
  simp_rw [sq_abs]
  have h := iterated_summation_by_parts a (Diter s a) ha (hasFiniteSupport_Diter ha s) s
  rw [← Diter_add a s s] at h
  simpa only [pairing, pow_two, two_mul] using h

/-- The paper's `A_i^(2s+1)`, centered at the first index of its window. -/
def localAmplitude (s : ℕ) (a : ℤ → ℝ) (i : ℤ) : ℝ :=
  (Finset.range (2 * s + 1)).sup' (by simp) fun q => |a (i + (q : ℤ))|

theorem center_abs_le_localAmplitude (s : ℕ) (a : ℤ → ℝ) (i : ℤ) :
    |a (i + (s : ℤ))| ≤ localAmplitude s a i := by
  unfold localAmplitude
  have hs : s ∈ Finset.range (2 * s + 1) := by
    simp only [Finset.mem_range]
    omega
  exact Finset.le_sup' (fun q : ℕ => |a (i + (q : ℤ))|) hs

/-- The localized functional on the right of equation (3.19). -/
def localizedEnergy (s : ℕ) (a : ℤ → ℝ) : ℝ :=
  ∑ᶠ i : ℤ, localAmplitude s a i * |Diter (2 * s) a i|

/--
Lemma 3.3, equation (3.19): the hidden square energy is controlled by the
selection-independent localized ENO source functional.
-/
theorem even_difference_energy_le_localized (a : ℤ → ℝ) (ha : a.HasFiniteSupport) (s : ℕ) :
    (∑ᶠ i : ℤ, |Diter s a i| ^ 2) ≤ localizedEnergy s a := by
  let b : ℤ → ℝ := Diter (2 * s) a
  have hb : b.HasFiniteSupport := hasFiniteSupport_Diter ha (2 * s)
  let S : Finset ℤ := hb.toFinset
  have hpair : pairing (fun i => a (i + (s : ℤ))) b =
      ∑ i ∈ S, a (i + (s : ℤ)) * b i := by
    unfold pairing
    apply finsum_eq_finsetSum_of_support_subset
    intro i hi
    apply hb.mem_toFinset.mpr
    rw [Function.mem_support] at hi ⊢
    intro hbi
    exact hi (by simp [hbi])
  have henergy : localizedEnergy s a =
      ∑ i ∈ S, localAmplitude s a i * |b i| := by
    unfold localizedEnergy
    apply finsum_eq_finsetSum_of_support_subset
    intro i hi
    apply hb.mem_toFinset.mpr
    rw [Function.mem_support] at hi ⊢
    intro hbi
    exact hi (by simp [b, hbi])
  rw [even_difference_energy_identity a ha s]
  change (-1 : ℝ) ^ s * pairing (fun i => a (i + (s : ℤ))) b ≤ localizedEnergy s a
  rw [hpair, henergy]
  calc
    (-1 : ℝ) ^ s * (∑ i ∈ S, a (i + (s : ℤ)) * b i)
        ≤ |(-1 : ℝ) ^ s * (∑ i ∈ S, a (i + (s : ℤ)) * b i)| := le_abs_self _
    _ = |∑ i ∈ S, a (i + (s : ℤ)) * b i| := by
      rw [abs_mul, abs_pow, abs_neg, abs_one, one_pow, one_mul]
    _ ≤ ∑ i ∈ S, |a (i + (s : ℤ)) * b i| := Finset.abs_sum_le_sum_abs _ _
    _ ≤ ∑ i ∈ S, localAmplitude s a i * |b i| := by
      apply Finset.sum_le_sum
      intro i hi
      rw [abs_mul]
      exact mul_le_mul_of_nonneg_right (center_abs_le_localAmplitude s a i) (abs_nonneg _)

#print axioms summation_by_parts
#print axioms iterated_summation_by_parts
#print axioms even_difference_energy_identity
#print axioms even_difference_energy_le_localized

end

end ENOTVCore