Documentation

Lean 4 Proof

private lemma multinomial_qf (P w : Fin J → ℝ) :
    ∑ i : Fin J, ∑ j : Fin J,
      (P i * P j - if i = j then P i else 0) *
        w i * w j =
    (∑ k, P k * w k) ^ 2 - ∑ k, P k * w k ^ 2 := by
  have h_split : ∀ i j : Fin J,
      (P i * P j - if i = j then P i else 0) *
        w i * w j =
      P i * w i * (P j * w j) -
        (if i = j then P i * w i ^ 2 else 0) := by
    intro i j
    split_ifs with h <;> [subst h; skip] <;> ring
  simp_rw [h_split, Finset.sum_sub_distrib]
  congr 1
  · rw [sq, Fintype.sum_mul_sum]
  · congr 1; ext i
    rw [Finset.sum_ite_eq Finset.univ i]; simp

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/GeneralHessian.lean:96

Module Section

General CES Hessian at Arbitrary Allocation

In the same file