Documentation

Lean 4 Proof

theorem superadditivity_quantitative_bound
    (F : AggFun J) (hhom : IsHomogDegOne J F)
    (x y : Fin J → ℝ) (hx : ∀ j, 0 < x j) (hy : ∀ j, 0 < y j)
    (hFx : 0 < F x) (hFy : 0 < F y)
    (C : ℝ) (hC : 0 ≤ C)
    (dist : (Fin J → ℝ) → (Fin J → ℝ) → ℝ)
    (hdist_nn : ∀ x' y', 0 ≤ dist x' y')
    (hstrong : ∀ (x' y' : Fin J → ℝ) (t : ℝ),
      (∀ j, 0 < x' j) → (∀ j, 0 < y' j) →
      F x' = 1 → F y' = 1 →
      0 ≤ t → t ≤ 1 →
      (∀ j, 0 < t * x' j + (1 - t) * y' j) →
      F (fun j => t * x' j + (1 - t) * y' j) - 1 ≥
        C * t * (1 - t) * dist x' y') :
    F (fun j => x j + y j) - F x - F y ≥
      C / 2 * min (F x) (F y) * dist (fun j => x j / F x) (fun j => y j / F y) := by
  set s := F x + F y with hs_def
  have hs_pos : 0 < s := by linarith
  have hsne : s ≠ 0 := ne_of_gt hs_pos
  set t := F x / s with ht_def
  have ht_ge : 0 ≤ t := div_nonneg hFx.le hs_pos.le
  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 hmix : ∀ j, 0 < t * x' j + (1 - t) * y' j := by
    intro j
    by_cases h0 : t = 0
    · simp only [h0, zero_mul, zero_add, one_mul, sub_zero]; exact hy' j
    · exact add_pos_of_pos_of_nonneg
        (mul_pos (lt_of_le_of_ne ht_ge (Ne.symm h0)) (hx' j))
        (mul_nonneg (by linarith) (hy' j).le)
  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]; field_simp; ring
  have hFxy := 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 hFxy
  set dsq := dist x' y'
  have hdeficit := hstrong x' y' t hx' hy' hFx' hFy' ht_ge ht_le hmix
  have hgap : F (fun j => x j + y j) - F x - F y =
      s * (F (fun j => t * x' j + (1 - t) * y' j) - 1) := by
    rw [hFxy]; ring
  have hdsq_nn : 0 ≤ dsq := hdist_nn x' y'
  rw [hgap]
  have hstep1 : s * (F (fun j => t * x' j + (1 - t) * y' j) - 1) ≥
      s * (C * t * (1 - t) * dsq) :=
    mul_le_mul_of_nonneg_left hdeficit hs_pos.le
  have hstep2 : s * (C * t * (1 - t) * dsq) =
      C * (F x * F y / s) * dsq := by
    rw [ht_def, h1t]; field_simp
  have hHM : min (F x) (F y) / 2 ≤ F x * F y / s :=
    harmonic_mean_ge_half_min hFx hFy
  calc s * (F (fun j => t * x' j + (1 - t) * y' j) - 1)
      ≥ s * (C * t * (1 - t) * dsq) := hstep1
    _ = C * (F x * F y / s) * dsq := hstep2
    _ ≥ C * (min (F x) (F y) / 2) * dsq :=
        mul_le_mul_of_nonneg_right (mul_le_mul_of_nonneg_left hHM hC) hdsq_nn
    _ = C / 2 * min (F x) (F y) * dsq := by ring

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/Superadditivity.lean:423

Module Section

Superadditivity of CES (Paper 1, Section 6):

In the same file