Documentation

Lean 4 Proof

theorem antisym_quadform_zero {M : ℕ}
    (A : Fin M -> Fin M -> ℝ) (hA : IsAntisymmetric A) (x : Fin M -> ℝ) :
    ∑ i, ∑ j, A i j * x i * x j = 0 := by
  have key : ∀ i j : Fin M, A i j = -A j i := hA
  -- S = sum_i sum_j A_{ij} x_i x_j
  -- By exchanging i,j: S = sum_j sum_i A_{ji} x_j x_i = sum_i sum_j A_{ji} x_j x_i
  -- = sum_i sum_j (-A_{ij}) x_j x_i = -sum_i sum_j A_{ij} x_i x_j = -S
  -- So S = -S, hence S = 0.
  have h : ∑ i, ∑ j, A i j * x i * x j = -(∑ i, ∑ j, A i j * x i * x j) := by
    conv_lhs =>
      rw [Finset.sum_comm]
      arg 2; ext j; arg 2; ext i
      rw [key i j]
    simp only [neg_mul, Finset.sum_neg_distrib]
    congr 1; congr 1; ext i; congr 1; ext j; ring
  linarith

Dependency Graph

Location

thesis/CESProofs/Dynamics/PhillipsCycles.lean:118

Module Section

Results 63-69: Phillips Curve, Endogenous Cycles, and Oscillation Energy

In the same file