2607.19283v1 / ENOTV/EvenFailure.lean

all files

import ENOTV.EvenEnergy

/-!
# Failure of coercivity in every even order at least four

The local estimates are reduced here to the scale calculation in the
paper.  We use `P=L^d` positive/negative block pairs; this differs from the
paper's notation only by counting pairs rather than individual blocks.
-/

noncomputable section

namespace ENOTV

def evenEnergyConstant (d : ℕ) : ℝ :=
  2 * (d + 1) *
    ((endpointUpper d (d + 1) : ℝ) * (junctionUpper d : ℝ) +
      2 ^ (d + 1) * (endpointUpper d (d + 1) : ℝ) ^ 2)

theorem evenEnergyConstant_nonneg (d : ℕ) :
    0 ≤ evenEnergyConstant d := by
  unfold evenEnergyConstant
  have hE : 0 ≤ (endpointUpper d (d + 1) : ℝ) := by
    exact_mod_cast endpointUpper_nonneg d (d + 1)
  have hJ : 0 ≤ (junctionUpper d : ℝ) := by
    exact_mod_cast junctionUpper_nonneg d
  positivity

theorem cEnergy_power_pairs_upper {d L : ℕ}
    (hd : 2 ≤ d) (heven : Even d) (hL : d + 1 ≤ L) :
    cEnergy (d + 2) (multiJumps d L (L ^ d)) ≤
      evenEnergyConstant d * (L : ℝ) ^ (2 * d - 1) := by
  have hLpos : 0 < L := by omega
  have hP : 0 < L ^ d := pow_pos hLpos _
  have hraw := cEnergy_multiJumps_upper (d := d) (L := L) (P := L ^ d)
    (by omega) heven hL hP
  let E : ℝ := (endpointUpper d (d + 1) : ℝ)
  let J : ℝ := (junctionUpper d : ℝ)
  have hE : 0 ≤ E := by
    dsimp [E]
    exact_mod_cast endpointUpper_nonneg d (d + 1)
  have hJ : 0 ≤ J := by
    dsimp [J]
    exact_mod_cast junctionUpper_nonneg d
  have hL1 : (1 : ℝ) ≤ L := by exact_mod_cast (show 1 ≤ L by omega)
  have hpow₁ :
      (L : ℝ) ^ d * (L : ℝ) ^ (d - 1) =
        (L : ℝ) ^ (2 * d - 1) := by
    rw [← pow_add]
    congr 1
    omega
  have hpow₂ :
      (L : ℝ) ^ (d - 1) * (L : ℝ) ^ (d - 1) =
        (L : ℝ) ^ (2 * d - 2) := by
    rw [← pow_add]
    congr 1
    omega
  have hpowmono :
      (L : ℝ) ^ (2 * d - 2) ≤ (L : ℝ) ^ (2 * d - 1) := by
    exact pow_le_pow_right₀ hL1 (by omega)
  have hPcast : ((L ^ d : ℕ) : ℝ) = (L : ℝ) ^ d := by norm_num
  have hsub :
      (((2 * (L ^ d) - 1 : ℕ) : ℝ)) ≤
        2 * (L : ℝ) ^ d := by
    rw [← hPcast]
    exact_mod_cast (Nat.sub_le (2 * L ^ d) 1)
  unfold boundaryAmplitudeUpper endpointEnergyUpper at hraw
  change cEnergy (d + 2) (multiJumps d L (L ^ d)) ≤
      ((2 * (L ^ d) - 1 : ℕ) : ℝ) * (d + 1) *
          ((E * (L : ℝ) ^ (d - 1)) * J) +
        2 * (d + 1) *
          ((E * (L : ℝ) ^ (d - 1)) *
            (2 ^ (d + 1) * (E * (L : ℝ) ^ (d - 1)))) at hraw
  calc
    cEnergy (d + 2) (multiJumps d L (L ^ d)) ≤
        ((2 * (L ^ d) - 1 : ℕ) : ℝ) * (d + 1) *
            ((E * (L : ℝ) ^ (d - 1)) * J) +
          2 * (d + 1) *
            ((E * (L : ℝ) ^ (d - 1)) *
              (2 ^ (d + 1) * (E * (L : ℝ) ^ (d - 1)))) := hraw
    _ ≤ (2 * (L : ℝ) ^ d) * (d + 1) *
            ((E * (L : ℝ) ^ (d - 1)) * J) +
          2 * (d + 1) *
            ((E * (L : ℝ) ^ (d - 1)) *
              (2 ^ (d + 1) * (E * (L : ℝ) ^ (d - 1)))) := by
      gcongr
    _ = 2 * (d + 1) * (E * J) *
            (L : ℝ) ^ (2 * d - 1) +
          2 * (d + 1) * (2 ^ (d + 1) * E ^ 2) *
            (L : ℝ) ^ (2 * d - 2) := by
      rw [← hpow₁, ← hpow₂]
      ring
    _ ≤ 2 * (d + 1) * (E * J) *
            (L : ℝ) ^ (2 * d - 1) +
          2 * (d + 1) * (2 ^ (d + 1) * E ^ 2) *
            (L : ℝ) ^ (2 * d - 1) := by
      gcongr
    _ = evenEnergyConstant d * (L : ℝ) ^ (2 * d - 1) := by
      unfold evenEnergyConstant
      dsimp [E, J]
      ring

