IndisputableMonolith.NumberTheory.RiemannHypothesis.WindowToOscillation

   1import IndisputableMonolith.NumberTheory.RiemannHypothesis.LocalToGlobalWedge
   2import Mathlib.MeasureTheory.Measure.Stieltjes
   3
   4/-!
   5# Riemann Hypothesis (BRF route): window/measure control → oscillation control
   6
   7This file targets the **bridge step** immediately preceding Lemma
   8`local-to-global-wedge` in `docs/primes/Riemann-proofs/Riemann-active.txt`:
   9
  10> a window (test-function) bound for the positive distribution `-w'`
  11> implies a bound on the essential oscillation
  12> `Δ_I(w) = essSup_I w - essInf_I w`.
  13
  14In Lean, the most robust way to formalize the “integration by parts” aspect is to model `-w'`
  15as a **Stieltjes measure** attached to a monotone right-continuous function. Concretely:
  16
  17- assume `w : ℝ → ℝ` is **antitone** (nonincreasing) and **right-continuous**;
  18- then `g := fun t ↦ -w t` is monotone and right-continuous, hence defines a Stieltjes measure `μ`;
  19- the mass `μ(Ioo a b)` is exactly the **drop** `w a - leftLim w b` (as an `ENNReal.ofReal`);
  20- for antitone `w`, this drop controls the essential oscillation on `Icc a b`.
  21
  22This is a clean, reusable interface: the analytic RH work provides bounds on the Stieltjes mass
  23on Whitney intervals; this file turns them into `oscOn` bounds, which then feed into the already
  24formalized local-to-global wedge lemma.
  25-/
  26
  27namespace IndisputableMonolith
  28namespace NumberTheory
  29namespace RiemannHypothesis
  30
  31open scoped Real Topology
  32open MeasureTheory Filter Set
  33open scoped ENNReal
  34
  35/-!
  36## Plateau/mass extraction (B1 bridge)
  37
  38If `μ` is a measure, `φ ≥ 0` is a window function, and `φ` has a pointwise lower bound `c` on a
  39set `s`, then bounding `∫ φ dμ` controls `μ(s)`:
  40
  41`(∀ x∈s, c ≤ φ x)` and `(∫ φ dμ ≤ A)`  ⇒  `μ(s) ≤ A / c`.
  42
  43This is the Lean version of the “plateau ⇒ mass extraction” step used in the active certificate.
  44-/
  45
  46namespace Plateau
  47
  48theorem measure_le_lintegral_div_of_forall_le_on {α : Type*} [MeasurableSpace α]
  49    {μ : Measure α} {s : Set α} (hs : MeasurableSet s) {φ : α → ℝ≥0∞} {c : ℝ≥0∞}
  50    (hc0 : c ≠ 0) (hcTop : c ≠ ⊤) (hle : ∀ x, x ∈ s → c ≤ φ x) :
  51    μ s ≤ (∫⁻ x, φ x ∂μ) / c := by
  52  -- First show `c * μ s ≤ ∫ φ dμ` by integrating the indicator of the constant `c` over `s`.
  53  have h_ind : s.indicator (fun _ : α => c) ≤ φ := by
  54    intro x
  55    by_cases hx : x ∈ s
  56    · simpa [hx] using hle x hx
  57    · -- outside `s`, the indicator is `0` and `0 ≤ φ x`.
  58      simp [hx]
  59  have hmul : c * μ s ≤ ∫⁻ x, φ x ∂μ := by
  60    calc
  61      c * μ s = ∫⁻ x, s.indicator (fun _ : α => c) x ∂μ := by
  62        simpa using (lintegral_indicator_const (μ := μ) hs c).symm
  63      _ ≤ ∫⁻ x, φ x ∂μ := lintegral_mono h_ind
  64  -- Divide by `c` using `ENNReal.le_div_iff_mul_le`.
  65  have : μ s ≤ (∫⁻ x, φ x ∂μ) / c :=
  66    (ENNReal.le_div_iff_mul_le (Or.inl hc0) (Or.inl hcTop)).2 (by simpa [mul_comm] using hmul)
  67  exact this
  68
  69end Plateau
  70
  71/-!
  72## Stieltjes measure for `-w`
  73-/
  74
  75/-- The Stieltjes function `t ↦ -w(t)` built from an antitone, right-continuous `w`. -/
  76noncomputable def stieltjesNeg (w : ℝ → ℝ) (hw : Antitone w)
  77    (hw_rc : ∀ x, ContinuousWithinAt w (Ici x) x) :
  78    StieltjesFunction ℝ :=
  79  { toFun := fun x => -w x
  80    mono' := by
  81      intro x y hxy
  82      have : w y ≤ w x := hw hxy
  83      exact neg_le_neg this
  84    right_continuous' := by
  85      intro x
  86      simpa using (hw_rc x).neg }
  87
  88namespace stieltjesNeg
  89
  90variable {w : ℝ → ℝ} {hw : Antitone w} {hw_rc : ∀ x, ContinuousWithinAt w (Ici x) x}
  91
  92/-- The Stieltjes measure associated to `t ↦ -w(t)`. -/
  93noncomputable def μ : Measure ℝ :=
  94  (stieltjesNeg w hw hw_rc).measure
  95
  96lemma leftLim_neg_eq_neg_leftLim (w : ℝ → ℝ) (hw : Antitone w) (b : ℝ) :
  97    Function.leftLim (fun x => -w x) b = - Function.leftLim w b := by
  98  -- Antitone functions have left limits; use uniqueness of limits and continuity of `neg`.
  99  have hwlim : Tendsto w (𝓝[<] b) (nhds (Function.leftLim w b)) :=
 100    Antitone.tendsto_leftLim hw b
 101  have hne : (𝓝[<] b) ≠ (⊥ : Filter ℝ) := by
 102    haveI : NeBot (𝓝[<] b) := by infer_instance
 103    exact (neBot_iff.1 (by infer_instance))
 104  have hwlim' : Tendsto (fun x => -w x) (𝓝[<] b) (nhds (-Function.leftLim w b)) :=
 105    hwlim.neg
 106  exact leftLim_eq_of_tendsto (f := fun x => -w x) (a := b) hne hwlim'
 107
 108/-- Stieltjes mass on `Ioo a b` equals the phase drop `w a - leftLim w b` (as `ofReal`). -/
 109lemma measure_Ioo_eq_ofReal_drop (a b : ℝ) :
 110    (μ (w := w) (hw := hw) (hw_rc := hw_rc)) (Set.Ioo a b)
 111      = ENNReal.ofReal (w a - Function.leftLim w b) := by
 112  -- Start from the generic Stieltjes formula.
 113  let g : StieltjesFunction ℝ := stieltjesNeg w hw hw_rc
 114  have hIoo : g.measure (Set.Ioo a b) = ENNReal.ofReal (Function.leftLim g b - g a) := by
 115    simpa using (StieltjesFunction.measure_Ioo (f := g) (a := a) (b := b))
 116  -- Rewrite `g a = -w a` and `leftLim g b = - leftLim w b`.
 117  have hLL : Function.leftLim g b = - Function.leftLim w b := by
 118    -- `g = fun x ↦ -w x`
 119    simpa [g, stieltjesNeg] using (leftLim_neg_eq_neg_leftLim (w := w) hw b)
 120  -- Simplify the real expression.
 121  have : (Function.leftLim g b - g a) = (w a - Function.leftLim w b) := by
 122    have hga : g a = -w a := by
 123      simp [g, stieltjesNeg]
 124    calc
 125      Function.leftLim g b - g a = Function.leftLim g b - (-w a) := by simpa [hga]
 126      _ = (-Function.leftLim w b) - (-w a) := by simpa [hLL]
 127      _ = w a - Function.leftLim w b := by
 128        simp [sub_eq_add_neg, add_comm, add_left_comm, add_assoc]
 129  -- Finish.
 130  simpa [μ, g, hIoo, this]
 131
 132end stieltjesNeg
 133
 134/-!
 135## Oscillation control for antitone phases
 136-/
 137
 138/-- On a nontrivial interval, an antitone phase has essential oscillation controlled by the
 139endpoint drop `w a - leftLim w b`. -/
 140theorem oscOn_Icc_le_drop_of_antitone {w : ℝ → ℝ} (hw : Antitone w) {a b : ℝ} (hab : a < b) :
 141    oscOn w (Set.Icc a b) ≤ w a - Function.leftLim w b := by
 142  classical
 143  let μI : Measure ℝ := volume.restrict (Set.Icc a b)
 144  have hμI_pos : 0 < μI Set.univ := by
 145    -- `μI univ = volume (Icc a b) = ofReal (b-a)`, positive for `a<b`.
 146    simpa [μI, Real.volume_Icc, hab.ne', sub_pos.2 hab] using
 147      (ENNReal.ofReal_pos.2 (sub_pos.2 hab))
 148
 149  -- Upper bound on `essSup` via its `sInf` characterization.
 150  have hsup : essSup w μI ≤ w a := by
 151    -- Let `S := {c | μI {x | c < w x} = 0}`.
 152    let S : Set ℝ := {c : ℝ | μI {x : ℝ | c < w x} = 0}
 153    -- `S` is bounded below by `w b`: if `c < w b` then `{c < w x}` contains the whole interval,
 154    -- hence has positive measure.
 155    have hS_bdd : BddBelow S := by
 156      refine ⟨w b, ?_⟩
 157      intro c hc
 158      by_contra hcb
 159      have hcb' : c < w b := lt_of_not_ge hcb
 160      have hsubset : Set.Icc a b ⊆ {x : ℝ | c < w x} := by
 161        intro x hx
 162        have : w b ≤ w x := hw hx.2
 163        exact lt_of_lt_of_le hcb' this
 164      have hpos : 0 < μI {x : ℝ | c < w x} := by
 165        have : 0 < μI (Set.Icc a b) := by
 166          -- `μI (Icc a b) = volume (Icc a b)` and is positive when `a<b`.
 167          simpa [μI, Real.volume_Icc, hab.ne', sub_pos.2 hab] using
 168            (ENNReal.ofReal_pos.2 (sub_pos.2 hab))
 169        -- `Icc a b ⊆ {c < w x}` gives positive measure of the larger set.
 170        exact lt_of_lt_of_le this (measure_mono hsubset)
 171      -- Contradiction with `c ∈ S`.
 172      exact (ne_of_gt hpos) (by simpa [S] using hc)
 173    -- `w a ∈ S` because `w a < w x` never happens on `Icc a b`.
 174    have hwa : (w a) ∈ S := by
 175      have hempty : ({x : ℝ | w a < w x} ∩ Set.Icc a b) = (∅ : Set ℝ) := by
 176        ext x; constructor
 177        · intro hx
 178          rcases hx with ⟨hx1, hx2⟩
 179          have : w x ≤ w a := hw hx2.1
 180          exact (not_lt_of_ge this hx1).elim
 181        · intro hx; simpa using hx
 182      have : μI {x : ℝ | w a < w x} = 0 := by
 183        -- `μI s = volume (s ∩ Icc a b)` and the intersection is empty.
 184        simp [μI, Measure.restrict_apply' (hs := measurableSet_Icc), hempty]
 185      simpa [S] using this
 186    -- Now apply `essSup_eq_sInf` and the conditional `csInf_le`.
 187    rw [essSup_eq_sInf (μ := μI) (f := w)]
 188    -- goal: `sInf S ≤ w a`
 189    -- `S` is bounded below and nonempty, so we can use `csInf_le`.
 190    simpa [S] using (csInf_le hS_bdd hwa)
 191
 192  -- Lower bound on `essInf` via its `sSup` characterization.
 193  have hinf : Function.leftLim w b ≤ essInf w μI := by
 194    let T : Set ℝ := {c : ℝ | μI {x : ℝ | w x < c} = 0}
 195    -- `T` is bounded above by `w a`.
 196    have hT_bdd : BddAbove T := by
 197      refine ⟨w a, ?_⟩
 198      intro c hc
 199      by_contra hac
 200      have hac' : w a < c := lt_of_not_ge hac
 201      have hsubset : Set.Icc a b ⊆ {x : ℝ | w x < c} := by
 202        intro x hx
 203        have : w x ≤ w a := hw hx.1
 204        exact lt_of_le_of_lt this hac'
 205      have hpos : 0 < μI {x : ℝ | w x < c} := by
 206        have : 0 < μI (Set.Icc a b) := by
 207          simpa [μI, Real.volume_Icc, hab.ne', sub_pos.2 hab] using
 208            (ENNReal.ofReal_pos.2 (sub_pos.2 hab))
 209        exact lt_of_lt_of_le this (measure_mono hsubset)
 210      exact (ne_of_gt hpos) (by simpa [T] using hc)
 211    -- `leftLim w b ∈ T` because `{w x < leftLim w b}` can only occur at the endpoint `b`,
 212    -- which is a null set for Lebesgue.
 213    have hLL : (Function.leftLim w b) ∈ T := by
 214      have hsubset : ({x : ℝ | w x < Function.leftLim w b} ∩ Set.Icc a b) ⊆ ({b} : Set ℝ) := by
 215        intro x hx
 216        rcases hx with ⟨hxlt, hxab⟩
 217        have hxle : x ≤ b := hxab.2
 218        by_contra hxb
 219        have hxb' : x < b := lt_of_le_of_ne hxle hxb
 220        have : Function.leftLim w b ≤ w x := Antitone.leftLim_le (hf := hw) hxb'
 221        exact (not_lt_of_ge this hxlt).elim
 222      have : μI {x : ℝ | w x < Function.leftLim w b} = 0 := by
 223        -- Expand the restricted measure: `μI s = volume (s ∩ Icc a b)`.
 224        have hb : volume ({b} : Set ℝ) = 0 := by simp
 225        have hle :
 226            volume ({x : ℝ | w x < Function.leftLim w b} ∩ Set.Icc a b) ≤ volume ({b} : Set ℝ) :=
 227          measure_mono hsubset
 228        have hzero : volume ({x : ℝ | w x < Function.leftLim w b} ∩ Set.Icc a b) = 0 :=
 229          le_antisymm (le_trans hle (by simpa [hb])) (by simp)
 230        -- Convert back to `μI`.
 231        simpa [μI, Measure.restrict_apply' (hs := measurableSet_Icc), Set.inter_assoc,
 232          Set.inter_left_comm, Set.inter_comm] using hzero
 233      simpa [T] using this
 234    -- Apply `essInf_eq_sSup` and `le_csSup`.
 235    rw [essInf_eq_sSup (μ := μI) (f := w)]
 236    -- goal: `leftLim w b ≤ sSup T`
 237    simpa [T] using (le_csSup hT_bdd hLL)
 238
 239  -- Combine into the oscillation bound.
 240  dsimp [oscOn]
 241  nlinarith [hsup, hinf]
 242
 243/-!
 244## From a Stieltjes mass bound to an `oscOn` bound
 245-/
 246
 247/-- If the Stieltjes mass of `t ↦ -w(t)` on `Ioo a b` is at most `π·Υ`, then the essential
 248oscillation of `w` on `Icc a b` is at most `π·Υ`. -/
 249theorem oscOn_Icc_le_pi_mul_of_stieltjes_Ioo_bound
 250    {w : ℝ → ℝ} (hw : Antitone w) (hw_rc : ∀ x, ContinuousWithinAt w (Ici x) x)
 251    {a b Υ : ℝ} (hab : a < b) (hΥ : 0 ≤ Υ)
 252    (hμ :
 253      (stieltjesNeg.μ (w := w) (hw := hw) (hw_rc := hw_rc)) (Set.Ioo a b)
 254        ≤ ENNReal.ofReal (Real.pi * Υ)) :
 255    oscOn w (Set.Icc a b) ≤ Real.pi * Υ := by
 256  have hoscle : oscOn w (Set.Icc a b) ≤ w a - Function.leftLim w b :=
 257    oscOn_Icc_le_drop_of_antitone (w := w) hw hab
 258  have hdrop : w a - Function.leftLim w b ≤ Real.pi * Υ := by
 259    have hnonneg : 0 ≤ Real.pi * Υ := mul_nonneg (le_of_lt Real.pi_pos) hΥ
 260    have hmass :
 261        ENNReal.ofReal (w a - Function.leftLim w b) ≤ ENNReal.ofReal (Real.pi * Υ) := by
 262      -- rewrite the LHS using the Stieltjes drop formula
 263      simpa [stieltjesNeg.measure_Ioo_eq_ofReal_drop (w := w) (hw := hw) (hw_rc := hw_rc) a b]
 264        using hμ
 265    exact (ENNReal.ofReal_le_ofReal_iff hnonneg).1 hmass
 266  exact le_trans hoscle hdrop
 267
 268/-!
 269## B1: window bound + plateau ⇒ `oscOn` bound
 270
 271This is the “plateau/mass-extraction” bridge: if a window `φ` is bounded below by `c>0` on
 272`Ioo a b`, and `∫ φ dμ ≤ D`, then `μ(Ioo a b) ≤ D / c`. For the Stieltjes measure `μ = d(-w)`,
 273this yields an `oscOn` bound on `Icc a b`.
 274-/
 275
 276theorem oscOn_Icc_le_div_of_window_lintegral_bound
 277    {w : ℝ → ℝ} (hw : Antitone w) (hw_rc : ∀ x, ContinuousWithinAt w (Ici x) x)
 278    {a b D c : ℝ} (hab : a < b) (hD : 0 ≤ D) (hc : 0 < c)
 279    {φ : ℝ → ℝ≥0∞}
 280    (hφ_lower : ∀ t, t ∈ Set.Ioo a b → ENNReal.ofReal c ≤ φ t)
 281    (hlin : ∫⁻ t, φ t ∂(stieltjesNeg.μ (w := w) (hw := hw) (hw_rc := hw_rc))
 282              ≤ ENNReal.ofReal D) :
 283    oscOn w (Set.Icc a b) ≤ D / c := by
 284  have hc0 : (ENNReal.ofReal c) ≠ 0 := by
 285    have : 0 < ENNReal.ofReal c := (ENNReal.ofReal_pos.2 hc)
 286    exact (ne_of_gt this)
 287  have hcTop : (ENNReal.ofReal c) ≠ ⊤ := ENNReal.ofReal_ne_top
 288  -- Mass extraction: `μ(Ioo a b) ≤ (∫ φ dμ) / c`.
 289  have hmass₁ :
 290      (stieltjesNeg.μ (w := w) (hw := hw) (hw_rc := hw_rc)) (Set.Ioo a b)
 291        ≤ (∫⁻ t, φ t ∂(stieltjesNeg.μ (w := w) (hw := hw) (hw_rc := hw_rc))) /
 292            (ENNReal.ofReal c) := by
 293    exact Plateau.measure_le_lintegral_div_of_forall_le_on
 294      (μ := stieltjesNeg.μ (w := w) (hw := hw) (hw_rc := hw_rc))
 295      (s := Set.Ioo a b) measurableSet_Ioo hc0 hcTop hφ_lower
 296  have hmass₂ :
 297      (stieltjesNeg.μ (w := w) (hw := hw) (hw_rc := hw_rc)) (Set.Ioo a b)
 298        ≤ ENNReal.ofReal (D / c) := by
 299    -- Combine the mass extraction with the lintegral bound and rewrite `ofReal (D / c)`.
 300    have hnonneg_c : 0 < c := hc
 301    have hnonneg_Dc : 0 ≤ D / c := by exact div_nonneg hD (le_of_lt hc)
 302    have : (∫⁻ t, φ t ∂(stieltjesNeg.μ (w := w) (hw := hw) (hw_rc := hw_rc))) / ENNReal.ofReal c
 303        ≤ ENNReal.ofReal D / ENNReal.ofReal c := by
 304      exact ENNReal.div_le_div_right hlin (ENNReal.ofReal c)
 305    have hrewrite : ENNReal.ofReal (D / c) = ENNReal.ofReal D / ENNReal.ofReal c := by
 306      simpa using (ENNReal.ofReal_div_of_pos (x := D) (y := c) hnonneg_c)
 307    have : (stieltjesNeg.μ (w := w) (hw := hw) (hw_rc := hw_rc)) (Set.Ioo a b)
 308        ≤ ENNReal.ofReal D / ENNReal.ofReal c := le_trans hmass₁ this
 309    simpa [hrewrite] using this
 310  -- Convert `μ(Ioo) ≤ ofReal(D/c)` into `oscOn ≤ D/c` using the already-proved drop bound.
 311  have hoscle : oscOn w (Set.Icc a b) ≤ w a - Function.leftLim w b :=
 312    oscOn_Icc_le_drop_of_antitone (w := w) hw hab
 313  have hdrop : w a - Function.leftLim w b ≤ D / c := by
 314    have hnonneg : 0 ≤ D / c := div_nonneg hD (le_of_lt hc)
 315    have hmass :
 316        ENNReal.ofReal (w a - Function.leftLim w b) ≤ ENNReal.ofReal (D / c) := by
 317      simpa [stieltjesNeg.measure_Ioo_eq_ofReal_drop (w := w) (hw := hw) (hw_rc := hw_rc) a b]
 318        using hmass₂
 319    exact (ENNReal.ofReal_le_ofReal_iff hnonneg).1 hmass
 320  exact le_trans hoscle hdrop
 321
 322end RiemannHypothesis
 323end NumberTheory
 324end IndisputableMonolith
 325