Documentation

Lean 4 Proof

theorem compound_symmetry_cov (J : ℕ) (s_sq g : ℝ) (hJ : 1 ≤ J) (i : Fin J) :
    ∑ j : Fin J, compoundSymmetryMatrix J s_sq g i j * 1 =
    (s_sq + (↑J - 1) * g) * 1 := by
  simp only [mul_one, compoundSymmetryMatrix]
  rw [← Finset.add_sum_erase _ _ (Finset.mem_univ i)]
  simp only [ite_true]
  have hcard : (Finset.univ.erase i).card = J - 1 := by
    rw [Finset.card_erase_of_mem (Finset.mem_univ i), Finset.card_fin]
  have hne : ∀ j ∈ Finset.univ.erase i, (if i = j then s_sq else g) = g := by
    intro j hj; rw [Finset.mem_erase] at hj; simp [Ne.symm hj.1]
  rw [Finset.sum_congr rfl hne, Finset.sum_const, hcard, nsmul_eq_mul]
  push_cast [Nat.cast_sub hJ]; ring

Dependency Graph

Location

thesis/CESProofs/Dynamics/ConservationLaws.lean:101

Module Section

Results 36-46: Conservation Laws and Symmetry Identities

In the same file