IndisputableMonolith.NumberTheory.RiemannHypothesis.Wedge

   1import IndisputableMonolith.NumberTheory.RiemannHypothesis.BRFPlumbing
   2
   3/-!
   4# Riemann Hypothesis (BRF route): boundary wedge → positivity
   5
   6In `docs/primes/Riemann-proofs/Riemann-active.txt`, the load-bearing boundary condition (P+)
   7asserts that after a unimodular rotation, the boundary phase `w(t)` is confined to a wedge:
   8
   9`|w(t)| ≤ π·Υ` with `Υ < 1/2` almost everywhere.
  10
  11This file records the simple but crucial algebraic consequence:
  12
  13`|w| ≤ π/2  ⇒  Re(exp(i w)) ≥ 0`,
  14
  15which is the “entry point” for Poisson transport + the Cayley transform.
  16-/
  17
  18namespace IndisputableMonolith
  19namespace NumberTheory
  20namespace RiemannHypothesis
  21
  22open scoped Real
  23open MeasureTheory
  24
  25/-- The unimodular complex number with phase `w`: `e^{i w}`. -/
  26noncomputable def phase (w : ℝ) : ℂ :=
  27  Complex.exp (w * Complex.I)
  28
  29theorem re_phase_nonneg_of_abs_le_pi_div_two {w : ℝ} (hw : |w| ≤ Real.pi / 2) :
  30    0 ≤ (phase w).re := by
  31  -- `Re(e^{iw}) = cos(w)` and `cos(w) ≥ 0` on `[-π/2, π/2]`.
  32  have hw' : w ∈ Set.Icc (-(Real.pi / 2)) (Real.pi / 2) := by
  33    exact abs_le.mp (by simpa [abs_neg] using hw)
  34  -- `Complex.exp_ofReal_mul_I_re` rewrites the real part into `Real.cos`.
  35  simpa [phase] using (Real.cos_nonneg_of_mem_Icc hw')
  36
  37/-- Almost-everywhere version: a wedge bound implies nonnegativity of the real part of the phase. -/
  38theorem ae_re_phase_nonneg_of_ae_abs_le_pi_mul
  39    {w : ℝ → ℝ} {Υ : ℝ}
  40    (hΥ : Υ ≤ (1 / 2 : ℝ))
  41    (hw : ∀ᵐ t ∂volume, |w t| ≤ Real.pi * Υ) :
  42    ∀ᵐ t ∂volume, 0 ≤ (phase (w t)).re := by
  43  have hpi : Real.pi * Υ ≤ Real.pi / 2 := by
  44    have hpi0 : 0 ≤ Real.pi := le_of_lt Real.pi_pos
  45    -- multiply `Υ ≤ 1/2` by `π ≥ 0`
  46    have := mul_le_mul_of_nonneg_left hΥ hpi0
  47    -- `π * (1/2) = π/2`
  48    simpa [div_eq_mul_inv, mul_assoc, mul_left_comm, mul_comm] using this
  49  filter_upwards [hw] with t ht
  50  exact re_phase_nonneg_of_abs_le_pi_div_two (le_trans ht hpi)
  51
  52/-- If the boundary wedge holds for `w` with parameter `Υ ≤ 1/2`, then the Cayley/BRF transform
  53`θ(J)=(2J-1)/(2J+1)` is Schur pointwise for the boundary values `J(t)=e^{iw(t)}`. -/
  54theorem ae_norm_theta_phase_le_one_of_ae_abs_le_pi_mul
  55    {w : ℝ → ℝ} {Υ : ℝ}
  56    (hΥ : Υ ≤ (1 / 2 : ℝ))
  57    (hw : ∀ᵐ t ∂volume, |w t| ≤ Real.pi * Υ) :
  58    ∀ᵐ t ∂volume, ‖theta (phase (w t))‖ ≤ 1 := by
  59  -- From the wedge we get `Re(J) ≥ 0`. Then apply the Cayley lemma.
  60  have hRe : ∀ᵐ t ∂volume, 0 ≤ (phase (w t)).re :=
  61    ae_re_phase_nonneg_of_ae_abs_le_pi_mul (w := w) (Υ := Υ) hΥ hw
  62  filter_upwards [hRe] with t ht
  63  exact norm_theta_le_one_of_re_nonneg (J := phase (w t)) ht
  64
  65end RiemannHypothesis
  66end NumberTheory
  67end IndisputableMonolith
  68