Documentation

Lean 4 Proof

theorem effectiveCurvature_le_K {ρ : ℝ} (hρ : ρ < 1)
    (P : Fin J → ℝ) (hP_nn : ∀ j, 0 ≤ P j)
    (hP_sum : ∑ j, P j = 1)
    (hJ : 0 < J) :
    effectiveCurvatureAt ρ P ≤ curvatureK J ρ := by
  -- Cauchy-Schwarz: (Σ P_j)² ≤ J · Σ P_j²
  have hCS : (∑ j : Fin J, P j) ^ 2 ≤
      ↑J * ∑ j : Fin J, P j ^ 2 := by
    have h := @sq_sum_le_card_mul_sum_sq (Fin J) ℝ
      _ _ _ _ Finset.univ P
    simp only [Finset.card_fin] at h; exact h
  rw [hP_sum] at hCS; simp only [one_pow] at hCS
  have hJpos : (0 : ℝ) < ↑J := Nat.cast_pos.mpr hJ
  -- 1 ≤ J · H, so 1/J ≤ H
  have hH : 1 / ↑J ≤ ∑ j : Fin J, P j ^ 2 := by
    rw [div_le_iff₀ hJpos]; linarith
  -- K_eff = (1-ρ)(1-H) ≤ (1-ρ)(1-1/J) = (1-ρ)(J-1)/J = K
  unfold effectiveCurvatureAt escortHerfindahl curvatureK
  have h1ρ : 0 < 1 - ρ := by linarith
  have hJne : (↑J : ℝ) ≠ 0 := ne_of_gt hJpos
  -- Rewrite K as (1-ρ)(1-1/J)
  rw [show (1 - ρ) * (↑J - 1) / ↑J =
    (1 - ρ) * (1 - 1 / ↑J) from by field_simp]
  -- (1-ρ)(1-H) ≤ (1-ρ)(1-1/J) since H ≥ 1/J
  apply mul_le_mul_of_nonneg_left _ h1ρ.le
  linarith

Dependency Graph

Location

thesis/CESProofs/Foundations/GeneralHessian.lean:296

Module Section

General CES Hessian at Arbitrary Allocation

In the same file