IndisputableMonolith.NumberTheory.RiemannHypothesis.AttachmentWithMargin

   1import IndisputableMonolith.NumberTheory.RiemannHypothesis.BRFPlumbing
   2
   3/-!
   4# RH (Christmas route): quantitative attachment with margin
   5
   6`Riemann-Christmas.tex` isolates the far-field remaining gap as the **attachment-with-margin**
   7inequality (equation `eq:attachment`):
   8
   9`sup_{s ∈ R} |J_N(s) - J_cert,N(s)| ≤ m_R / 4`, where `m_R := inf_{s ∈ R} Re(2 J_cert,N(s))`.
  10
  11This file formalizes the *purely algebraic* consequence:
  12
  13`(attachment-with-margin) ⇒ Re(2 J_N) ≥ 0` (hence the Cayley transform is Schur),
  14
  15without touching any number theory. The analytic difficulty is entirely in proving the
  16uniform approximation bound itself.
  17-/
  18
  19namespace IndisputableMonolith
  20namespace NumberTheory
  21namespace RiemannHypothesis
  22
  23open scoped Real
  24
  25/-!
  26## One-step algebra: approximation within margin ⇒ Herglotz/Schur on a set
  27-/
  28
  29/-- The **Christmas-route attachment-with-margin** predicate on a set `R`.
  30
  31This is the one-line analytic gap from `Riemann-Christmas.tex` (`eq:attachment`), expressed
  32pointwise (which is implied by the `sup` version).
  33-/
  34def AttachmentWithMargin (R : Set ℂ) (J Jcert : ℂ → ℂ) (m : ℝ) : Prop :=
  35  0 ≤ m ∧ (∀ s ∈ R, m ≤ (2 * Jcert s).re) ∧ (∀ s ∈ R, ‖J s - Jcert s‖ ≤ m / 4)
  36
  37/-- A convenient “budget form”: it suffices to bound the uniform approximation error by a
  38sum of nonnegative budgets `Etail + Ewin` and then check `Etail + Ewin ≤ m/4`. -/
  39theorem attachmentWithMargin_of_errorBudget
  40    {R : Set ℂ} {J Jcert : ℂ → ℂ} {m Etail Ewin : ℝ}
  41    (hm_nonneg : 0 ≤ m)
  42    (hmargin : ∀ s ∈ R, m ≤ (2 * Jcert s).re)
  43    (herr : ∀ s ∈ R, ‖J s - Jcert s‖ ≤ Etail + Ewin)
  44    (hbudget : Etail + Ewin ≤ m / 4) :
  45    AttachmentWithMargin R J Jcert m := by
  46  refine ⟨hm_nonneg, hmargin, ?_⟩
  47  intro s hs
  48  exact (herr s hs).trans hbudget
  49
  50/-- **Quantitative attachment with margin** (algebraic core).
  51
  52Let `Jcert` be a "certificate" function and `J` an approximant. If, on a set `R`,
  53
  54- `Re(2*Jcert)` is bounded below by a nonnegative margin `m`, and
  55- `J` stays within `m/4` (in norm) of `Jcert`,
  56
  57then `Re(2*J) ≥ 0` on `R`.
  58
  59This is the Lean analogue of `Riemann-Christmas.tex`, Lemma `attachment-identity`
  60(the step after equation `eq:attachment` is assumed).
  61-/
  62theorem re_two_mul_nonneg_of_attachmentWithMargin
  63    {R : Set ℂ} {J Jcert : ℂ → ℂ} {m : ℝ}
  64    (hm_nonneg : 0 ≤ m)
  65    (hmargin : ∀ s ∈ R, m ≤ (2 * Jcert s).re)
  66    (hclose : ∀ s ∈ R, ‖J s - Jcert s‖ ≤ m / 4) :
  67    ∀ s ∈ R, 0 ≤ (2 * J s).re := by
  68  intro s hs
  69  have hJcert : m ≤ (2 * Jcert s).re := hmargin s hs
  70  have hdiff : ‖J s - Jcert s‖ ≤ m / 4 := hclose s hs
  71
  72  -- Control the real part of the perturbation by its norm.
  73  have hAbsRe :
  74      |(2 * (J s - Jcert s)).re| ≤ ‖2 * (J s - Jcert s)‖ :=
  75    Complex.abs_re_le_norm _
  76  have hRe_lower :
  77      -‖2 * (J s - Jcert s)‖ ≤ (2 * (J s - Jcert s)).re :=
  78    (abs_le.mp hAbsRe).1
  79
  80  -- Convert `‖2 * (J-Jcert)‖` into `2 * ‖J-Jcert‖` and use the `m/4` bound.
  81  have hnorm_two : ‖(2 : ℂ)‖ = (2 : ℝ) := by
  82    -- `‖(x:ℂ)‖ = |x|` for real `x`, and `|2|=2`.
  83    simp
  84  have hnorm_mul :
  85      ‖2 * (J s - Jcert s)‖ ≤ m / 2 := by
  86    -- `‖2 * z‖ = ‖2‖ * ‖z‖ = 2 * ‖z‖`.
  87    have hnorm :
  88        ‖2 * (J s - Jcert s)‖ = (2 : ℝ) * ‖J s - Jcert s‖ := by
  89      simpa [mul_assoc, hnorm_two] using
  90        (norm_mul (2 : ℂ) (J s - Jcert s))
  91    -- Multiply the `m/4` bound by `2`.
  92    have hmul : (2 : ℝ) * ‖J s - Jcert s‖ ≤ (2 : ℝ) * (m / 4) :=
  93      mul_le_mul_of_nonneg_left hdiff (by norm_num : (0 : ℝ) ≤ 2)
  94    -- `2 * (m/4) = m/2`
  95    have hmul_simp : (2 : ℝ) * (m / 4) = m / 2 := by ring
  96    -- Finish.
  97    -- Rewrite the left-hand side using `hnorm`, then close by `hmul` and `hmul_simp`.
  98    calc
  99      ‖2 * (J s - Jcert s)‖ = (2 : ℝ) * ‖J s - Jcert s‖ := hnorm
 100      _ ≤ (2 : ℝ) * (m / 4) := hmul
 101      _ = m / 2 := hmul_simp
 102
 103  -- Now bound the target real part:
 104  --   Re(2J) = Re(2Jcert) + Re(2(J-Jcert)) ≥ m - ‖2(J-Jcert)‖ ≥ m/2 ≥ 0.
 105  have hRe2 :
 106      (2 * J s).re ≥ m - ‖2 * (J s - Jcert s)‖ := by
 107    -- `2*J = 2*Jcert + 2*(J-Jcert)`
 108    have hsplit : (2 * J s) = (2 * Jcert s) + (2 * (J s - Jcert s)) := by
 109      ring
 110    -- Take real parts and use the perturbation lower bound.
 111    -- `re(a+b) = re(a) + re(b)`
 112    have : (2 * J s).re = (2 * Jcert s).re + (2 * (J s - Jcert s)).re := by
 113      simpa [hsplit, Complex.add_re]
 114    -- combine
 115    nlinarith [this, hJcert, hRe_lower]
 116
 117  have : (2 * J s).re ≥ m / 2 := by
 118    nlinarith [hRe2, hnorm_mul]
 119  have : 0 ≤ (2 * J s).re := by
 120    nlinarith [this, hm_nonneg]
 121  simpa using this
 122
 123/-- Wrapper: `AttachmentWithMargin` implies `Re(2*J) ≥ 0` on `R`. -/
 124theorem re_two_mul_nonneg_of_AttachmentWithMargin
 125    {R : Set ℂ} {J Jcert : ℂ → ℂ} {m : ℝ}
 126    (h : AttachmentWithMargin R J Jcert m) :
 127    ∀ s ∈ R, 0 ≤ (2 * J s).re := by
 128  rcases h with ⟨hm_nonneg, hmargin, hclose⟩
 129  exact re_two_mul_nonneg_of_attachmentWithMargin
 130    (R := R) (J := J) (Jcert := Jcert) (m := m) hm_nonneg hmargin hclose
 131
 132/-- Attachment-with-margin also yields the Schur (disk) bound for the Cayley transform `theta`. -/
 133theorem norm_theta_le_one_of_attachmentWithMargin
 134    {R : Set ℂ} {J Jcert : ℂ → ℂ} {m : ℝ}
 135    (hm_nonneg : 0 ≤ m)
 136    (hmargin : ∀ s ∈ R, m ≤ (2 * Jcert s).re)
 137    (hclose : ∀ s ∈ R, ‖J s - Jcert s‖ ≤ m / 4) :
 138    ∀ s ∈ R, ‖theta (J s)‖ ≤ 1 := by
 139  intro s hs
 140  have hRe : 0 ≤ (2 * J s).re :=
 141    re_two_mul_nonneg_of_attachmentWithMargin (R := R) (J := J) (Jcert := Jcert)
 142      (m := m) hm_nonneg hmargin hclose s hs
 143  -- Cayley: if `Re(2J) ≥ 0` then `‖cayley(2J)‖ ≤ 1`, i.e. `‖theta J‖ ≤ 1`.
 144  simpa [theta] using (norm_cayley_le_one_of_re_nonneg (z := 2 * J s) hRe)
 145
 146/-- Wrapper: `AttachmentWithMargin` implies the Schur bound `‖theta (J s)‖ ≤ 1` on `R`. -/
 147theorem norm_theta_le_one_of_AttachmentWithMargin
 148    {R : Set ℂ} {J Jcert : ℂ → ℂ} {m : ℝ}
 149    (h : AttachmentWithMargin R J Jcert m) :
 150    ∀ s ∈ R, ‖theta (J s)‖ ≤ 1 := by
 151  rcases h with ⟨hm_nonneg, hmargin, hclose⟩
 152  exact norm_theta_le_one_of_attachmentWithMargin
 153    (R := R) (J := J) (Jcert := Jcert) (m := m) hm_nonneg hmargin hclose
 154
 155end RiemannHypothesis
 156end NumberTheory
 157end IndisputableMonolith
 158