2607.19283v1 / ENOTV/Positive.lean

all files

import ENOTV.SourceComparison

/-!
# Odd-order coercivity from the two analytic interfaces

The only standard analytic result absent from mathlib is the all-order
discrete Gagliardo--Nirenberg inequality.  We expose it as a named
hypothesis rather than hiding it as a global declaration.  The ENO-specific source
localization interface is kept separate.
-/

noncomputable section

namespace ENOTV

/-- Standard discrete Gagliardo--Nirenberg inequality used in the paper. -/
def DiscreteGagliardoNirenberg : Prop :=
  ∀ m : ℕ, 2 ≤ m →
    ∃ C : ℝ, 0 ≤ C ∧ ∀ v : CSeq,
      cJumpMoment (2 * m - 1) v ≤
        C * camplitude v ^ (2 * m - 2) *
          dot (cdiffIter m v) (cdiffIter m v)

/-- The direction of the source-localization theorem needed for odd
coercivity.  This is intentionally a separately named interface: it is the
paper's ENO-specific combinatorial theorem, not part of the standard
analytic hypothesis above. -/
def SourceDominatesEnergy : Prop :=
  ∀ k : ℕ, 2 ≤ k →
    ∃ K : ℝ, 0 < K ∧ ∀ u : CSeq,
      cEnergy k (cdiff u) ≤ K * cSource k u

theorem cdiffIter_cdiff (n : ℕ) (u : CSeq) :
    cdiffIter n (cdiff u) = cdiffIter (n + 1) u := by
  change cdiffIter n (cdiffIter 1 u) = cdiffIter (n + 1) u
  exact cdiffIter_add n 1 u

theorem odd_coercive_of_interfaces
    (hGN : DiscreteGagliardoNirenberg)
    (hsource : SourceDominatesEnergy)
    (m : ℕ) (hm : 2 ≤ m) :
    CCoercive (2 * m - 1) := by
  obtain ⟨C, hC, hGNm⟩ := hGN m hm
  obtain ⟨K, hK, hloc⟩ := hsource (2 * m - 1) (by omega)
  refine ⟨C * K, mul_nonneg hC hK.le, ?_⟩
  intro u
  have hsq :
      dot (cdiffIter m u) (cdiffIter m u) ≤
        cEnergy (2 * m - 1) (cdiff u) := by
    have he := square_energy_le_localized (m - 1) (cdiff u)
    rw [cdiffIter_cdiff, show m - 1 + 1 = m by omega] at he
    have hk : 2 * (m - 1) + 1 = 2 * m - 1 := by omega
    rw [hk] at he
    exact he
  have hU : 0 ≤ camplitude u ^ (2 * m - 2) :=
    pow_nonneg (camplitude_nonneg u) _
  have hscale : 0 ≤ C * camplitude u ^ (2 * m - 2) :=
    mul_nonneg hC hU
  calc
    cJumpMoment (2 * m - 1) u ≤
        C * camplitude u ^ (2 * m - 2) *
          dot (cdiffIter m u) (cdiffIter m u) := hGNm u
    _ ≤ C * camplitude u ^ (2 * m - 2) *
          cEnergy (2 * m - 1) (cdiff u) := by gcongr
    _ ≤ C * camplitude u ^ (2 * m - 2) *
          (K * cSource (2 * m - 1) u) := by
      gcongr
      exact hloc u
    _ = (C * K) * camplitude u ^ (2 * m - 1 - 1) *
          cSource (2 * m - 1) u := by
      have hexp : 2 * m - 1 - 1 = 2 * m - 2 := by omega
      rw [hexp]
      ring

theorem sourceDominatesEnergy_of_FMT
    (hFMT : FMTReconstructionTheorem) :
    SourceDominatesEnergy := by
  intro k hk
  exact source_dominates_energy hFMT hk

theorem odd_coercive
    (hFMT : FMTReconstructionTheorem)
    (hGN : DiscreteGagliardoNirenberg)
    (m : ℕ) (hm : 2 ≤ m) :
    CCoercive (2 * m - 1) :=
  odd_coercive_of_interfaces hGN
    (sourceDominatesEnergy_of_FMT hFMT) m hm

end ENOTV