DiagonalNoisyRate.lean

1 import KomorebiSpace.InfiniteDiagonalModel
2 import KomorebiSpace.RegularizedHilbertRepair
3 import Mathlib.Analysis.SpecialFunctions.Pow.Real
4 import Mathlib.Analysis.Real.Sqrt
5 import Mathlib.Algebra.Order.Floor.Ring
6 import Mathlib.Tactic
7 
8 set_option autoImplicit false
9 noncomputable section
10 
11 namespace KomorebiSpace.DiagonalRegularization
12 
13 /-- The literal integer schedule in Corollary 30.3; the exponents are real. -/
14 def noiseSchedule (δ : ℝ) : ℕ := Nat.ceil (δ ^ (-(2 : ℝ) / 3))
15 
16 /-- Positivity of the noise level makes the chosen integer positive. -/
17 theorem noiseSchedule_pos {δ : ℝ} (hδ : 0 < δ) : 0 < noiseSchedule δ := by
18   exact Nat.ceil_pos.mpr (Real.rpow_pos_of_pos hδ _)
19 
20 theorem one_le_noiseSchedule {δ : ℝ} (hδ : 0 < δ) : 1 ≤ noiseSchedule δ :=
21   noiseSchedule_pos hδ
22 
23 private theorem noise_rpow_mul {δ : ℝ} (hδ : 0 < δ) :
24     δ * δ ^ (-(2 : ℝ) / 3) = δ ^ ((1 : ℝ) / 3) := by
25   calc
26     δ * δ ^ (-(2 : ℝ) / 3) =
27         δ ^ (1 : ℝ) * δ ^ (-(2 : ℝ) / 3) := by rw [Real.rpow_one]
28     _ = δ ^ ((1 : ℝ) + -(2 : ℝ) / 3) := (Real.rpow_add hδ _ _).symm
29     _ = δ ^ ((1 : ℝ) / 3) := by norm_num
30 
31 private theorem noise_rpow_sq {δ : ℝ} (hδ : 0 < δ) :
32     δ ^ (-(2 : ℝ) / 3) * (δ ^ ((1 : ℝ) / 3)) ^ 2 = 1 := by
33   have hs : (δ ^ ((1 : ℝ) / 3)) ^ 2 = δ ^ ((2 : ℝ) / 3) := by
34     rw [← Real.rpow_natCast, ← Real.rpow_mul hδ.le]
35     norm_num
36   rw [hs, ← Real.rpow_add hδ]
37   norm_num
38 
39 /-- Both ceiling bounds retain the full rounding factor. -/
40 theorem noiseSchedule_bounds {δ : ℝ} (hδ : 0 < δ) (hδ₁ : δ ≤ 1) :
41     δ ^ (-(2 : ℝ) / 3) ≤ (noiseSchedule δ : ℝ) ∧
42       (noiseSchedule δ : ℝ) ≤ 2 * δ ^ (-(2 : ℝ) / 3) := by
43   have hu : 1 ≤ δ ^ (-(2 : ℝ) / 3) := by
44     exact Real.one_le_rpow_of_pos_of_le_one_of_nonpos hδ hδ₁ (by norm_num)
45   constructor
46   · exact Nat.le_ceil _
47   · have hc := Nat.ceil_lt_add_one (show 0 ≤ δ ^ (-(2 : ℝ) / 3) from
48       (Real.rpow_pos_of_pos hδ _).le)
49     dsimp [noiseSchedule]
50     linarith
51 
52 /-- The exact-data term after rounding. -/
53 theorem noiseSchedule_bias_bound {δ : ℝ} (hδ : 0 < δ) (hδ₁ : δ ≤ 1) :
54     Real.sqrt (2 / (noiseSchedule δ : ℝ)) ≤
55       Real.sqrt 2 * δ ^ ((1 : ℝ) / 3) := by
56   have hm : 0 < (noiseSchedule δ : ℝ) := by exact_mod_cast noiseSchedule_pos hδ
57   have hq : 0 < δ ^ ((1 : ℝ) / 3) := Real.rpow_pos_of_pos hδ _
58   have hmul := mul_le_mul_of_nonneg_right (noiseSchedule_bounds hδ hδ₁).1
59     (sq_nonneg (δ ^ ((1 : ℝ) / 3)))
60   rw [noise_rpow_sq hδ] at hmul
61   have hquot : 2 / (noiseSchedule δ : ℝ) ≤ 2 * (δ ^ ((1 : ℝ) / 3)) ^ 2 := by
62     apply (div_le_iff₀ hm).2
63     nlinarith
64   have hleft := Real.sq_sqrt (show 0 ≤ 2 / (noiseSchedule δ : ℝ) by positivity)
65   have hright : (Real.sqrt 2 * δ ^ ((1 : ℝ) / 3)) ^ 2 =
66       2 * (δ ^ ((1 : ℝ) / 3)) ^ 2 := by
67     rw [mul_pow, Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 2)]
68   have hn := Real.sqrt_nonneg (2 / (noiseSchedule δ : ℝ))
69   have hn' : 0 ≤ Real.sqrt 2 * δ ^ ((1 : ℝ) / 3) := by positivity
70   apply (sq_le_sq₀ hn hn').mp
71   rw [hleft, hright]
72   exact hquot
73 
74 /-- The propagated-noise term after rounding. -/
75 theorem noiseSchedule_noise_bound {δ : ℝ} (hδ : 0 < δ) (hδ₁ : δ ≤ 1) :
76     δ * (noiseSchedule δ : ℝ) / 2 ≤ δ ^ ((1 : ℝ) / 3) := by
77   have h := mul_le_mul_of_nonneg_left (noiseSchedule_bounds hδ hδ₁).2 hδ.le
78   have he := noise_rpow_mul hδ
79   nlinarith
80 
81 /-- The scalar part of Corollary 30.3, with the literal ceiling schedule. -/
82 theorem noiseSchedule_rate {δ : ℝ} (hδ : 0 < δ) (hδ₁ : δ ≤ 1) :
83     Real.sqrt (2 / (noiseSchedule δ : ℝ)) + δ * (noiseSchedule δ : ℝ) / 2 ≤
84       (Real.sqrt 2 + 1) * δ ^ ((1 : ℝ) / 3) := by
85   have hb := noiseSchedule_bias_bound hδ hδ₁
86   have hn := noiseSchedule_noise_bound hδ hδ₁
87   nlinarith
88 
89 /-- The sharp universal noise estimate at the inverse-square parameter.
90 This lemma deliberately retains its exact-data bias hypothesis. -/
91 theorem noisy_error_of_bias_bound
92     {H Y : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
93     [NormedAddCommGroup Y] [InnerProductSpace ℝ Y] [CompleteSpace Y]
94     (T : H →L[ℝ] Y) (r s : Y) (aMin : H) (m : ℕ) (hm : 1 ≤ m)
95     {δ : ℝ} (hdata : ‖s - r‖ ≤ δ)
96     (hα : 0 < ((m : ℝ) ^ 2)⁻¹)
97     (hbias : ‖RegularizedHilbertRepair.correction T (((m : ℝ) ^ 2)⁻¹) hα r -
98       aMin‖ ≤ Real.sqrt (2 / (m : ℝ))) :
99     ‖RegularizedHilbertRepair.correction T (((m : ℝ) ^ 2)⁻¹) hα s - aMin‖ ≤
100       Real.sqrt (2 / (m : ℝ)) + δ * (m : ℝ) / 2 := by
101   have hmpos : 0 < (m : ℝ) := by exact_mod_cast (lt_of_lt_of_le Nat.zero_lt_one hm)
102   have hsqrt : Real.sqrt (((m : ℝ) ^ 2)⁻¹) = (m : ℝ)⁻¹ := by
103     rw [Real.sqrt_inv, Real.sqrt_sq hmpos.le]
104   have hnoise := (RegularizedHilbertRepair.data_noise_bound T
105     (((m : ℝ) ^ 2)⁻¹) hα s r).trans
106       (div_le_div_of_nonneg_right hdata (by positivity))
107   rw [hsqrt] at hnoise
108   have hquot : δ / (2 * (m : ℝ)⁻¹) = δ * (m : ℝ) / 2 := by
109     field_simp [ne_of_gt hmpos]
110   rw [hquot] at hnoise
111   have he : RegularizedHilbertRepair.correction T (((m : ℝ) ^ 2)⁻¹) hα s - aMin =
112       (RegularizedHilbertRepair.correction T (((m : ℝ) ^ 2)⁻¹) hα s -
113         RegularizedHilbertRepair.correction T (((m : ℝ) ^ 2)⁻¹) hα r) +
114       (RegularizedHilbertRepair.correction T (((m : ℝ) ^ 2)⁻¹) hα r - aMin) := by
115     abel
116   rw [he]
117   exact (norm_add_le _ _).trans ((add_le_add hnoise hbias).trans_eq (add_comm _ _))
118 
119 /-- The ceiling schedule transfers an assumed exact-data bias bound to a noisy rate.
120 The concrete diagonal corollary additionally needs its proved bias identity. -/
121 theorem noisy_rounded_rate_of_bias_bound
122     {H Y : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
123     [NormedAddCommGroup Y] [InnerProductSpace ℝ Y] [CompleteSpace Y]
124     (T : H →L[ℝ] Y) (r s : Y) (aMin : H) {δ : ℝ}
125     (hδ : 0 < δ) (hδ₁ : δ ≤ 1) (hdata : ‖s - r‖ ≤ δ)
126     (hα : 0 < ((noiseSchedule δ : ℝ) ^ 2)⁻¹)
127     (hbias : ‖RegularizedHilbertRepair.correction T
128       (((noiseSchedule δ : ℝ) ^ 2)⁻¹) hα r - aMin‖ ≤
129         Real.sqrt (2 / (noiseSchedule δ : ℝ))) :
130     ‖RegularizedHilbertRepair.correction T (((noiseSchedule δ : ℝ) ^ 2)⁻¹) hα s -
131       aMin‖ ≤ (Real.sqrt 2 + 1) * δ ^ ((1 : ℝ) / 3) := by
132   exact (noisy_error_of_bias_bound T r s aMin (noiseSchedule δ)
133     (one_le_noiseSchedule hδ) hdata hα hbias).trans (noiseSchedule_rate hδ hδ₁)
134 
135 /-- The concrete attainable datum has the previously estimated infinite bias. -/
136 theorem diagonal_bias_bound {m : ℕ} (hm : 1 ≤ m) :
137     ‖RegularizedHilbertRepair.correction T (alpha m) (alpha_pos hm) b - w‖ ≤
138       Real.sqrt (2 / (m : ℝ)) := by
139   rw [← c_eq_correction hm]
140   apply (sq_le_sq₀ (norm_nonneg _) (Real.sqrt_nonneg _)).mp
141   rw [norm_bias_sq, Real.sq_sqrt (by positivity : 0 ≤ 2 / (m : ℝ))]
142   exact B_upper m hm
143 
144 /-- The first printed inequality for arbitrary Hilbert noise and every positive integer. -/
145 theorem diagonal_noisy_error (s : H) {m : ℕ} (hm : 1 ≤ m) {δ : ℝ}
146     (hdata : ‖s - b‖ ≤ δ) :
147     ‖RegularizedHilbertRepair.correction T (alpha m) (alpha_pos hm) s - w‖ ≤
148       Real.sqrt (2 / (m : ℝ)) + δ * (m : ℝ) / 2 := by
149   exact noisy_error_of_bias_bound T b s w m hm hdata (alpha_pos hm)
150     (diagonal_bias_bound hm)
151 
152 /-- Corollary 30.3 on the actual infinite Hilbert model.
153 The datum and preimage are identified by `b_apply`, `w_apply`, and
154 `w_minimum_norm_preimage`; no exact-data bias assumption remains. -/
155 theorem corollary_30_3 (s : H) {δ : ℝ} (hδ : 0 < δ) (hδ₁ : δ ≤ 1)
156     (hdata : ‖s - b‖ ≤ δ) :
157     let m := Nat.ceil (δ ^ (-(2 : ℝ) / 3))
158     let hm : 1 ≤ m := one_le_noiseSchedule hδ
159     ‖RegularizedHilbertRepair.correction T (alpha m) (alpha_pos hm) s - w‖ ≤
160         Real.sqrt (2 / (m : ℝ)) + δ * (m : ℝ) / 2 ∧
161       Real.sqrt (2 / (m : ℝ)) + δ * (m : ℝ) / 2 ≤
162         (Real.sqrt 2 + 1) * δ ^ ((1 : ℝ) / 3) := by
163   exact ⟨diagonal_noisy_error s (one_le_noiseSchedule hδ) hdata,
164     noiseSchedule_rate hδ hδ₁⟩
165 
166 end KomorebiSpace.DiagonalRegularization

Back to source controls