Documentation

Lean 4 Proof

theorem static_vri_cross {Jn Jm : ℕ}
    (P_n : Fin Jn → ℝ) (P_m : Fin Jm → ℝ)
    (x_n : Fin Jn → ℝ) (x_m : Fin Jm → ℝ) :
    (∑ j, ∑ k, P_n j * P_m k * x_n j * x_m k) =
    (∑ j, P_n j * x_n j) * (∑ k, P_m k * x_m k) := by
  have h : ∀ j k, P_n j * P_m k * x_n j * x_m k =
      (P_n j * x_n j) * (P_m k * x_m k) := by intros; ring
  simp_rw [h, ← Finset.mul_sum, ← Finset.sum_mul]

Dependency Graph

Location

thesis/CESProofs/Dynamics/FluctuationResponse.lean:46

Module Section

Results 8-16: Variance-Response Identity and Early Warning

In the same file