2607.19283v1 / ENOTV/Compact.lean

all files

import ENOTV.Basic

/-!
# Compactly supported lattice sequences

`ℤ →₀ ℝ` is the convenient proof representation of the paper's compactly
supported sequences.  This file supplies forward differences, exact finite
sums, the sup amplitude, and coercivity in this representation.
-/

noncomputable section

open scoped BigOperators

namespace ENOTV

abbrev CSeq := ℤ →₀ ℝ

/-- Shift a compact sequence one site to the left:
`(cshift u) i = u (i+1)`. -/
def cshift : CSeq ≃+ CSeq :=
  Finsupp.domCongr (Equiv.addRight (-1 : ℤ))

@[simp] theorem cshift_apply (u : CSeq) (i : ℤ) :
    cshift u i = u (i + 1) := by
  simp [cshift]

/-- Forward difference of a compact sequence. -/
def cdiff (u : CSeq) : CSeq := cshift u - u

@[simp] theorem cdiff_apply (u : CSeq) (i : ℤ) :
    cdiff u i = u (i + 1) - u i := by
  simp [cdiff]

/-- Iterated compact forward difference. -/
def cdiffIter : ℕ → CSeq → CSeq
  | 0, u => u
  | n + 1, u => cdiff (cdiffIter n u)

@[simp] theorem cdiffIter_zero (u : CSeq) : cdiffIter 0 u = u := rfl

@[simp] theorem cdiffIter_apply_zero (u : CSeq) (i : ℤ) :
    cdiffIter 0 u i = u i := by simp

theorem cdiffIter_succ (n : ℕ) (u : CSeq) :
    cdiffIter (n + 1) u = cdiff (cdiffIter n u) := rfl

@[simp] theorem cdiffIter_apply (n : ℕ) (u : CSeq) (i : ℤ) :
    cdiffIter n u i = diffIter n (u : Seq) i := by
  induction n generalizing i with
  | zero => rfl
  | succ n ih =>
      rw [cdiffIter_succ]
      simp [diffIter, diff, ih]

/-- Supremum amplitude of a compact sequence.  The adjoined `0` also
handles the zero sequence without a separate nonempty-support branch. -/
def camplitude (u : CSeq) : ℝ :=
  Finset.max' (insert 0 (u.support.image fun i => |u i|))
    (Finset.insert_nonempty 0 _)

theorem camplitude_nonneg (u : CSeq) : 0 ≤ camplitude u := by
  apply Finset.le_max'
  simp

theorem abs_le_camplitude (u : CSeq) (i : ℤ) : |u i| ≤ camplitude u := by
  by_cases hi : u i = 0
  · simp [hi, camplitude_nonneg]
  · apply Finset.le_max'
    simp only [Finset.mem_insert, Finset.mem_image]
    right
    exact ⟨i, Finsupp.mem_support_iff.mpr hi, rfl⟩

@[simp] theorem camplitude_zero : camplitude (0 : CSeq) = 0 := by
  simp [camplitude]

/-- Exact finite jump moment. -/
def cJumpMoment (k : ℕ) (u : CSeq) : ℝ :=
  (cdiff u).sum fun _ ai => |ai| ^ (k + 1)

/-- Exact finite ENO source. -/
def cSource (k : ℕ) (u : CSeq) : ℝ :=
  (cdiff u).sum fun i ai => ai * reconstructedJump k (u : Seq) i

/-- Fixed-order coercivity, now quantified directly over the type of
compact sequences. -/
def CCoercive (k : ℕ) : Prop :=
  ∃ C : ℝ, 0 ≤ C ∧ ∀ u : CSeq,
    cJumpMoment k u ≤ C * camplitude u ^ (k - 1) * cSource k u

end ENOTV