IndisputableMonolith.NumberTheory.RiemannHypothesis.LocalToGlobalWedge

   1import IndisputableMonolith.NumberTheory.RiemannHypothesis.Wedge
   2
   3/-!
   4# Riemann Hypothesis (BRF route): local-to-global wedge lemma
   5
   6This file formalizes the abstract “local-to-global wedge” step appearing as
   7Lemma `local-to-global-wedge` in `docs/primes/Riemann-proofs/Riemann-active.txt`.
   8
   9In the manuscript, one bounds the **essential oscillation** of a boundary phase `w(t)` on a
  10Whitney/dyadic schedule of intervals. After a unimodular rotation (i.e. subtracting a constant
  11phase), this yields an a.e. wedge bound `|w(t)| ≤ π·Υ`.
  12
  13We implement a clean measure-theoretic core:
  14
  15- Define the oscillation on a set `s` as `essSup - essInf` w.r.t. Lebesgue measure restricted to `s`.
  16- If this oscillation is uniformly bounded on a nested exhaustion `[-n,n]`, then there exists a
  17  constant `c` (the “rotation”) such that `|w(t) - c| ≤ D` a.e. on `ℝ`.
  18
  19This is the exact reusable interface we want: analytic work supplies the oscillation bound; this
  20lemma turns it into the wedge bound needed for the Poisson/Cayley step.
  21-/
  22
  23namespace IndisputableMonolith
  24namespace NumberTheory
  25namespace RiemannHypothesis
  26
  27open scoped Real
  28open MeasureTheory Filter
  29
  30/-!
  31## Essential oscillation on a set
  32-/
  33
  34/-- Essential oscillation of `w` on a set `s`, with respect to Lebesgue measure:
  35`oscOn w s = essSup(w|_s) - essInf(w|_s)`. -/
  36noncomputable def oscOn (w : ℝ → ℝ) (s : Set ℝ) : ℝ :=
  37  essSup w (volume.restrict s) - essInf w (volume.restrict s)
  38
  39lemma essInf_le_essSup_of_neZero {w : ℝ → ℝ} {μ : Measure ℝ} (hμ : μ ≠ 0)
  40    (hupper : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (ae μ) w)
  41    (hlower : IsBoundedUnder (fun x1 x2 => x1 ≥ x2) (ae μ) w) :
  42    essInf w μ ≤ essSup w μ := by
  43  have hae :
  44      (∀ᵐ x ∂μ, essInf w μ ≤ essSup w μ) := by
  45    -- combine the pointwise a.e. bounds `essInf ≤ w ≤ essSup`.
  46    filter_upwards [ae_essInf_le (μ := μ) (f := w) hlower,
  47      ae_le_essSup (μ := μ) (f := w) hupper] with x hx1 hx2
  48    exact le_trans hx1 hx2
  49  by_contra h
  50  have : μ Set.univ = 0 := by
  51    -- If the constant inequality is false, its negation holds everywhere; but `hae` says its
  52    -- negation has measure zero.
  53    have : μ {x : ℝ | ¬ (essInf w μ ≤ essSup w μ)} = 0 := by
  54      simpa [MeasureTheory.ae_iff] using hae
  55    simpa [h] using this
  56  exact hμ ((Measure.measure_univ_eq_zero).1 this)
  57
  58/-!
  59## Local oscillation on an exhaustion implies a global wedge after rotation
  60-/
  61
  62/-- **Core local-to-global wedge lemma**.
  63
  64Assume the essential oscillation of `w` on the symmetric intervals `[-(n+1), (n+1)]`
  65is bounded by `D`. Then there exists a constant `c` (corresponding to a unimodular rotation)
  66such that `|w(t) - c| ≤ D` almost everywhere on `ℝ`. -/
  67theorem exists_shift_ae_abs_sub_le_of_oscOn_Icc_exhaustion
  68    {w : ℝ → ℝ} {D : ℝ}
  69    (hupper : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (ae volume) w)
  70    (hlower : IsBoundedUnder (fun x1 x2 => x1 ≥ x2) (ae volume) w)
  71    (hosc : ∀ n : ℕ, oscOn w (Set.Icc (-(n.succ : ℝ)) (n.succ : ℝ)) ≤ D) :
  72    ∃ c : ℝ, ∀ᵐ t ∂volume, |w t - c| ≤ D := by
  73  classical
  74  -- Base interval `[-1,1]`.
  75  let I0 : Set ℝ := Set.Icc (- (1 : ℝ)) (1 : ℝ)
  76  let μ0 : Measure ℝ := volume.restrict I0
  77
  78  have hμ0 : μ0 ≠ 0 := by
  79    -- `μ0 univ = volume I0 = 2`.
  80    have hU : μ0 Set.univ = (2 : ENNReal) := by
  81      simp [μ0, I0, Real.volume_Icc]
  82      norm_num
  83    have : μ0 Set.univ ≠ 0 := by
  84      simp [hU]
  85    exact (Measure.measure_univ_ne_zero).1 this
  86
  87  -- `ae μ0` is nontrivial since `μ0 ≠ 0`. This is needed for coboundedness lemmas.
  88  haveI : NeBot (ae μ0) := (ae_neBot.2 hμ0)
  89
  90  let a0 : ℝ := essInf w μ0
  91  let b0 : ℝ := essSup w μ0
  92
  93  -- Boundedness on the restricted measure `μ0`, inherited from the global phase boundedness.
  94  have hupper0 : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (ae μ0) w := by
  95    rcases hupper with ⟨B, hB⟩
  96    refine ⟨B, ?_⟩
  97    -- `μ0 ≪ volume`, so a.e. under `volume` implies a.e. under `μ0`.
  98    have hle : ae μ0 ≤ ae volume :=
  99      (Measure.ae_le_iff_absolutelyContinuous).2 Measure.absolutelyContinuous_restrict
 100    exact hB.filter_mono hle
 101  have hlower0 : IsBoundedUnder (fun x1 x2 => x1 ≥ x2) (ae μ0) w := by
 102    rcases hlower with ⟨B, hB⟩
 103    refine ⟨B, ?_⟩
 104    have hle : ae μ0 ≤ ae volume :=
 105      (Measure.ae_le_iff_absolutelyContinuous).2 Measure.absolutelyContinuous_restrict
 106    exact hB.filter_mono hle
 107
 108  have hab : a0 ≤ b0 :=
 109    essInf_le_essSup_of_neZero (w := w) (μ := μ0) hμ0 hupper0 hlower0
 110
 111  -- Choose the “rotation” constant as the midpoint of `[a0,b0]`.
 112  let c : ℝ := (a0 + b0) / 2
 113  refine ⟨c, ?_⟩
 114
 115  -- Step 1: show the bound on each restricted measure `volume.restrict [-N,N]`.
 116  have h_on : ∀ n : ℕ,
 117      (∀ᵐ t ∂volume.restrict (Set.Icc (-(n.succ : ℝ)) (n.succ : ℝ)), |w t - c| ≤ D) := by
 118    intro n
 119    let In : Set ℝ := Set.Icc (-(n.succ : ℝ)) (n.succ : ℝ)
 120    let μn : Measure ℝ := volume.restrict In
 121
 122    -- Monotonicity of `essSup`/`essInf` from `I0 ⊆ In` (since `n.succ ≥ 1`).
 123    have hI0n : I0 ⊆ In := by
 124      intro x hx
 125      rcases hx with ⟨hxL, hxU⟩
 126      have hn : (1 : ℝ) ≤ (n.succ : ℝ) := by
 127        exact_mod_cast (Nat.succ_le_succ (Nat.zero_le n))
 128      constructor
 129      · -- `-(n.succ) ≤ x` from `-1 ≤ x` and `-(n.succ) ≤ -1`.
 130        have : (-(n.succ : ℝ)) ≤ -(1 : ℝ) := by nlinarith [hn]
 131        exact le_trans this hxL
 132      · exact le_trans hxU hn
 133
 134    -- First, inherit boundedness/coboundedness for `w` on `μn` from the global bounds.
 135    have huppern : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (ae μn) w := by
 136      rcases hupper with ⟨B, hB⟩
 137      refine ⟨B, ?_⟩
 138      have hle : ae μn ≤ ae volume :=
 139        (Measure.ae_le_iff_absolutelyContinuous).2 Measure.absolutelyContinuous_restrict
 140      exact hB.filter_mono hle
 141    have hlowern : IsBoundedUnder (fun x1 x2 => x1 ≥ x2) (ae μn) w := by
 142      rcases hlower with ⟨B, hB⟩
 143      refine ⟨B, ?_⟩
 144      have hle : ae μn ≤ ae volume :=
 145        (Measure.ae_le_iff_absolutelyContinuous).2 Measure.absolutelyContinuous_restrict
 146      exact hB.filter_mono hle
 147
 148    have hAE : ae μ0 ≤ ae μn := by
 149      have hleμ : μ0 ≤ μn := Measure.restrict_mono hI0n le_rfl
 150      have hac : μ0 ≪ μn := Measure.absolutelyContinuous_of_le hleμ
 151      exact (Measure.ae_le_iff_absolutelyContinuous).2 hac
 152
 153    -- `b0 ≤ essSup w μn` from monotonicity of `limsup` along `ae` filters.
 154    have hb0_le : b0 ≤ essSup w μn := by
 155      -- `essSup` is `limsup` along `ae`.
 156      -- Apply `limsup_le_limsup_of_le` with bounds inherited from boundedness on `μn`/`μ0`.
 157      have hCobdd0 : (ae μ0).IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) w :=
 158        hlower0.isCoboundedUnder_le
 159      have hBddn : (ae μn).IsBoundedUnder (fun x1 x2 => x1 ≤ x2) w :=
 160        huppern
 161      simpa [b0, essSup] using (limsup_le_limsup_of_le (h := hAE) (u := w) hCobdd0 hBddn)
 162
 163    -- `essInf w μn ≤ a0` from monotonicity of `liminf` along `ae` filters.
 164    have ha_le : essInf w μn ≤ a0 := by
 165      have hBddn : (ae μn).IsBoundedUnder (fun x1 x2 => x1 ≥ x2) w :=
 166        hlowern
 167      have hCobdd0 : (ae μ0).IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) w :=
 168        hupper0.isCoboundedUnder_ge
 169      -- With `hAE : ae μ0 ≤ ae μn`, we have `liminf w (ae μn) ≤ liminf w (ae μ0)`.
 170      simpa [a0, essInf] using
 171        (liminf_le_liminf_of_le (h := hAE) (u := w) hBddn hCobdd0)
 172
 173    have hc_lower : essInf w μn ≤ c := by
 174      have : a0 ≤ c := by
 175        dsimp [c]
 176        nlinarith [hab]
 177      exact le_trans ha_le this
 178    have hc_upper : c ≤ essSup w μn := by
 179      have : c ≤ b0 := by
 180        dsimp [c]
 181        nlinarith [hab]
 182      exact le_trans this hb0_le
 183
 184    -- For a.e. `t` in `In`, we have `essInf ≤ w t ≤ essSup`.
 185    have hlow : ∀ᵐ t ∂μn, essInf w μn ≤ w t :=
 186      ae_essInf_le (μ := μn) (f := w) hlowern
 187    have hupp : ∀ᵐ t ∂μn, w t ≤ essSup w μn :=
 188      ae_le_essSup (μ := μn) (f := w) huppern
 189
 190    -- Now bound the distance to `c` by the diameter `essSup-essInf ≤ D`.
 191    have hdiam : essSup w μn - essInf w μn ≤ D := by
 192      simpa [oscOn, μn, In] using (hosc n)
 193
 194    filter_upwards [hlow, hupp] with t htL htU
 195    have h1 : w t - c ≤ essSup w μn - essInf w μn := by
 196      nlinarith [htU, hc_lower]
 197    have h2 : c - w t ≤ essSup w μn - essInf w μn := by
 198      nlinarith [htL, hc_upper]
 199    have habs : |w t - c| ≤ essSup w μn - essInf w μn :=
 200      (abs_sub_le_iff.2 ⟨h1, h2⟩)
 201    exact le_trans habs hdiam
 202
 203  -- Step 2: upgrade from each restricted interval to all of `ℝ` by countable union.
 204  have hbad0 :
 205      volume {t : ℝ | ¬ |w t - c| ≤ D} = 0 := by
 206    -- Let `Bad = {t | ¬ |w t - c| ≤ D}`.
 207    let Bad : Set ℝ := {t : ℝ | ¬ |w t - c| ≤ D}
 208    have hbad : ∀ n : ℕ, volume (Bad ∩ Set.Icc (-(n.succ : ℝ)) (n.succ : ℝ)) = 0 := by
 209      intro n
 210      let In : Set ℝ := Set.Icc (-(n.succ : ℝ)) (n.succ : ℝ)
 211      -- Turn the restricted a.e. statement into an a.e. implication on `volume`.
 212      have hn : ∀ᵐ t ∂volume, t ∈ In → |w t - c| ≤ D :=
 213        ae_imp_of_ae_restrict (μ := volume) (s := In) (p := fun t => |w t - c| ≤ D) (h_on n)
 214      -- Convert the implication to a measure-zero statement on `Bad ∩ In`.
 215      have : volume {t : ℝ | t ∈ In ∧ D < |w t - c|} = 0 := by
 216        -- `¬ (t ∈ In → P)` is `t ∈ In ∧ ¬P`, and `¬(|w-c| ≤ D)` is `D < |w-c|`.
 217        simpa [MeasureTheory.ae_iff, _root_.not_imp, not_le, and_left_comm, and_assoc, and_comm] using hn
 218      -- Rewrite `{t | t ∈ In ∧ D < |w-c|}` as `Bad ∩ In`.
 219      have hset : {t : ℝ | t ∈ In ∧ D < |w t - c|} = Bad ∩ In := by
 220        ext t
 221        simp [Bad, In, not_le, and_assoc, and_comm]
 222      have hBadIn : volume (Bad ∩ In) = 0 := by
 223        simpa [hset] using this
 224      simpa [In, Set.inter_assoc, Set.inter_comm, Set.inter_left_comm] using hBadIn
 225    have hBad_eq : Bad = ⋃ n : ℕ, Bad ∩ Set.Icc (-(n.succ : ℝ)) (n.succ : ℝ) := by
 226      ext t; constructor
 227      · intro ht
 228        obtain ⟨N, hN⟩ := exists_nat_ge (|t|)
 229        refine Set.mem_iUnion.2 ?_
 230        refine ⟨N, ?_⟩
 231        have hN' : |t| ≤ (N.succ : ℝ) := le_trans hN (by exact_mod_cast (Nat.le_succ N))
 232        refine ⟨ht, (abs_le.mp hN')⟩
 233      · intro ht
 234        rcases Set.mem_iUnion.1 ht with ⟨n, hn⟩
 235        exact hn.1
 236    -- measure of the union is zero.
 237    have hUnion : volume (⋃ n : ℕ, Bad ∩ Set.Icc (-(n.succ : ℝ)) (n.succ : ℝ)) = 0 :=
 238      measure_iUnion_null hbad
 239    have hBad : volume Bad = 0 := by
 240      -- Avoid `simp` rewriting `Bad` recursively (since `hBad_eq` has `Bad` on both sides).
 241      have hvol_eq : volume Bad = volume (⋃ n : ℕ, Bad ∩ Set.Icc (-(n.succ : ℝ)) (n.succ : ℝ)) := by
 242        simpa using congrArg (fun s : Set ℝ => volume s) hBad_eq
 243      simpa [hvol_eq] using hUnion
 244    simpa [Bad] using hBad
 245
 246  -- Convert the measure statement to an `ae` statement.
 247  simpa [MeasureTheory.ae_iff] using hbad0
 248
 249/-- A paper-friendly wrapper: if the oscillation on *all centered intervals* is bounded by `D`,
 250then (after rotation) `|w-c| ≤ D` almost everywhere. -/
 251theorem exists_shift_ae_abs_sub_le_of_forall_centered_oscOn
 252    {w : ℝ → ℝ} {D : ℝ}
 253    (hupper : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (ae volume) w)
 254    (hlower : IsBoundedUnder (fun x1 x2 => x1 ≥ x2) (ae volume) w)
 255    (hosc : ∀ L : ℝ, 0 < L → oscOn w (Set.Icc (-L) L) ≤ D) :
 256    ∃ c : ℝ, ∀ᵐ t ∂volume, |w t - c| ≤ D := by
 257  -- Apply the exhaustion lemma with `L = n+1`.
 258  refine exists_shift_ae_abs_sub_le_of_oscOn_Icc_exhaustion (w := w) (D := D) hupper hlower ?_
 259  intro n
 260  simpa using (hosc (n.succ : ℝ) (by exact_mod_cast (Nat.succ_pos n)))
 261
 262/-- Specialization to the RH wedge parameter: if oscillation on centered intervals is bounded by
 263`π·Υ`, then after rotation we have the a.e. wedge `|w-c| ≤ π·Υ`. -/
 264theorem exists_shift_ae_abs_sub_le_pi_mul_of_forall_centered_oscOn
 265    {w : ℝ → ℝ} {Υ : ℝ}
 266    (hupper : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (ae volume) w)
 267    (hlower : IsBoundedUnder (fun x1 x2 => x1 ≥ x2) (ae volume) w)
 268    (hosc : ∀ L : ℝ, 0 < L → oscOn w (Set.Icc (-L) L) ≤ Real.pi * Υ) :
 269    ∃ c : ℝ, ∀ᵐ t ∂volume, |w t - c| ≤ Real.pi * Υ := by
 270  exact exists_shift_ae_abs_sub_le_of_forall_centered_oscOn (w := w) (D := Real.pi * Υ) hupper
 271    hlower hosc
 272
 273end RiemannHypothesis
 274end NumberTheory
 275end IndisputableMonolith
 276