realizedDefectCollapseBoundaryApproaching_of_nonzero_charge

proof body

Tactic-mode proof.

 359  intro ε hε
 360  let fam := canonicalDefectSampledFamily sensor hm
 361  have hfam : fam.sensor.charge ≠ 0 := by
 362    simpa [fam, canonicalDefectSampledFamily_sensor] using hm
 363  by_cases hεle : ε ≤ 1
 364  · let B : ℝ := ε⁻¹ - 1
 365    obtain ⟨N, hN⟩ := defectSampledFamily_unbounded fam hfam B
 366    refine ⟨N, ?_⟩
 367    unfold realizedDefectCollapseScalar
 368    dsimp [fam, B] at hN ⊢
 369    have hden_pos : 0 < 1 + annularCost ((canonicalDefectSampledFamily sensor hm).mesh N) := by
 370      have hcost_nonneg :
 371          0 ≤ annularCost ((canonicalDefectSampledFamily sensor hm).mesh N) :=
 372        annularCost_nonneg _
 373      linarith
 374    have hmul :
 375        1 < ε * (1 + annularCost ((canonicalDefectSampledFamily sensor hm).mesh N)) := by
 376      have hgt : ε⁻¹ < 1 + annularCost ((canonicalDefectSampledFamily sensor hm).mesh N) := by
 377        linarith
 378      have hεpos : 0 < ε := hε
 379      have htmp := mul_lt_mul_of_pos_left hgt hεpos
 380      have hleft : ε * ε⁻¹ = 1 := by
 381        field_simp [hε.ne']
 382      calc
 383        1 = ε * ε⁻¹ := hleft.symm
 384        _ < ε * (1 + annularCost ((canonicalDefectSampledFamily sensor hm).mesh N)) := htmp
 385    rw [div_lt_iff₀ hden_pos]
 386    exact hmul
 387  · have hεgt : 1 < ε := lt_of_not_ge hεle
 388    obtain ⟨N, hN⟩ := defectSampledFamily_unbounded fam hfam 0
 389    refine ⟨N, ?_⟩
 390    unfold realizedDefectCollapseScalar
 391    have hden_pos : 0 < 1 + annularCost ((canonicalDefectSampledFamily sensor hm).mesh N) := by
 392      linarith
 393    have hlt_one :
 394        1 / (1 + annularCost ((canonicalDefectSampledFamily sensor hm).mesh N)) < 1 := by
 395      have hden_gt : 1 < 1 + annularCost ((canonicalDefectSampledFamily sensor hm).mesh N) := by
 396        linarith
 397      rw [div_lt_iff₀ hden_pos, one_mul]
 398      simpa using hden_gt
 399    exact lt_trans hlt_one hεgt
 400
 401/-- Closed form of the T1 defect on the realized collapse scalar. -/