def evenDenominatorConstant (d : ℕ) : ℝ :=
  (4 * (eulerUpper d : ℝ)) ^ (d + 1) *
    gammaMax (d + 2) (by omega) * evenEnergyConstant d

theorem evenDenominatorConstant_nonneg (d : ℕ) :
    0 ≤ evenDenominatorConstant d := by
  unfold evenDenominatorConstant
  have hG : 0 ≤ gammaMax (d + 2) (by omega) :=
    (abs_nonneg (gamma (d + 2) 0)).trans
      (gamma_le_gammaMax (by omega) (by omega))
  have hEuler : 0 ≤ (eulerUpper d : ℝ) := by
    exact_mod_cast eulerUpper_nonneg d
  exact mul_nonneg (mul_nonneg (pow_nonneg (by positivity) _) hG)
    (evenEnergyConstant_nonneg d)

theorem amplitude_source_power_upper
    (hFMT : FMTReconstructionTheorem) {d L : ℕ}
    (hd : 2 ≤ d) (heven : Even d) (hL : d + 1 ≤ L) :
    camplitude (multiDatum d L (L ^ d)) ^ (d + 1) *
        cSource (d + 2) (multiDatum d L (L ^ d)) ≤
      evenDenominatorConstant d * (L : ℝ) ^ (d ^ 2 + 4 * d) := by
  have hLpos : 0 < L := by omega
  have hA := multiDatum_amplitude_bound d L (L ^ d) hLpos
  have hS := source_le_energy hFMT (by omega : 2 ≤ d + 2)
    (multiDatum d L (L ^ d))
  rw [cdiff_multiDatum] at hS
  have hE := cEnergy_power_pairs_upper hd heven hL
  have hA0 : 0 ≤ camplitude (multiDatum d L (L ^ d)) :=
    camplitude_nonneg _
  have hAbound0 : 0 ≤ 4 * (eulerUpper d : ℝ) *
      (L : ℝ) ^ (d + 1) := by
    have : 0 ≤ (eulerUpper d : ℝ) := by exact_mod_cast eulerUpper_nonneg d
    positivity
  have hApow := pow_le_pow_left₀ hA0 hA (d + 1)
  have hG : 0 ≤ gammaMax (d + 2) (by omega) :=
    (abs_nonneg (gamma (d + 2) 0)).trans
      (gamma_le_gammaMax (by omega) (by omega))
  have hSpow :
      cSource (d + 2) (multiDatum d L (L ^ d)) ≤
        gammaMax (d + 2) (by omega) *
          (evenEnergyConstant d * (L : ℝ) ^ (2 * d - 1)) :=
    hS.trans (mul_le_mul_of_nonneg_left hE hG)
  have hS0 : 0 ≤ cSource (d + 2) (multiDatum d L (L ^ d)) := by
    rw [cSource_eq_ownerSource hFMT (by omega)]
    unfold ownerSource
    apply Finsupp.sum_nonneg
    intro j hj
    positivity
  calc
    camplitude (multiDatum d L (L ^ d)) ^ (d + 1) *
          cSource (d + 2) (multiDatum d L (L ^ d)) ≤
        (4 * (eulerUpper d : ℝ) * (L : ℝ) ^ (d + 1)) ^ (d + 1) *
          (gammaMax (d + 2) (by omega) *
            (evenEnergyConstant d * (L : ℝ) ^ (2 * d - 1))) := by
      exact mul_le_mul hApow hSpow hS0 (pow_nonneg hAbound0 _)
    _ = evenDenominatorConstant d *
          (L : ℝ) ^ (d ^ 2 + 4 * d) := by
      unfold evenDenominatorConstant
      rw [mul_pow, ← pow_mul]
      have hpow :
          (L : ℝ) ^ ((d + 1) * (d + 1)) *
              (L : ℝ) ^ (2 * d - 1) =
            (L : ℝ) ^ (d ^ 2 + 4 * d) := by
        rw [← pow_add]
        congr 1
        rw [show (d + 1) * (d + 1) = d ^ 2 + 2 * d + 1 by ring]
        omega
      calc
        (4 * (eulerUpper d : ℝ)) ^ (d + 1) *
              (L : ℝ) ^ ((d + 1) * (d + 1)) *
              (gammaMax (d + 2) (by omega) *
                (evenEnergyConstant d * (L : ℝ) ^ (2 * d - 1))) =
            (4 * (eulerUpper d : ℝ)) ^ (d + 1) *
              gammaMax (d + 2) (by omega) * evenEnergyConstant d *
              ((L : ℝ) ^ ((d + 1) * (d + 1)) *
                (L : ℝ) ^ (2 * d - 1)) := by ring
        _ = (4 * (eulerUpper d : ℝ)) ^ (d + 1) *
              gammaMax (d + 2) (by omega) * evenEnergyConstant d *
              (L : ℝ) ^ (d ^ 2 + 4 * d) := by rw [hpow]

