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

defect_le_constants_mul_energyGap

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)

  91theorem defect_le_constants_mul_energyGap
  92  (M : Model β) (a : β) :
  93  M.defectMass a ≤ (M.C.Knet * M.C.Cproj * M.C.Ceng) * M.energyGap a := by

proof body

Tactic-mode proof.

  94  have hA : M.defectMass a ≤ M.C.Knet * M.C.Cproj * M.orthoMass a :=
  95    M.projection_defect a
  96  have hB : M.orthoMass a ≤ M.C.Ceng * M.energyGap a :=
  97    M.energy_control a
  98  calc M.defectMass a
  99      ≤ M.C.Knet * M.C.Cproj * M.orthoMass a := hA
 100    _ ≤ M.C.Knet * M.C.Cproj * (M.C.Ceng * M.energyGap a) := by
 101        apply mul_le_mul_of_nonneg_left hB
 102        have h₁ : 0 ≤ M.C.Knet := M.C.Knet_nonneg
 103        have h₂ : 0 ≤ M.C.Cproj := M.C.Cproj_nonneg
 104        exact mul_nonneg h₁ h₂
 105    _ = (M.C.Knet * M.C.Cproj * M.C.Ceng) * M.energyGap a := by ring
 106
 107/-- Coercivity in the usual “energy gap ≥ c_min · defect” form.
 108
 109Requires the product `K_net · C_proj · C_eng` to be strictly positive to
 110invert safely. -/

used by (5)

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

depends on (13)

Lean names referenced from this declaration's body.