Documentation

Lean 4 Proof

theorem compound_symmetry_cov_perp (J : ℕ) (s_sq g : ℝ)
    (v : Fin J → ℝ) (hv : ∑ j : Fin J, v j = 0) (k : Fin J) :
    ∑ j : Fin J, compoundSymmetryMatrix J s_sq g k j * v j =
    (s_sq - g) * v k := by
  simp only [compoundSymmetryMatrix]
  rw [← Finset.add_sum_erase _ _ (Finset.mem_univ k)]
  simp only [ite_true]
  have hne : ∀ j ∈ Finset.univ.erase k,
      (if k = j then s_sq else g) * v j = g * v j := by
    intro j hj; rw [Finset.mem_erase] at hj; simp [Ne.symm hj.1]
  rw [Finset.sum_congr rfl hne, ← Finset.mul_sum]
  set S := Finset.univ.erase k with hS_def
  have hrest : Finset.sum S v = -v k := by
    have h := Finset.add_sum_erase (f := v) Finset.univ (Finset.mem_univ k)
    simp only [← hS_def] at h; linarith
  rw [hrest]; ring

Dependency Graph

Location

thesis/CESProofs/Dynamics/ConservationLaws.lean:116

Module Section

Results 36-46: Conservation Laws and Symmetry Identities

In the same file