2607.19283v1 / Repro.lean

all files

import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Data.Finsupp.Order
import Mathlib.LinearAlgebra.Lagrange

/-!
# A faithful statement of the ENO--TV parity theorem

This file formalizes the uniform-grid definitions in Li--Wu, arXiv:2607.19283v1,
Sections 1--2.  Interface coordinates have been translated by `-1/2`: the paper's
point `x_{n+1/2}` is the real number `n` below.  Translation does not change the
derivative of the reconstruction polynomial.
-/

noncomputable section

open scoped BigOperators
open Polynomial

namespace ENOTV

/-- Compactly supported cell averages on the integer-indexed unit grid. -/
abbrev CellData := ℤ →₀ ℝ

/-- The forward difference of a bi-infinite sequence. -/
def forwardDiff : ℕ → (ℤ → ℝ) → (ℤ → ℝ)
  | 0, a => a
  | n + 1, a => fun i => forwardDiff n a (i + 1) - forwardDiff n a i

/-- The cell-average jump `a_i = ubar_{i+1} - ubar_i`. -/
def jump (u : CellData) (i : ℤ) : ℝ := u (i + 1) - u i

/--
The left endpoint after `steps` ENO extensions.  Thus `steps = 0` is the
paper's level `ℓ = 1`, and an order-`k` stencil uses `steps = k - 1`.

The common factorial in the two divided differences is omitted, exactly as in
equation (2.3).  The strict-left/non-strict-right tie convention is (2.6).
-/
def enoLeftEndpoint (u : CellData) (i : ℤ) : ℕ → ℤ
  | 0 => i
  | steps + 1 =>
      let r := enoLeftEndpoint u i steps
      if |forwardDiff steps (jump u) (r - 1)| < |forwardDiff steps (jump u) r| then
        r - 1
      else
        r

/-- The final left endpoint of the standard order-`k` ENO stencil. -/
def finalLeftEndpoint (u : CellData) (k : ℕ) (i : ℤ) : ℤ :=
  enoLeftEndpoint u i (k - 1)

/--
The cumulative interface datum `V_{n+1/2} = sum_{j ≤ n} ubar_j` from (2.9).
The sum is finite because `u` is a `Finsupp`.
-/
def cumulativeInterface (u : CellData) (n : ℤ) : ℝ :=
  ∑ j ∈ u.support.filter (fun j => j ≤ n), u j

/-- Boundary node number `q` for the `k+1` nodes attached to a left endpoint `r`. -/
def boundaryNode (r : ℤ) {k : ℕ} (q : Fin (k + 1)) : ℝ :=
  (r - 1 + (q : ℕ) : ℤ)

/-- The cumulative value prescribed at `boundaryNode r q`. -/
def boundaryValue (u : CellData) (r : ℤ) {k : ℕ} (q : Fin (k + 1)) : ℝ :=
  cumulativeInterface u (r - 1 + (q : ℕ))

/--
The degree-at-most-`k` cumulative-interface interpolant through the `k+1`
boundary points of the selected stencil, as in (2.10).
-/
def primitiveReconstruction (u : CellData) (k : ℕ) (i : ℤ) : ℝ[X] :=
  let r := finalLeftEndpoint u k i
  Lagrange.interpolate (Finset.univ : Finset (Fin (k + 1)))
    (@boundaryNode r k) (@boundaryValue u r k)

/--
The order-`k` reconstructed trace from cell `cell`, evaluated at the interface
whose translated coordinate is `interface`.  This is `(P_i^(k))'` in (2.11).
-/
def reconstructedTrace (u : CellData) (k : ℕ) (cell interface : ℤ) : ℝ :=
  (primitiveReconstruction u k cell).derivative.eval (interface : ℝ)

/-- The reconstructed interface jump from (2.12). -/
def reconstructedJump (u : CellData) (k : ℕ) (i : ℤ) : ℝ :=
  reconstructedTrace u k (i + 1) i - reconstructedTrace u k i i

/--
All indices at which `jump u` can be nonzero.  Summing over this set is exactly
the paper's sum over all integers, because the other summands have `a_i = 0`.
-/
def jumpIndexSet (u : CellData) : Finset ℤ :=
  u.support ∪ u.support.image (fun j => j - 1)

/-- The actual data-dependent ENO source `Q_k` from (1.3)/(2.14). -/
def enoSource (u : CellData) (k : ℕ) : ℝ :=
  ∑ i ∈ jumpIndexSet u, jump u i * reconstructedJump u k i

/-- The `ℓ∞` amplitude of the compactly supported cell-average sequence. -/
def amplitude (u : CellData) : ℝ :=
  if h : u.support.Nonempty then u.support.sup' h (fun i => |u i|) else 0

/-- The `(k+1)`st absolute jump moment in the ENO--TV estimate. -/
def jumpMoment (u : CellData) (k : ℕ) : ℝ :=
  ∑ i ∈ jumpIndexSet u, |jump u i| ^ (k + 1)

/-- The paper's uniform coercivity assertion at one reconstruction order. -/
def CoerciveAt (k : ℕ) : Prop :=
  ∃ C : ℝ, 0 < C ∧ ∀ u : CellData,
    jumpMoment u k ≤ C * amplitude u ^ (k - 1) * enoSource u k

/--
Theorem A (central parity classification), stated with the paper's definitions:
uniform ENO--TV coercivity holds exactly at order two and at odd orders.
-/
def theoremA_statement : Prop :=
  ∀ k : ℕ, 2 ≤ k → (CoerciveAt k ↔ k = 2 ∨ Odd k)

#check theoremA_statement
#print axioms theoremA_statement

end ENOTV