449theorem defectSampledFamily_unbounded (fam : DefectSampledFamily) 450 (hm : fam.sensor.charge ≠ 0) : 451 ∀ B : ℝ, ∃ N : ℕ, B < annularCost (fam.mesh N) := by
proof body
Tactic-mode proof.
452 intro B 453 obtain ⟨N, hN⟩ := defect_cost_unbounded fam.sensor hm B 454 refine ⟨N, ?_⟩ 455 have hcharge : ∀ n, ((fam.mesh N).rings n).winding = fam.sensor.charge := by 456 intro n 457 rw [((fam.mesh N).uniform_charge n), fam.charge_spec N] 458 exact hN (fam.mesh N) hcharge 459 460/-- A realized sampled family with nonzero charge can never have bounded annular 461cost. This is the contradiction theorem underlying the refined Axiom 2. -/
used by (5)
From the project-wide theorem graph. These declarations reference this one in their body.