Documentation

Lean 4 Proof

theorem equalWeights_maximize_K (_hJ : 2 ≤ J) {ρ : ℝ} (_hρ : ρ < 1)
    {a : Fin J → ℝ} (_ha_pos : ∀ j, 0 < a j) (_ha_sum : ∑ j : Fin J, a j = 1) :
    generalCurvatureK J ρ a ≤ curvatureK J ρ := by
  -- K(ρ,a) = (1-ρ)(1-H) ≤ (1-ρ)(1-1/J) = K  because H ≥ 1/J
  -- By Cauchy-Schwarz: (Σ aⱼ)² ≤ J · Σ aⱼ², so 1 ≤ J·H, i.e. H ≥ 1/J.
  simp only [generalCurvatureK, curvatureK]
  have hJne : (↑J : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (by omega)
  have hJpos : (0 : ℝ) < ↑J := by exact_mod_cast (by omega : 0 < J)
  have h1ρ : 0 < 1 - ρ := by linarith
  -- Cauchy-Schwarz: (Σ aⱼ)² ≤ card · Σ aⱼ²
  have cs := sq_sum_le_card_mul_sum_sq (s := Finset.univ) (f := a)
  rw [Finset.card_univ, Fintype.card_fin, _ha_sum] at cs
  -- cs : 1 ^ 2 ≤ ↑J * Σ aⱼ², i.e. 1 ≤ J * Σ aⱼ²
  simp only [one_pow] at cs
  -- Need: (1-ρ)(1 - Σaⱼ²) ≤ (1-ρ)(J-1)/J
  -- Suffices: 1 - Σaⱼ² ≤ (J-1)/J = 1 - 1/J
  -- i.e., 1/J ≤ Σaⱼ²
  -- From cs: 1 ≤ J * Σaⱼ², so 1/J ≤ Σaⱼ²
  -- Goal: (1-ρ)*(1 - Σaⱼ²) ≤ (1-ρ)*(J-1)/J
  -- Rewrite RHS as (1-ρ)*((J-1)/J)
  have goal_rw : (1 - ρ) * (↑J - 1) / ↑J = (1 - ρ) * ((↑J - 1) / ↑J) := by ring
  rw [goal_rw]
  apply mul_le_mul_of_nonneg_left _ (le_of_lt h1ρ)
  -- Need: 1 - Σaⱼ² ≤ (J-1)/J = 1 - 1/J, i.e. 1/J ≤ Σaⱼ²
  -- From cs: 1 ≤ J * Σaⱼ², so Σaⱼ² ≥ 1/J
  -- Need: 1 - Σaⱼ² ≤ (J-1)/J
  rw [sub_div, div_self hJne]
  -- Goal: 1 - Σaⱼ² ≤ 1 - 1/J, i.e. 1/J ≤ Σaⱼ²
  -- 1/J ≤ Σaⱼ² follows from cs: 1 ≤ J*Σaⱼ²
  have h1J : 1 / (↑J : ℝ) ≤ ∑ j : Fin J, a j ^ 2 := by
    rw [div_le_iff₀ hJpos]
    linarith [mul_comm (↑J : ℝ) (∑ i : Fin J, a i ^ 2)]
  linarith

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/GeneralWeights.lean:142

Module Section

General-weight CES results (Paper 1, Section 10):

In the same file