theorem
proved
tactic proof
weight_polynomial_decay_summable
show as:
view Lean formalization →
formal statement (Lean)
104theorem weight_polynomial_decay_summable {lamP : Nat.Primes → ℝ}
105 {ε : ℝ} (hε : 0 ≤ ε) (h : WeightDecayPolynomial lamP ε) :
106 WeightSquareSummable lamP := by
proof body
Tactic-mode proof.
107 obtain ⟨C, hC_pos, hC⟩ := h
108 -- Define the comparison function on Nat.Primes.
109 set g : Nat.Primes → ℝ := fun p => (C / (p.val : ℝ) ^ (1 + ε)) ^ 2 with hg_def
110 -- Step 1: g is summable.
111 have h_g_sum : Summable g := by
112 have h_exp : (1 : ℝ) < 2 * (1 + ε) := by linarith
113 have h_nat_sum : Summable (fun n : ℕ => (1 : ℝ) / (n : ℝ) ^ (2 * (1 + ε))) := by
114 simpa using Real.summable_one_div_nat_rpow.mpr h_exp
115 have h_inj : Function.Injective (fun p : Nat.Primes => p.val) := fun _ _ hpq => Subtype.ext hpq
116 -- Comparison: (C / p^(1+ε))^2 = C^2 / p^(2(1+ε))
117 -- Pull back to primes.
118 have h_pulled : Summable (fun p : Nat.Primes =>
119 (1 : ℝ) / ((p.val : ℝ)) ^ (2 * (1 + ε))) := by
120 have := h_nat_sum.comp_injective h_inj
121 simpa [Function.comp] using this
122 have h_scaled : Summable (fun p : Nat.Primes =>
123 C^2 * ((1 : ℝ) / ((p.val : ℝ)) ^ (2 * (1 + ε)))) :=
124 h_pulled.mul_left (C^2)
125 -- Now: g p = C^2 * (1 / p^(2(1+ε))).
126 have h_g_eq : ∀ p : Nat.Primes,
127 g p = C^2 * ((1 : ℝ) / ((p.val : ℝ)) ^ (2 * (1 + ε))) := by
128 intro p
129 have hpval : (0 : ℝ) < (p.val : ℝ) := by exact_mod_cast p.prop.pos
130 have h_pow_split : ((p.val : ℝ)) ^ (2 * (1 + ε)) =
131 (((p.val : ℝ)) ^ (1 + ε)) ^ 2 := by
132 rw [show (2 * (1 + ε) : ℝ) = (1 + ε) + (1 + ε) from by ring]
133 rw [Real.rpow_add hpval]
134 ring
135 simp only [hg_def, div_pow, h_pow_split]
136 ring
137 have h_eq_func : g = fun p : Nat.Primes =>
138 C^2 * ((1 : ℝ) / ((p.val : ℝ)) ^ (2 * (1 + ε))) := by
139 funext p; exact h_g_eq p
140 rw [h_eq_func]
141 exact h_scaled
142 -- Step 2: |λ_p|^2 ≤ g(p) pointwise.
143 have h_pointwise : ∀ p : Nat.Primes, ‖(lamP p) ^ 2‖ ≤ g p := by
144 intro p
145 have hbound : |lamP p| ≤ C / (p.val : ℝ) ^ (1 + ε) := hC p
146 have h_abs_nn : 0 ≤ |lamP p| := abs_nonneg _
147 have hnorm : ‖(lamP p) ^ 2‖ = (lamP p) ^ 2 := by
148 rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)]
149 rw [hnorm]
150 have h_abs_sq : (lamP p) ^ 2 = |lamP p| ^ 2 := (sq_abs _).symm
151 rw [h_abs_sq]
152 have h_div_nn : 0 ≤ C / (p.val : ℝ) ^ (1 + ε) := by
153 apply div_nonneg (le_of_lt hC_pos)
154 apply le_of_lt
155 apply Real.rpow_pos_of_pos
156 exact_mod_cast p.prop.pos
157 -- Unfold g and convert ^2 to multiplication on both sides.
158 show |lamP p| ^ 2 ≤ (C / (p.val : ℝ) ^ (1 + ε)) ^ 2
159 rw [sq, sq]
160 exact mul_le_mul hbound hbound h_abs_nn h_div_nn
161 exact Summable.of_norm_bounded h_g_sum h_pointwise
162
163/-! ## Hypothesis structures: the three regularity sub-conjectures -/
164
165/-- Sub-conjecture C.1: essential self-adjointness of the cost
166 operator on the dense domain `denseDomain`, given the bandwidth
167 constraint. -/