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

master_absorption

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)

 117theorem master_absorption
 118    {dJdt transport_total viscous_total stretching_total : ℝ}
 119    (hsplit : dJdt = transport_total + viscous_total + stretching_total)
 120    (htransport : transport_total = 0)
 121    (habsorb : stretching_total ≤ -viscous_total) :
 122    dJdt ≤ 0 := by

proof body

Term-mode proof.

 123  rw [hsplit, htransport, zero_add]; linarith
 124
 125/-! ## Exponential Decay -/
 126

depends on (1)

Lean names referenced from this declaration's body.