2607.19283v1 / ENOTV/Energy.lean

all files

import ENOTV.Compact

/-!
# Summation by parts and the even-difference energy

This is the algebraic half of the positive odd-order argument.  Everything
here is proved for genuinely compact lattice sequences, so all infinite sums
below are finite sums in disguise.
-/

noncomputable section

open scoped BigOperators

namespace ENOTV

/-- Bilinear finite-support pairing on the integer lattice. -/
def dot (f g : CSeq) : ℝ := ∑' i : ℤ, f i * g i

theorem summable_mul_left (f : CSeq) (g : Seq) :
    Summable fun i => f i * g i := by
  apply summable_of_ne_finset_zero (s := f.support)
  intro i hi
  rw [Finsupp.notMem_support_iff.mp hi, zero_mul]

theorem summable_mul_right (f : Seq) (g : CSeq) :
    Summable fun i => f i * g i := by
  simpa [mul_comm] using summable_mul_left g f

theorem tsum_add_int (F : Seq) (c : ℤ) :
    (∑' i : ℤ, F (i + c)) = ∑' i : ℤ, F i :=
  (Equiv.addRight c).tsum_eq F

theorem dot_comm (f g : CSeq) : dot f g = dot g f := by
  apply tsum_congr
  intro i
  exact mul_comm _ _

theorem dot_add_left (f g h : CSeq) : dot (f + g) h = dot f h + dot g h := by
  unfold dot
  simpa [add_mul] using
    (summable_mul_left f h).tsum_add (summable_mul_left g h)

theorem dot_sub_left (f g h : CSeq) : dot (f - g) h = dot f h - dot g h := by
  unfold dot
  simpa [sub_mul] using
    (summable_mul_left f h).tsum_sub (summable_mul_left g h)

theorem dot_add_right (f g h : CSeq) : dot f (g + h) = dot f g + dot f h := by
  rw [dot_comm, dot_add_left, dot_comm g, dot_comm h]

theorem dot_sub_right (f g h : CSeq) : dot f (g - h) = dot f g - dot f h := by
  rw [dot_comm, dot_sub_left, dot_comm g, dot_comm h]

theorem dot_neg_left (f g : CSeq) : dot (-f) g = -dot f g := by
  simpa [dot] using dot_sub_left (0 : CSeq) f g

theorem dot_neg_right (f g : CSeq) : dot f (-g) = -dot f g := by
  rw [dot_comm, dot_neg_left, dot_comm]

theorem dot_cshift_both (f g : CSeq) : dot (cshift f) (cshift g) = dot f g := by
  unfold dot
  simp only [cshift_apply]
  exact tsum_add_int (fun i => f i * g i) 1

/-- Compact summation by parts, with the shift dictated by a forward
difference. -/
theorem dot_cdiff_left (f g : CSeq) :
    dot (cdiff f) g = -dot (cshift f) (cdiff g) := by
  rw [show cdiff f = cshift f - f by rfl, dot_sub_left]
  rw [show cdiff g = cshift g - g by rfl, dot_sub_right, dot_cshift_both]
  ring

theorem cdiff_cshift (f : CSeq) : cdiff (cshift f) = cshift (cdiff f) := by
  ext i
  simp [cdiff_apply]

/-- Iterated lattice shift. -/
def cshiftIter : ℕ → CSeq → CSeq
  | 0, f => f
  | n + 1, f => cshift (cshiftIter n f)

@[simp] theorem cshiftIter_zero (f : CSeq) : cshiftIter 0 f = f := rfl

theorem cshiftIter_succ (n : ℕ) (f : CSeq) :
    cshiftIter (n + 1) f = cshift (cshiftIter n f) := rfl

@[simp] theorem cshiftIter_apply (n : ℕ) (f : CSeq) (i : ℤ) :
    cshiftIter n f i = f (i + n) := by
  induction n generalizing i with
  | zero => simp
  | succ n ih =>
      rw [cshiftIter_succ, cshift_apply, ih]
      congr 1
      push_cast
      omega

theorem cdiffIter_cshift (n : ℕ) (f : CSeq) :
    cdiffIter n (cshift f) = cshift (cdiffIter n f) := by
  induction n with
  | zero => rfl
  | succ n ih =>
      rw [cdiffIter_succ, cdiffIter_succ, ih, cdiff_cshift]

theorem cdiffIter_add (m n : ℕ) (f : CSeq) :
    cdiffIter m (cdiffIter n f) = cdiffIter (m + n) f := by
  induction m with
  | zero => simp
  | succ m ih =>
      change cdiff (cdiffIter m (cdiffIter n f)) = cdiffIter (m + 1 + n) f
      rw [ih, Nat.succ_add]
      rfl

/-- Repeated summation by parts. -/
theorem dot_diffIter_left (n : ℕ) (f g : CSeq) :
    dot (cdiffIter n f) g =
      (-1 : ℝ) ^ n * dot (cshiftIter n f) (cdiffIter n g) := by
  induction n generalizing f g with
  | zero => simp
  | succ n ih =>
      rw [cdiffIter_succ, dot_cdiff_left]
      rw [← cdiffIter_cshift]
      rw [ih (cshift f) (cdiff g)]
      have hd : cdiffIter n (cdiff g) = cdiffIter (n + 1) g := by
        change cdiffIter n (cdiffIter 1 g) = cdiffIter (n + 1) g
        exact cdiffIter_add n 1 g
      rw [hd]
      have hs : cshiftIter n (cshift f) = cshiftIter (n + 1) f := by
        ext i
        simp only [cshiftIter_apply, cshift_apply]
        congr 1
        push_cast
        ring
      rw [hs, pow_succ]
      ring

/-- The square identity of Lemma 3.3. -/
theorem even_difference_energy (s : ℕ) (a : CSeq) :
    dot (cdiffIter s a) (cdiffIter s a) =
      (-1 : ℝ) ^ s * dot (cshiftIter s a) (cdiffIter (2 * s) a) := by
  rw [dot_diffIter_left, cdiffIter_add]
  congr 3
  omega

/-- Selection-free localized source functional `Eₖ`. -/
def cEnergy (k : ℕ) (a : CSeq) : ℝ :=
  (cdiffIter (k - 1) a).sum fun j w =>
    blockAmplitude k (a : Seq) j * |w|

theorem blockAmplitude_nonneg (k : ℕ) (a : Seq) (j : ℤ) :
    0 ≤ blockAmplitude k a j := by
  by_cases hk : 0 < k
  · unfold blockAmplitude
    simp only [dif_pos hk]
    apply le_trans (abs_nonneg (a j))
    have hle := Finset.le_sup' (f := fun s : ℕ => |a (j + (s : ℤ))|)
      (show 0 ∈ Finset.range k by simpa)
    convert hle using 1 <;> simp
  · simp [blockAmplitude, hk]

theorem abs_le_blockAmplitude {k s : ℕ} (hs : s < k) (a : Seq) (j : ℤ) :
    |a (j + s)| ≤ blockAmplitude k a j := by
  have hk : 0 < k := Nat.zero_lt_of_lt hs
  unfold blockAmplitude
  simp only [dif_pos hk]
  apply Finset.le_sup' (f := fun q : ℕ => |a (j + (q : ℤ))|)
  simpa using hs

theorem cEnergy_nonneg (k : ℕ) (a : CSeq) : 0 ≤ cEnergy k a := by
  apply Finsupp.sum_nonneg
  intro j hj
  exact mul_nonneg (blockAmplitude_nonneg k (a : Seq) j) (abs_nonneg _)

theorem dot_eq_finsupp_sum (f g : CSeq) :
    dot f g = f.sum fun i x => x * g i := by
  have hs : Function.support (fun i => f i * g i) ⊆ (f.support : Set ℤ) := by
    intro i hi
    by_contra hif
    have hzero := Finsupp.notMem_support_iff.mp hif
    exact hi (by simp [hzero])
  rw [dot, tsum_eq_sum' hs]
  rfl

/-- Absolute form of the even-difference square estimate. -/
theorem square_energy_le_localized (s : ℕ) (a : CSeq) :
    dot (cdiffIter s a) (cdiffIter s a) ≤ cEnergy (2 * s + 1) a := by
  rw [even_difference_energy]
  have hsign : |(-1 : ℝ) ^ s| = 1 := by simp
  calc
    (-1 : ℝ) ^ s * dot (cshiftIter s a) (cdiffIter (2 * s) a)
        ≤ |(-1 : ℝ) ^ s * dot (cshiftIter s a) (cdiffIter (2 * s) a)| :=
      le_abs_self _
    _ = |dot (cshiftIter s a) (cdiffIter (2 * s) a)| := by
      rw [abs_mul, hsign, one_mul]
    _ ≤ (cdiffIter (2 * s) a).sum
          (fun j w => |cshiftIter s a j * w|) := by
      rw [dot_comm, dot_eq_finsupp_sum]
      simpa only [Finsupp.sum, abs_mul, mul_comm] using
        (Finset.abs_sum_le_sum_abs
          (fun j => (cdiffIter (2 * s) a) j * cshiftIter s a j)
          (cdiffIter (2 * s) a).support)
    _ ≤ (cdiffIter (2 * s) a).sum
          (fun j w => blockAmplitude (2 * s + 1) (a : Seq) j * |w|) := by
      apply Finsupp.sum_le_sum
      intro j hj
      rw [abs_mul]
      gcongr
      simpa [cshiftIter_apply, add_comm] using
        abs_le_blockAmplitude (show s < 2 * s + 1 by omega) (a : Seq) j
    _ = cEnergy (2 * s + 1) a := by
      congr 1

end ENOTV