defect_cost_unbounded

formal source

 144    a defect with unbounded annular cost, violating cost-covering.
 145
 146    This is the key contradiction lemma. -/
 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
 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