2607.19283v1 / ENOTV/Representation.lean

all files

import ENOTV.Main

/-!
# Equivalence with the paper's function formulation

The development uses `ℤ →₀ ℝ` so that every sum is manifestly finite.
This file proves that this is exactly the paper's class of compactly
supported functions and that all three quantities in coercivity agree.
-/

noncomputable section

namespace ENOTV

theorem finiteSupport_coe (u : CSeq) : FiniteSupport (u : Seq) := by
  refine u.support.finite_toSet.subset ?_
  intro i hi
  exact Finsupp.mem_support_iff.mpr hi

theorem amplitude_coe (u : CSeq) :
    amplitude (u : Seq) = camplitude u := by
  have hbdd : BddAbove (Set.range fun i : ℤ => |u i|) :=
    ⟨camplitude u, by
      rintro x ⟨i, rfl⟩
      exact abs_le_camplitude u i⟩
  apply le_antisymm
  · apply csSup_le
    · exact Set.range_nonempty _
    · rintro x ⟨i, rfl⟩
      exact abs_le_camplitude u i
  · unfold camplitude
    apply Finset.max'_le
    intro x hx
    simp only [Finset.mem_insert, Finset.mem_image] at hx
    rcases hx with rfl | ⟨i, hi, rfl⟩
    · exact (abs_nonneg (u 0)).trans
        (le_csSup hbdd ⟨0, rfl⟩)
    · exact le_csSup hbdd ⟨i, rfl⟩

theorem jumpMoment_coe (k : ℕ) (u : CSeq) :
    jumpMoment k (u : Seq) = cJumpMoment k u := by
  rw [cJumpMoment_eq_powerSum, powerSum_eq_tsum]
  apply tsum_congr
  intro i
  simp [jumps, diff, cdiff_apply]

theorem source_coe (k : ℕ) (u : CSeq) :
    source k (u : Seq) = cSource k u := by
  rw [cSource_eq_tsum]
  unfold source
  apply tsum_congr
  intro i
  simp [jumps, diff, cdiff_apply]

/-- `CSeq` coercivity is propositionally equivalent to the paper's
compact-support function statement. -/
theorem coercive_iff_CCoercive (k : ℕ) :
    Coercive k ↔ CCoercive k := by
  constructor
  · rintro ⟨C, hC, h⟩
    refine ⟨C, hC, ?_⟩
    intro u
    have hu := h (u : Seq) (finiteSupport_coe u)
    simpa [jumpMoment_coe, amplitude_coe, source_coe] using hu
  · rintro ⟨C, hC, h⟩
    refine ⟨C, hC, ?_⟩
    intro u hu
    let f : CSeq := Finsupp.ofSupportFinite u hu
    have hf : (f : Seq) = u := Finsupp.ofSupportFinite_coe
    have hh := h f
    rw [← jumpMoment_coe, ← amplitude_coe, ← source_coe, hf] at hh
    exact hh

/-- Coercivity stated directly with the naive Lagrange reconstruction,
with no localized formula built into its definition. -/
def LiteralCoercive (k : ℕ) : Prop :=
  ∃ C : ℝ, 0 ≤ C ∧ ∀ u : CSeq,
    cJumpMoment k u ≤
      C * camplitude u ^ (k - 1) * literalSource k u

theorem literalCoercive_iff_CCoercive
    (hFMT : FMTReconstructionTheorem) {k : ℕ} (hk : 2 ≤ k) :
    LiteralCoercive k ↔ CCoercive k := by
  unfold LiteralCoercive CCoercive
  simp_rw [literalSource_eq_cSource hFMT hk]

/-- The parity dichotomy exactly in the paper's `ℤ → ℝ` formulation. -/
theorem eno_tv_parity_dichotomy_paper
    (hFMT : FMTReconstructionTheorem)
    (hGN : DiscreteGagliardoNirenberg)
    (hSecond : SecondOrderENOCoercivity) :
    ∀ k : ℕ, 2 ≤ k →
      (Coercive k ↔ k = 2 ∨ Odd k) := by
  intro k hk
  rw [coercive_iff_CCoercive]
  exact eno_tv_parity_dichotomy hFMT hGN hSecond k hk

/-- The parity dichotomy using the literal Lagrange-reconstructed traces.
This is the closest executable restatement of Theorem A in the paper. -/
theorem eno_tv_parity_dichotomy_literal
    (hFMT : FMTReconstructionTheorem)
    (hGN : DiscreteGagliardoNirenberg)
    (hSecond : SecondOrderENOCoercivity) :
    ∀ k : ℕ, 2 ≤ k →
      (LiteralCoercive k ↔ k = 2 ∨ Odd k) := by
  intro k hk
  rw [literalCoercive_iff_CCoercive hFMT hk]
  exact eno_tv_parity_dichotomy hFMT hGN hSecond k hk

end ENOTV