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

defectAnnularMesh

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)

  40def defectAnnularMesh (dpf : DefectPhaseFamily) (N : ℕ) : AnnularMesh N where
  41  rings := fun k =>

proof body

Definition body.

  42    (dpf.phaseAtLevel (k.val + 1) (Nat.succ_pos k.val)).toAnnularRingSample
  43      (k.val + 1) (Nat.succ_pos k.val)
  44  charge := dpf.sensor.charge
  45  uniform_charge := fun k =>
  46    dpf.charge_uniform (k.val + 1) (Nat.succ_pos k.val)
  47
  48/-- The mesh obtained from phase sampling has the correct total charge. -/

used by (6)

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

depends on (9)

Lean names referenced from this declaration's body.