Documentation

Lean 4 Proof

theorem generalHessianQF_specializes_to_symmetric
    (hJ : 0 < J) (ρ c : ℝ) (hc : c ≠ 0)
    (v : Fin J → ℝ) :
    -(1 - ρ) * c *
      ((∑ k : Fin J,
          (1 : ℝ) / ↑J * (v k / c) ^ 2) -
       (∑ k : Fin J,
          (1 : ℝ) / ↑J * (v k / c)) ^ 2) =
    cesHessianQF J ρ c v := by
  simp only [cesHessianQF]
  have hJne : (↑J : ℝ) ≠ 0 :=
    Nat.cast_ne_zero.mpr (by omega)
  -- Simplify the weighted sums
  have h1 : ∀ k : Fin J,
      (1 : ℝ) / ↑J * (v k / c) ^ 2 =
      v k ^ 2 / (↑J * c ^ 2) := by
    intro k; field_simp
  have h2 : ∀ k : Fin J,
      (1 : ℝ) / ↑J * (v k / c) =
      v k / (↑J * c) := by
    intro k; field_simp
  simp_rw [h1, h2, ← Finset.sum_div]
  field_simp
  ring

Dependency Graph

Location

thesis/CESProofs/Foundations/GeneralHessian.lean:333

Module Section

General CES Hessian at Arbitrary Allocation

In the same file