IndisputableMonolith.NumberTheory.RiemannHypothesis.CertificateWindow

   1import IndisputableMonolith.NumberTheory.RiemannHypothesis.WindowToOscillation
   2import Mathlib.Analysis.LConvolution
   3
   4/-!
   5# RH (BRF route): concrete certificate windows `φ_{L,t0}`
   6
   7This file defines the actual **window functions** used in the certificate layer:
   8
   9- a **flat-top window** built from a profile `ψ` with a unit plateau on `[-1,1]`,
  10  scaled to mass `1` by `1/L`;
  11- a **Poisson-plateau window** (abstractly) as a Poisson-kernel convolution of the profile,
  12  also scaled by `1/L`.
  13
  14We then instantiate the B1 bridge from `WindowToOscillation`:
  15
  16`(∫ φ_{L,t0} d(-w') ≤ D) + (φ_{L,t0} ≥ c on Ioo(t0-L,t0+L))  ⇒  oscOn w (Icc(t0-L,t0+L)) ≤ D / c`.
  17-/
  18
  19namespace IndisputableMonolith
  20namespace NumberTheory
  21namespace RiemannHypothesis
  22
  23open scoped Real Topology ENNReal MeasureTheory
  24open MeasureTheory Filter Set
  25
  26/-!
  27## Flat-top window
  28-/
  29
  30/-- The (nonnegative) flat-top window associated to a profile `ψ : ℝ → ℝ` at scale `L>0`
  31and center `t0`:
  32\[
  33  \varphi_{L,t0}(t) := \mathrm{ofReal}\Big(\frac{\psi((t-t0)/L)}{L}\Big).
  34\]
  35
  36This matches the manuscript’s `L^{-1} ψ((t-t0)/L)` when `ψ ≥ 0`.
  37-/
  38noncomputable def certificateWindowFlat (ψ : ℝ → ℝ) (L t0 : ℝ) : ℝ → ℝ≥0∞ :=
  39  fun t => ENNReal.ofReal (ψ ((t - t0) / L) / L)
  40
  41namespace certificateWindowFlat
  42
  43variable {ψ : ℝ → ℝ} {L t0 : ℝ}
  44
  45lemma lower_of_plateau_one (hL : 0 < L)
  46    (hψ : ∀ x : ℝ, |x| ≤ 1 → ψ x = 1) :
  47    ∀ t, t ∈ Set.Ioo (t0 - L) (t0 + L) →
  48      ENNReal.ofReal (1 / L) ≤ certificateWindowFlat ψ L t0 t := by
  49  intro t ht
  50  have hlt : |t - t0| < L := by
  51    have h1 : t - t0 < L := by linarith [ht.2]
  52    have h2 : -L < t - t0 := by linarith [ht.1]
  53    exact abs_lt.2 ⟨h2, h1⟩
  54  have habs : |(t - t0) / L| ≤ 1 := by
  55    have habs' : |(t - t0) / L| < 1 := by
  56      -- `|(t-t0)/L| = |t-t0|/L < 1` since `|t-t0| < L` and `L>0`.
  57      have : |t - t0| / L < 1 := by
  58        -- rewrite as `|t-t0| < 1*L`.
  59        have : |t - t0| < 1 * L := by simpa using hlt
  60        -- `b / c < a ↔ b < a*c`
  61        exact (div_lt_iff₀ hL).2 (by simpa [one_mul] using this)
  62      simpa [abs_div, abs_of_pos hL] using this
  63    exact le_of_lt habs'
  64  have hψ1 : ψ ((t - t0) / L) = 1 := hψ _ habs
  65  -- On the plateau, the window equals `ofReal (1/L)`.
  66  simp [certificateWindowFlat, hψ1, one_div]
  67
  68end certificateWindowFlat
  69
  70/-!
  71## Poisson kernel and Poisson-plateau window (scaled)
  72
  73We define the normalized Poisson kernel on `ℝ` (as an `ℝ≥0∞`-valued function) and the
  74additive `⋆ₗ` convolution window `P_b * ψ`, then scale it in the same `L^{-1}` manner.
  75
  76This is set up so the manuscript constant
  77`c0(ψ) := inf_{0<b≤1, |x|≤1} (P_b * ψ)(x)` can be plugged in later.
  78-/
  79
  80/-- Normalized Poisson kernel on `ℝ` (as a nonnegative `ℝ≥0∞` function). -/
  81noncomputable def poissonKernel (b : ℝ) : ℝ → ℝ≥0∞ :=
  82  fun x => ENNReal.ofReal ((1 / Real.pi) * (b / (b ^ 2 + x ^ 2)))
  83
  84/-- Poisson convolution of a profile `ψ : ℝ → ℝ≥0∞` at height `b`. -/
  85noncomputable def poissonConv (b : ℝ) (ψ : ℝ → ℝ≥0∞) : ℝ → ℝ≥0∞ :=
  86  (poissonKernel b ⋆ₗ[volume] ψ)
  87
  88/-- The value-set used to define the manuscript constant
  89\[
  90  c_0(ψ) := \inf_{0<b\le 1,\ |x|\le 1} (P_b * ψ)(x).
  91\]
  92
  93We store the infimum in `ℝ≥0∞` since `poissonConv` is `ℝ≥0∞`-valued. -/
  94def poissonPlateauValSet (ψ : ℝ → ℝ≥0∞) : Set ℝ≥0∞ :=
  95  { y | ∃ b : ℝ, 0 < b ∧ b ≤ 1 ∧ ∃ x : ℝ, |x| ≤ 1 ∧ y = poissonConv b ψ x }
  96
  97/-- The Poisson plateau constant `c0(ψ)` as an `ℝ≥0∞` infimum. -/
  98noncomputable def c0PoissonENN (ψ : ℝ → ℝ≥0∞) : ℝ≥0∞ :=
  99  sInf (poissonPlateauValSet ψ)
 100
 101/-- Convenience real-valued version `c0(ψ)` defined as `toReal` of the `ℝ≥0∞` infimum.
 102
 103To use it as a genuine plateau constant (rather than defaulting to `0` when `= ⊤`),
 104you will typically assume `c0PoissonENN ψ ≠ ⊤` and `0 < c0Poisson ψ`. -/
 105noncomputable def c0Poisson (ψ : ℝ → ℝ≥0∞) : ℝ :=
 106  (c0PoissonENN ψ).toReal
 107
 108lemma c0PoissonENN_le_poissonConv {ψ : ℝ → ℝ≥0∞} {b x : ℝ}
 109    (hb0 : 0 < b) (hb1 : b ≤ 1) (hx : |x| ≤ 1) :
 110    c0PoissonENN ψ ≤ poissonConv b ψ x := by
 111  -- `Inf S ≤ a` for any `a ∈ S`.
 112  unfold c0PoissonENN
 113  refine sInf_le ?_
 114  exact ⟨b, hb0, hb1, x, hx, rfl⟩
 115
 116lemma ofReal_c0Poisson_le_poissonConv {ψ : ℝ → ℝ≥0∞} {b x : ℝ}
 117    (hc0_top : c0PoissonENN ψ ≠ ⊤) (hb0 : 0 < b) (hb1 : b ≤ 1) (hx : |x| ≤ 1) :
 118    ENNReal.ofReal (c0Poisson ψ) ≤ poissonConv b ψ x := by
 119  have h0 : c0PoissonENN ψ ≤ poissonConv b ψ x :=
 120    c0PoissonENN_le_poissonConv (ψ := ψ) (b := b) (x := x) hb0 hb1 hx
 121  -- Rewrite `ofReal (toReal (c0PoissonENN ψ))` back to `c0PoissonENN ψ`.
 122  have hrew : ENNReal.ofReal (c0Poisson ψ) = c0PoissonENN ψ := by
 123    simpa [c0Poisson] using (ENNReal.ofReal_toReal (a := c0PoissonENN ψ) hc0_top)
 124  simpa [hrew] using h0
 125
 126lemma hpoisson_plateau_of_c0Poisson {ψ : ℝ → ℝ≥0∞} {b : ℝ}
 127    (hc0_top : c0PoissonENN ψ ≠ ⊤) (hb0 : 0 < b) (hb1 : b ≤ 1) :
 128    ∀ x : ℝ, |x| ≤ 1 → ENNReal.ofReal (c0Poisson ψ) ≤ poissonConv b ψ x := by
 129  intro x hx
 130  exact ofReal_c0Poisson_le_poissonConv (ψ := ψ) (b := b) (x := x) hc0_top hb0 hb1 hx
 131
 132/-- The scaled Poisson-plateau window at scale `L` and center `t0`:
 133\[
 134  \varphi^{P}_{L,t0}(t) := \frac{1}{L}\,(P_b * ψ)\big((t-t0)/L\big),
 135\]
 136encoded in `ℝ≥0∞` using `ENNReal.ofReal`.
 137
 138This matches the user-facing “`c0(ψ)/L` plateau” behavior on `t ∈ (t0-L,t0+L)` when
 139`(P_b*ψ)(x) ≥ c0(ψ)` for `|x|≤1`.
 140-/
 141noncomputable def certificateWindowPoisson (b : ℝ) (ψ : ℝ → ℝ≥0∞) (L t0 : ℝ) : ℝ → ℝ≥0∞ :=
 142  fun t => (ENNReal.ofReal (1 / L)) * (poissonConv b ψ ((t - t0) / L))
 143
 144/-!
 145## Instantiations of the B1 bridge (`window` ⇒ `oscOn`) on a Whitney interval
 146-/
 147
 148theorem oscOn_Icc_whitney_le_mul_L_of_flatTop
 149    {w : ℝ → ℝ} (hw : Antitone w) (hw_rc : ∀ x, ContinuousWithinAt w (Ici x) x)
 150    {ψ : ℝ → ℝ} {L t0 D : ℝ} (hL : 0 < L) (hD : 0 ≤ D)
 151    (hψ : ∀ x : ℝ, |x| ≤ 1 → ψ x = 1)
 152    (hlin :
 153      ∫⁻ t, certificateWindowFlat ψ L t0 t ∂(stieltjesNeg.μ (w := w) (hw := hw) (hw_rc := hw_rc))
 154        ≤ ENNReal.ofReal D) :
 155    oscOn w (Set.Icc (t0 - L) (t0 + L)) ≤ D * L := by
 156  have hab : (t0 - L) < (t0 + L) := by linarith
 157  have hc : 0 < (1 / L) := one_div_pos.2 hL
 158  have hφ_lower :
 159      ∀ t, t ∈ Set.Ioo (t0 - L) (t0 + L) → ENNReal.ofReal (1 / L) ≤ certificateWindowFlat ψ L t0 t :=
 160    certificateWindowFlat.lower_of_plateau_one (ψ := ψ) (L := L) (t0 := t0) hL hψ
 161  have hosC :
 162      oscOn w (Set.Icc (t0 - L) (t0 + L)) ≤ D / (1 / L) := by
 163    simpa [Set.Ioo] using
 164      oscOn_Icc_le_div_of_window_lintegral_bound (w := w) hw hw_rc (a := t0 - L) (b := t0 + L)
 165        (D := D) (c := (1 / L)) hab hD hc hφ_lower hlin
 166  -- simplify `D / (1/L)` to `D*L`
 167  simpa [div_div, one_div] using (le_trans hosC (le_of_eq (by field_simp [hL.ne'])))
 168
 169theorem oscOn_Icc_whitney_le_div_c0_mul_L_of_poissonPlateau
 170    {w : ℝ → ℝ} (hw : Antitone w) (hw_rc : ∀ x, ContinuousWithinAt w (Ici x) x)
 171    {ψ : ℝ → ℝ≥0∞} {b L t0 D c0 : ℝ} (hL : 0 < L) (hD : 0 ≤ D) (hc0 : 0 < c0)
 172    (hpoisson_plateau :
 173      ∀ x : ℝ, |x| ≤ 1 → ENNReal.ofReal c0 ≤ poissonConv b ψ x)
 174    (hlin :
 175      ∫⁻ t, certificateWindowPoisson b ψ L t0 t
 176          ∂(stieltjesNeg.μ (w := w) (hw := hw) (hw_rc := hw_rc))
 177        ≤ ENNReal.ofReal D) :
 178    oscOn w (Set.Icc (t0 - L) (t0 + L)) ≤ (D / c0) * L := by
 179  have hab : (t0 - L) < (t0 + L) := by linarith
 180  -- lower bound `c0/L` on `Ioo`.
 181  have hφ_lower :
 182      ∀ t, t ∈ Set.Ioo (t0 - L) (t0 + L) →
 183        ENNReal.ofReal (c0 / L) ≤ certificateWindowPoisson b ψ L t0 t := by
 184    intro t ht
 185    have hlt : |t - t0| < L := by
 186      have h1 : t - t0 < L := by linarith [ht.2]
 187      have h2 : -L < t - t0 := by linarith [ht.1]
 188      exact abs_lt.2 ⟨h2, h1⟩
 189    have habs : |(t - t0) / L| ≤ 1 := by
 190      have habs' : |(t - t0) / L| < 1 := by
 191        have : |t - t0| / L < 1 := by
 192          have : |t - t0| < 1 * L := by simpa using hlt
 193          exact (div_lt_iff₀ hL).2 (by simpa [one_mul] using this)
 194        simpa [abs_div, abs_of_pos hL] using this
 195      exact le_of_lt habs'
 196    have hconv : ENNReal.ofReal c0 ≤ poissonConv b ψ ((t - t0) / L) := hpoisson_plateau _ habs
 197    -- multiply by `1/L` to get `c0/L`.
 198    -- `ofReal (c0/L) = ofReal c0 * ofReal (1/L)` (since both nonnegative).
 199    have hrew : ENNReal.ofReal (c0 / L) = ENNReal.ofReal c0 * ENNReal.ofReal (1 / L) := by
 200      -- `c0 / L = c0 * (1/L)`
 201      simpa [div_eq_mul_inv] using (ENNReal.ofReal_mul (p := c0) (q := (1 / L)) (le_of_lt hc0))
 202    have hrew' : ENNReal.ofReal (c0 / L) = ENNReal.ofReal (1 / L) * ENNReal.ofReal c0 := by
 203      simpa [mul_comm] using hrew
 204    -- Now: multiply the plateau inequality by `ofReal (1/L)`.
 205    have hmul :
 206        ENNReal.ofReal (1 / L) * ENNReal.ofReal c0
 207          ≤ ENNReal.ofReal (1 / L) * poissonConv b ψ ((t - t0) / L) :=
 208      mul_le_mul_right hconv (ENNReal.ofReal (1 / L))
 209    -- Repackage as the window lower bound.
 210    simpa [certificateWindowPoisson, hrew', mul_assoc] using hmul
 211  -- Apply the generic B1 bridge with `c = c0/L`.
 212  have hc : 0 < (c0 / L) := by exact div_pos hc0 hL
 213  have hosC :
 214      oscOn w (Set.Icc (t0 - L) (t0 + L)) ≤ D / (c0 / L) := by
 215    simpa using
 216      oscOn_Icc_le_div_of_window_lintegral_bound (w := w) hw hw_rc (a := t0 - L) (b := t0 + L)
 217        (D := D) (c := (c0 / L)) hab hD hc hφ_lower hlin
 218  -- simplify `D / (c0/L) = (D/c0) * L`.
 219  have : D / (c0 / L) = (D / c0) * L := by
 220    field_simp [hL.ne', (ne_of_gt hc0)]
 221  simpa [this, mul_assoc] using hosC
 222
 223theorem oscOn_Icc_whitney_le_div_c0Poisson_mul_L_of_poissonPlateau
 224    {w : ℝ → ℝ} (hw : Antitone w) (hw_rc : ∀ x, ContinuousWithinAt w (Ici x) x)
 225    {ψ : ℝ → ℝ≥0∞} {b L t0 D : ℝ} (hL : 0 < L) (hD : 0 ≤ D)
 226    (hb0 : 0 < b) (hb1 : b ≤ 1)
 227    (hc0_top : c0PoissonENN ψ ≠ ⊤) (hc0 : 0 < c0Poisson ψ)
 228    (hlin :
 229      ∫⁻ t, certificateWindowPoisson b ψ L t0 t
 230          ∂(stieltjesNeg.μ (w := w) (hw := hw) (hw_rc := hw_rc))
 231        ≤ ENNReal.ofReal D) :
 232    oscOn w (Set.Icc (t0 - L) (t0 + L)) ≤ (D / (c0Poisson ψ)) * L := by
 233  -- This is the previous theorem, with `hpoisson_plateau` derived from the definition of `c0Poisson`.
 234  refine
 235    oscOn_Icc_whitney_le_div_c0_mul_L_of_poissonPlateau (w := w) hw hw_rc (ψ := ψ) (b := b)
 236      (L := L) (t0 := t0) (D := D) (c0 := c0Poisson ψ) hL hD hc0
 237      (hpoisson_plateau := hpoisson_plateau_of_c0Poisson (ψ := ψ) (b := b) hc0_top hb0 hb1)
 238      (hlin := hlin)
 239
 240end RiemannHypothesis
 241end NumberTheory
 242end IndisputableMonolith
 243