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

total_conservativeTransportField_zero

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)

  73theorem total_conservativeTransportField_zero {siteCount : ℕ}
  74    (flux : ScalarField siteCount) (perm : Equiv.Perm (Fin siteCount)) :
  75    total (conservativeTransportField flux perm) = 0 := by

proof body

Tactic-mode proof.

  76  unfold total conservativeTransportField
  77  rw [Finset.sum_sub_distrib]
  78  have hperm : (∑ i : Fin siteCount, flux (perm i)) = ∑ i : Fin siteCount, flux i := by
  79    simpa using (Equiv.sum_comp perm flux)
  80  rw [hperm]
  81  ring
  82
  83/-! ## Velocity Gradient Magnitude -/
  84
  85/-- Maximum absolute forward difference across all component/direction pairs. -/

used by (2)

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.