2607.19283v1 / ENOTV/Basic.lean

all files

import Mathlib

/-!
# The ENO--TV parity problem: basic discrete definitions

This file starts a self-contained formalization of the uniform-grid objects
in Sections 1--2 of the paper.  Sequences are represented as functions on
`ℤ`; compact support is recorded separately by `FiniteSupport`.
-/

noncomputable section

open scoped BigOperators

namespace ENOTV

abbrev Seq := ℤ → ℝ

/-- Forward lattice difference, `(D u) i = u (i+1) - u i`. -/
def diff (u : Seq) : Seq := fun i => u (i + 1) - u i

/-- Iterated forward difference. -/
def diffIter : ℕ → Seq → Seq
  | 0, u => u
  | n + 1, u => diff (diffIter n u)

/-- The cell-average jump sequence. -/
def jumps (u : Seq) : Seq := diff u

/-- The paper's compact-support convention. -/
def FiniteSupport (u : Seq) : Prop := Set.Finite (Function.support u)

/-- The maximum absolute value of a length-`k` jump block. -/
def blockAmplitude (k : ℕ) (a : Seq) (j : ℤ) : ℝ :=
  if hk : 0 < k then
    Finset.sup' (Finset.range k) (by simp [Nat.ne_of_gt hk])
      fun s : ℕ => |a (j + (s : ℤ))|
  else 0

/-- ENO's recursively selected left endpoint.

`enoLeft u i ell` is the endpoint of the `(ell+1)`-cell stencil: level
`ell = 0` starts at cell `i`, and each successor performs the paper's
strict-left / weak-right comparison.
-/
def enoLeft (u : Seq) (i : ℤ) : ℕ → ℤ
  | 0 => i
  | ell + 1 =>
      let r := enoLeft u i ell
      let a := jumps u
      if |diffIter ell a (r - 1)| < |diffIter ell a r| then r - 1 else r

/-- The final-level half-open endpoint interval `Bᵢ⁽ᵏ⁾`. -/
def selectedInterval (k : ℕ) (u : Seq) (i j : ℤ) : Prop :=
  enoLeft u i (k - 1) ≤ j ∧ j < enoLeft u (i + 1) (k - 1)

/-- The coefficient `γ_{k,d}` in the localized FMT formula. -/
def gamma (k d : ℕ) : ℝ :=
  ((-1 : ℝ) ^ (k - 1 - d) * d.factorial * (k - 1 - d).factorial) /
    k.factorial

/-- The localized reconstructed interface jump of Proposition 2.2.

The sum is written as a finite interval sum.  It is empty when adjacent
selected endpoints agree.
-/
def reconstructedJump (k : ℕ) (u : Seq) (i : ℤ) : ℝ :=
  let l := enoLeft u i (k - 1)
  let r := enoLeft u (i + 1) (k - 1)
  ∑ j ∈ Finset.Ico l r,
    gamma k (Int.toNat (i - j)) * diffIter (k - 1) (jumps u) j

/-- The ENO source `Qₖ`, expressed by the exact localized FMT formula.
For compactly supported data the summand is finitely supported. -/
def source (k : ℕ) (u : Seq) : ℝ :=
  ∑' i : ℤ, jumps u i * reconstructedJump k u i

/-- The `(k+1)`-moment of the cell-average jumps. -/
def jumpMoment (k : ℕ) (u : Seq) : ℝ :=
  ∑' i : ℤ, |jumps u i| ^ (k + 1)

/-- Supremum amplitude, using the bounded-function norm after equipping a
finitely supported sequence with its canonical boundedness proof. -/
def amplitude (u : Seq) : ℝ := sSup (Set.range fun i => |u i|)

/-- The paper's fixed-order coercivity assertion. -/
def Coercive (k : ℕ) : Prop :=
  ∃ C : ℝ, 0 ≤ C ∧ ∀ u : Seq, FiniteSupport u →
    jumpMoment k u ≤ C * amplitude u ^ (k - 1) * source k u

/-! ## Elementary support and stencil facts -/

theorem finiteSupport_iff_eventuallyEq_zero {u : Seq} :
    FiniteSupport u ↔ u =ᶠ[Filter.cofinite] 0 := by
  change Set.Finite (Function.support u) ↔ ∀ᶠ i in Filter.cofinite, u i = 0
  rw [Filter.eventually_cofinite]
  rfl

theorem FiniteSupport.add {u v : Seq} (hu : FiniteSupport u) (hv : FiniteSupport v) :
    FiniteSupport (u + v) := by
  exact (hu.union hv).subset (Function.support_add u v)

theorem FiniteSupport.neg {u : Seq} (hu : FiniteSupport u) : FiniteSupport (-u) := by
  simpa [FiniteSupport, Function.support] using hu

theorem finiteSupport_comp_add (u : Seq) (h : FiniteSupport u) (c : ℤ) :
    FiniteSupport (fun i => u (i + c)) := by
  refine (h.image fun j => j - c).subset ?_
  intro i hi
  refine ⟨i + c, hi, ?_⟩
  simp

theorem FiniteSupport.diff {u : Seq} (hu : FiniteSupport u) :
    FiniteSupport (diff u) := by
  apply ((finiteSupport_comp_add u hu 1).add hu.neg).subset
  intro i hi
  change u (i + 1) - u i ≠ 0 at hi
  change u (i + 1) + -u i ≠ 0
  simpa [sub_eq_add_neg] using hi

theorem FiniteSupport.diffIter {u : Seq} (hu : FiniteSupport u) :
    ∀ n, FiniteSupport (diffIter n u)
  | 0 => hu
  | n + 1 => (hu.diffIter n).diff

@[simp] theorem enoLeft_zero (u : Seq) (i : ℤ) : enoLeft u i 0 = i := rfl

theorem enoLeft_bounds (u : Seq) (i : ℤ) (ell : ℕ) :
    i - ell ≤ enoLeft u i ell ∧ enoLeft u i ell ≤ i := by
  induction ell with
  | zero => simp
  | succ ell ih =>
      simp only [enoLeft]
      split_ifs <;> omega

theorem enoLeft_mono_step (u : Seq) (i : ℤ) (ell : ℕ) :
    enoLeft u i ell ≤ enoLeft u (i + 1) ell := by
  induction ell with
  | zero => simp [enoLeft]
  | succ ell ih =>
      by_cases hEq : enoLeft u i ell = enoLeft u (i + 1) ell
      · simp [enoLeft, hEq]
      · have hlt : enoLeft u i ell < enoLeft u (i + 1) ell :=
          lt_of_le_of_ne ih hEq
        simp only [enoLeft]
        split_ifs <;> omega

theorem mem_selectedInterval_bounds {k : ℕ} {u : Seq} {i j : ℤ}
    (hk : 1 ≤ k) (hj : selectedInterval k u i j) :
    0 ≤ i - j ∧ i - j ≤ k - 1 := by
  rcases hj with ⟨hl, hr⟩
  have hi := enoLeft_bounds u i (k - 1)
  have hi1 := enoLeft_bounds u (i + 1) (k - 1)
  constructor <;> omega

end ENOTV