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

dJdt_eq_viscous_plus_stretching

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)

 105theorem dJdt_eq_viscous_plus_stretching {siteCount : ℕ} (e : EvolutionIdentity siteCount)
 106    (htransport : totalTransport e.contributions = 0) :
 107    e.dJdt = totalViscous e.contributions + totalStretching e.contributions := by

proof body

Term-mode proof.

 108  rw [e.split, htransport, zero_add]
 109
 110/-- If stretching is absorbed by viscosity, then the total derivative is nonpositive. -/

used by (1)

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

depends on (11)

Lean names referenced from this declaration's body.