pith. machine review for the scientific record. sign in
lemma proved decidable or rfl

coherence_defect_expand

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)

  69private lemma coherence_defect_expand (field : ProcessingField) (obj : ExtendedObject) (a : ℝ) :
  70    coherence_defect field obj a =
  71      abs ((field.phi obj.h_cm + deriv field.phi obj.h_cm * obj.extent + a * obj.extent) -
  72           (field.phi obj.h_cm + deriv field.phi obj.h_cm * (-obj.extent) + a * (-obj.extent))) := by

proof body

Decided by rfl or decide.

  73  rfl
  74
  75/-- Closed form for the linearized coherence defect:
  76    `coherence_defect = | 2 * extent * (∂ϕ + a) |`. -/

used by (1)

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

depends on (5)

Lean names referenced from this declaration's body.