DiagonalTheorems.lean

1 import KomorebiSpace.DiagonalNoisyRate
2 
3 set_option autoImplicit false
4 noncomputable section
5 namespace KomorebiSpace.DiagonalRegularization
6 
7 /-- The displayed infinite vector is the unique global regularized minimizer. -/
8 theorem a_unique_minimizer {m : ℕ} (hm : 1 ≤ m) :
9     (∀ x : H, RegularizedHilbertRepair.objective T (alpha m) w (a m) ≤
10       RegularizedHilbertRepair.objective T (alpha m) w x) ∧
11     (∀ x : H, (∀ y : H, RegularizedHilbertRepair.objective T (alpha m) w x ≤
12       RegularizedHilbertRepair.objective T (alpha m) w y) → x = a m) := by
13   constructor
14   · intro x
15     rw [a_eq_correction hm]
16     exact RegularizedHilbertRepair.correction_best T (alpha m) (alpha_pos hm) w x
17   · intro x hx
18     rw [a_eq_correction hm]
19     exact RegularizedHilbertRepair.correction_unique T (alpha m) (alpha_pos hm) w x (hx _)
20 
21 /-- Proposition 30.1, with all infinite-model and quantitative obligations combined.
22 The coordinate formulas are the definitions identified by `a_apply` and `v_apply`.
23 Membership in the actual Hilbert space is part of the types of `a m` and `v m`. -/
24 theorem proposition_30_1 (m K : ℕ) (hm : 1 ≤ m) (hmK : m ≤ K) :
25     a m = RegularizedHilbertRepair.correction T (alpha m) (alpha_pos hm) w ∧
26     w - T (a m) = v m ∧
27     ‖a m‖ ^ 2 = A m ∧ ‖v m‖ ^ 2 = B m ∧
28     (m : ℝ) / 4 ≤ A m ∧ A m ≤ 4 * (m : ℝ) / 3 ∧
29     1 / (4 * ((m : ℝ) + 1)) ≤ B m ∧ B m ≤ 2 / (m : ℝ) ∧
30     0 ≤ A m - partialA m K ∧ A m - partialA m K ≤ (m : ℝ)^4 / (3 * (K : ℝ)^3) ∧
31     0 ≤ B m - partialB m K ∧ B m - partialB m K ≤ 1 / (K : ℝ) := by
32   exact ⟨a_eq_correction hm, residual_eq_v m, norm_a_sq m, norm_v_sq m,
33     proposition_30_1_series m K hm hmK⟩
34 
35 end KomorebiSpace.DiagonalRegularization

Back to source controls