Documentation

Lean 4 Proof

theorem superadditivity_qualitative
    (F : AggFun J) (hhom : IsHomogDegOne J F)
    (hconcave : ∀ (x y : Fin J → ℝ) (t : ℝ),
      (∀ j, 0 < x j) → (∀ j, 0 < y j) → 0 ≤ t → t ≤ 1 →
      F (fun j => t * x j + (1 - t) * y j) ≥ t * F x + (1 - t) * F y)
    (x y : Fin J → ℝ) (hx : ∀ j, 0 < x j) (hy : ∀ j, 0 < y j)
    (hFx : 0 < F x) (hFy : 0 < F y) :
    F (fun j => x j + y j) ≥ F x + F y := by
  set s := F x + F y with hs_def
  have hs_pos : 0 < s := by linarith
  set t := F x / s with ht_def
  have ht_ge : 0 ≤ t := div_nonneg (le_of_lt hFx) (le_of_lt hs_pos)
  have ht_le : t ≤ 1 := by rw [ht_def, div_le_one₀ hs_pos]; linarith
  have h1t : 1 - t = F y / s := by
    rw [ht_def]; field_simp; linarith
  set x' := fun j => x j / F x
  set y' := fun j => y j / F y
  have hx' : ∀ j, 0 < x' j := fun j => div_pos (hx j) hFx
  have hy' : ∀ j, 0 < y' j := fun j => div_pos (hy j) hFy
  have hFx' : F x' = 1 := by
    have h1 := hhom x (F x)⁻¹ (inv_pos.mpr hFx)
    rw [show (fun j => (F x)⁻¹ * x j) = x' from by
      ext j; simp [x', div_eq_inv_mul]] at h1
    rw [h1, inv_mul_cancel₀ (ne_of_gt hFx)]
  have hFy' : F y' = 1 := by
    have h1 := hhom y (F y)⁻¹ (inv_pos.mpr hFy)
    rw [show (fun j => (F y)⁻¹ * y j) = y' from by
      ext j; simp [y', div_eq_inv_mul]] at h1
    rw [h1, inv_mul_cancel₀ (ne_of_gt hFy)]
  have mix_eq : ∀ j, x j + y j = s * (t * x' j + (1 - t) * y' j) := by
    intro j; simp only [x', y', ht_def]
    have hFxne : F x ≠ 0 := ne_of_gt hFx
    have hFyne : F y ≠ 0 := ne_of_gt hFy
    have hsne : s ≠ 0 := ne_of_gt hs_pos
    field_simp; ring
  have hconc := hconcave x' y' t hx' hy' ht_ge ht_le
  rw [hFx', hFy'] at hconc
  have hge1 : F (fun j => t * x' j + (1 - t) * y' j) ≥ 1 := by linarith
  have := hhom (fun j => t * x' j + (1 - t) * y' j) s hs_pos
  rw [show (fun j => s * (t * x' j + (1 - t) * y' j)) = (fun j => x j + y j) from by
    ext j; rw [mix_eq]] at this
  rw [this]
  calc s * F (fun j => t * x' j + (1 - t) * y' j)
      ≥ s * 1 := by apply mul_le_mul_of_nonneg_left hge1 (le_of_lt hs_pos)
    _ = s := mul_one s

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/Superadditivity.lean:48

Module Section

Superadditivity of CES (Paper 1, Section 6):

In the same file