pith. machine review for the scientific record. sign in
theorem proved term proof

canonicalDefectSampledFamily_charge

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 107theorem canonicalDefectSampledFamily_charge (sensor : DefectSensor)
 108    (hm : sensor.charge ≠ 0) (N : ℕ) :
 109    ((canonicalDefectSampledFamily sensor hm).mesh N).charge = sensor.charge := by

proof body

Term-mode proof.

 110  simpa [canonicalDefectSampledFamily_sensor sensor hm] using
 111    ((canonicalDefectSampledFamily sensor hm).charge_spec N)
 112
 113/-! ### §3. Refined bounded-cost proposition -/
 114
 115/-- The annular cost of a realized sampled family is bounded independently of
 116mesh refinement. This is the realizable replacement for the previous
 117over-strong quantification over arbitrary `AnnularMesh` values. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (17)

Lean names referenced from this declaration's body.