pith. machine review for the scientific record. sign in
structure definition def or abbrev

DefectSampledFamily

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)

  60structure DefectSampledFamily where
  61  sensor : DefectSensor
  62  mesh : ∀ N : ℕ, AnnularMesh N
  63  charge_spec : ∀ N : ℕ, (mesh N).charge = sensor.charge
  64
  65/-- Convert a `DefectPhaseFamily` to its realized sampled annular family. -/
  66def DefectPhaseFamily.toSampledFamily (dpf : DefectPhaseFamily) :
  67    DefectSampledFamily where
  68  sensor := dpf.sensor

proof body

Definition body.

  69  mesh := defectAnnularMesh dpf
  70  charge_spec := defectAnnularMesh_charge dpf
  71
  72/-- Choose one phase family attached to a hypothetical defect sensor.
  73
  74This uses the strengthened existential package
  75`defect_phase_family_with_perturbation_exists`, so the chosen family comes with
  76the perturbation witness needed downstream for the annular excess argument. -/

used by (16)

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

depends on (4)

Lean names referenced from this declaration's body.