Documentation

Lean 4 Proof

theorem cesGeneralHessianQF_eq_neg_variance
    (ρ F : ℝ) (P x v : Fin J → ℝ)
    (hx : ∀ j, x j ≠ 0) :
    cesGeneralHessianQF ρ F P x v =
      -(1 - ρ) * F *
        ((∑ k, P k * (v k / x k) ^ 2) -
         (∑ k, P k * (v k / x k)) ^ 2) := by
  unfold cesGeneralHessianQF cesGeneralHessianEntry
  -- Rewrite each H_{ij} v_i v_j in terms of w_j = v_j/x_j
  have h_entry : ∀ i j : Fin J,
      (if i = j then
        F * (1 - ρ) * P i * (P i - 1) / (x i) ^ 2
      else
        F * (1 - ρ) * P i * P j / (x i * x j)) *
        v i * v j =
      F * (1 - ρ) *
        ((P i * P j - if i = j then P i else 0) *
          (v i / x i) * (v j / x j)) := by
    intro i j
    split_ifs with h
    · subst h; field_simp
    · field_simp; ring
  simp_rw [h_entry]
  -- Pull F(1-ρ) out of the double sum
  have pull_const : ∀ (c : ℝ) (f : Fin J → Fin J → ℝ),
      ∑ i : Fin J, ∑ j : Fin J, c * f i j =
      c * ∑ i : Fin J, ∑ j : Fin J, f i j := by
    intro c f
    simp_rw [← Finset.mul_sum]
  rw [pull_const]
  rw [multinomial_qf P (fun j => v j / x j)]
  ring

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/GeneralHessian.lean:136

Module Section

General CES Hessian at Arbitrary Allocation

In the same file