theorem exists_moment_power_lower (d : ℕ) :
    ∃ b : ℕ, ∃ c₀ : ℝ, 0 < b ∧ 0 < c₀ ∧
      ∀ M : ℕ, 0 < M →
        let L := b * M
        c₀ * (M : ℝ) * (L : ℝ) ^ (d ^ 2 + 4 * d) ≤
          cJumpMoment (d + 2) (multiDatum d L (L ^ d)) := by
  obtain ⟨b, c, hb, hc, hlower⟩ :=
    exists_multi_moment_lower d (d + 2)
  refine ⟨b, (c : ℝ) ^ (d + 3), hb, pow_pos (by exact_mod_cast hc) _, ?_⟩
  intro M hM
  let L := b * M
  have hraw := hlower M (L ^ d) hM
  dsimp only at hraw ⊢
  change ((L ^ d : ℕ) : ℝ) * (M : ℝ) *
      ((c : ℝ) * (L : ℝ) ^ d) ^ (d + 3) ≤
        cJumpMoment (d + 2) (multiDatum d L (L ^ d)) at hraw
  have hpow :
      (L : ℝ) ^ d * (L : ℝ) ^ (d * (d + 3)) =
        (L : ℝ) ^ (d ^ 2 + 4 * d) := by
    rw [← pow_add]
    congr 1
    ring
  calc
    (c : ℝ) ^ (d + 3) * (M : ℝ) *
          (L : ℝ) ^ (d ^ 2 + 4 * d) =
        ((L ^ d : ℕ) : ℝ) * (M : ℝ) *
          ((c : ℝ) * (L : ℝ) ^ d) ^ (d + 3) := by
      push_cast
      rw [mul_pow, ← pow_mul, ← hpow]
      ring
    _ ≤ cJumpMoment (d + 2) (multiDatum d L (L ^ d)) := hraw

