theorem
proved
tactic proof
defect_cost_unbounded
show as:
view Lean formalization →
formal statement (Lean)
147theorem defect_cost_unbounded (sensor : DefectSensor)
148 (hm : sensor.charge ≠ 0) :
149 ∀ B : ℝ, ∃ N : ℕ, ∀ (mesh : AnnularMesh N),
150 (∀ n, (mesh.rings n).winding = sensor.charge) →
151 B < annularCost mesh := by
proof body
Tactic-mode proof.
152 intro B
153 let C : ℝ := Real.pi ^ 2 * kappa / 4 * (sensor.charge : ℝ) ^ 2
154 have hcharge_ne : (sensor.charge : ℝ) ≠ 0 := by
155 exact_mod_cast hm
156 have hC_pos : 0 < C := by
157 unfold C
158 have hsq : 0 < (sensor.charge : ℝ) ^ 2 := by
159 exact sq_pos_iff.mpr hcharge_ne
160 have hpi2 : 0 < Real.pi ^ 2 := by positivity
161 have h4 : 0 < (4 : ℝ) := by norm_num
162 have hconst : 0 < Real.pi ^ 2 * kappa / 4 := by
163 exact div_pos (mul_pos hpi2 kappa_pos) h4
164 exact mul_pos hconst hsq
165 obtain ⟨N0, hN0⟩ :=
166 ((Filter.tendsto_atTop.1 harmonic_sum_diverges) (B / C + 1)).exists_forall_of_atTop
167 refine ⟨N0 + 1, ?_⟩
168 intro mesh hmesh
169 have hsum_gt : B / C < ∑ n : Fin (N0 + 1), (1 : ℝ) / ((n : ℝ) + 1) := by
170 have hge := hN0 (N0 + 1) (Nat.le_succ _)
171 linarith
172 have hscaled : B < C * ∑ n : Fin (N0 + 1), (1 : ℝ) / ((n : ℝ) + 1) := by
173 have hmul := mul_lt_mul_of_pos_left hsum_gt hC_pos
174 have hleft : C * (B / C) = B := by
175 field_simp [hC_pos.ne']
176 calc
177 B = C * (B / C) := hleft.symm
178 _ < C * ∑ n : Fin (N0 + 1), (1 : ℝ) / ((n : ℝ) + 1) := hmul
179 have hcharge_eq : mesh.charge = sensor.charge := by
180 have h0 := hmesh ⟨0, by positivity⟩
181 rw [mesh.uniform_charge ⟨0, by positivity⟩] at h0
182 exact h0
183 have hmesh_nonzero : mesh.charge ≠ 0 := by
184 rw [hcharge_eq]
185 exact hm
186 have hcoerc :
187 C * ∑ n : Fin (N0 + 1), (1 : ℝ) / ((n : ℝ) + 1) ≤ annularCost mesh := by
188 unfold C
189 rw [← hcharge_eq]
190 simpa [mul_assoc, mul_left_comm, mul_comm] using
191 (annular_coercivity (N := N0 + 1) (by positivity) mesh hmesh_nonzero)
192 exact lt_of_lt_of_le hscaled hcoerc
193
194/-- The defect topological floor is unbounded for nonzero charge. -/