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

modified_total_potential

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)

  76def modified_total_potential
  77    (field : ProcessingField) (ext : ExternalPhaseField)
  78    (obj : ExtendedObject) (a : ℝ) (z : ℝ) : ℝ :=

proof body

Definition body.

  79  let phi_grav := field.phi obj.h_cm + (deriv field.phi obj.h_cm) * z
  80  let phi_ext := ext.psi obj.h_cm + (deriv ext.psi obj.h_cm) * z
  81  let phi_acc := a * z
  82  phi_grav + phi_ext + phi_acc
  83
  84/-- Modified coherence defect with external phase field present. -/

used by (1)

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

depends on (7)

Lean names referenced from this declaration's body.