theorem not_CCoercive_even_core
    (hFMT : FMTReconstructionTheorem) (d : ℕ)
    (hd : 2 ≤ d) (heven : Even d) :
    ¬ CCoercive (d + 2) := by
  rintro ⟨C, hC, hcoerc⟩
  obtain ⟨b, c₀, hb, hc₀, hlower⟩ := exists_moment_power_lower d
  let D := evenDenominatorConstant d
  obtain ⟨N, hN⟩ := exists_nat_gt (C * D / c₀)
  let M := N + d + 1
  let L := b * M
  have hM : 0 < M := by dsimp [M]; omega
  have hMlarge : d + 1 ≤ M := by dsimp [M]; omega
  have hb1 : 1 ≤ b := by omega
  have hL : d + 1 ≤ L := by
    dsimp [L]
    exact hMlarge.trans (by simpa using Nat.mul_le_mul_right M hb1)
  have hconst : C * D < c₀ * (M : ℝ) := by
    have hNM : (N : ℝ) ≤ (M : ℝ) := by
      exact_mod_cast (show N ≤ M by dsimp [M]; omega)
    have hdiv : C * D / c₀ < (M : ℝ) := hN.trans_le hNM
    have := (div_lt_iff₀ hc₀).mp hdiv
    nlinarith
  have hbulk := hlower M hM
  dsimp only at hbulk
  change c₀ * (M : ℝ) * (L : ℝ) ^ (d ^ 2 + 4 * d) ≤
      cJumpMoment (d + 2) (multiDatum d L (L ^ d)) at hbulk
  have hden := amplitude_source_power_upper hFMT hd heven hL
  change camplitude (multiDatum d L (L ^ d)) ^ (d + 1) *
      cSource (d + 2) (multiDatum d L (L ^ d)) ≤
        D * (L : ℝ) ^ (d ^ 2 + 4 * d) at hden
  have hco := hcoerc (multiDatum d L (L ^ d))
  have hupper :
      cJumpMoment (d + 2) (multiDatum d L (L ^ d)) ≤
        C * D * (L : ℝ) ^ (d ^ 2 + 4 * d) := by
    calc
      cJumpMoment (d + 2) (multiDatum d L (L ^ d)) ≤
          C * camplitude (multiDatum d L (L ^ d)) ^ (d + 2 - 1) *
            cSource (d + 2) (multiDatum d L (L ^ d)) := hco
      _ = C * (camplitude (multiDatum d L (L ^ d)) ^ (d + 1) *
            cSource (d + 2) (multiDatum d L (L ^ d))) := by
        rw [show d + 2 - 1 = d + 1 by omega]
        ring
      _ ≤ C * (D * (L : ℝ) ^ (d ^ 2 + 4 * d)) := by
        gcongr
      _ = C * D * (L : ℝ) ^ (d ^ 2 + 4 * d) := by ring
  have hLpos : (0 : ℝ) < L := by
    exact_mod_cast (show 0 < L by omega)
  have hpowpos : 0 < (L : ℝ) ^ (d ^ 2 + 4 * d) :=
    pow_pos hLpos _
  have hstrict :
      C * D * (L : ℝ) ^ (d ^ 2 + 4 * d) <
        c₀ * (M : ℝ) * (L : ℝ) ^ (d ^ 2 + 4 * d) := by
    exact mul_lt_mul_of_pos_right hconst hpowpos
  linarith

theorem not_CCoercive_even
    (hFMT : FMTReconstructionTheorem) {k : ℕ}
    (hk : 4 ≤ k) (heven : Even k) :
    ¬ CCoercive k := by
  let d := k - 2
  have hd : 2 ≤ d := by dsimp [d]; omega
  have hkform : k = d + 2 := by dsimp [d]; omega
  have hdeven : Even d := by
    obtain ⟨q, hq⟩ := heven
    refine ⟨q - 1, ?_⟩
    dsimp [d]
    omega
  rw [hkform]
  exact not_CCoercive_even_core hFMT d hd hdeven

end ENOTV