Documentation

Lean 4 Proof

theorem subadditivity_qualitative
    (F : AggFun J) (hhom : IsHomogDegOne J F)
    (hconvex : ∀ (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
  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 hconv := hconvex x' y' t hx' hy' ht_ge ht_le
  rw [hFx', hFy'] at hconv
  -- hconv : F(t*x' + (1-t)*y') ≤ t*1 + (1-t)*1 = 1
  have hle1 : F (fun j => t * x' j + (1 - t) * y' j) ≤ 1 := by linarith
  have hmix := 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 hmix
  rw [hmix]
  calc s * F (fun j => t * x' j + (1 - t) * y' j)
      ≤ s * 1 := by apply mul_le_mul_of_nonneg_left hle1 (le_of_lt hs_pos)
    _ = s := mul_one s

Dependency Graph

Location

thesis/CESProofs/Potential/SubstituteRegime.lean:104

Module Section

Substitute Regime: The ρ > 1 Theory (Anti-Complementarity)

In the same file