Documentation

Lean 4 Proof

lemma rpow_concavity_deficit (ρ a b t : ℝ)
    (hρ0 : 0 < ρ) (hρ1 : ρ < 1)
    (ha : 0 < a) (hb : 0 < b)
    (ht0 : 0 ≤ t) (ht1 : t ≤ 1) :
    (t * a + (1 - t) * b) ^ ρ - t * a ^ ρ - (1 - t) * b ^ ρ ≥
      ρ * (1 - ρ) / 2 * (max a b) ^ (ρ - 2) * t * (1 - t) * (a - b) ^ 2 := by
  -- Define the mixing function u(s) = sa + (1-s)b and the modulus
  set u : ℝ → ℝ := fun s => s * a + (1 - s) * b with hu_def
  set m := ρ * (1 - ρ) / 2 * max a b ^ (ρ - 2) with hm_def
  -- Define the residual h(s) = u(s)^ρ - s·a^ρ - (1-s)·b^ρ - m·s·(1-s)·(a-b)²
  set h : ℝ → ℝ := fun s =>
    (u s) ^ ρ - s * a ^ ρ - (1 - s) * b ^ ρ - m * s * (1 - s) * (a - b) ^ 2 with hh_def
  -- Suffices: h(t) ≥ 0
  suffices hsuff : 0 ≤ h t by simp only [hh_def, hu_def] at hsuff; linarith
  -- u(s) > 0 for s ∈ [0,1]
  have hu_pos : ∀ s ∈ Set.Icc (0 : ℝ) 1, 0 < u s := by
    intro s ⟨hs0, hs1⟩; simp only [hu_def]
    nlinarith [mul_nonneg hs0 ha.le, mul_nonneg (show 0 ≤ 1 - s by linarith) hb.le]
  have hmax_pos : 0 < max a b := lt_max_of_lt_left ha
  -- h(0) = 0, h(1) = 0
  have hh0 : h 0 = 0 := by simp [hh_def, hu_def]
  have hh1 : h 1 = 0 := by simp [hh_def, hu_def]
  -- u has derivative a - b everywhere
  have hu_hasderiv : ∀ s, HasDerivAt u (a - b) s := by
    intro s; show HasDerivAt (fun s => s * a + (1 - s) * b) (a - b) s
    have h1 : HasDerivAt (fun s => s * a) (1 * a) s := hasDerivAt_id s |>.mul_const a
    have h2 : HasDerivAt (fun s => (1 - s) * b) ((0 - 1) * b) s :=
      (hasDerivAt_const s 1 |>.sub (hasDerivAt_id s)).mul_const b
    exact (h1.add h2).congr_deriv (by ring)
  -- Define h', h'' for the second derivative test
  set h' : ℝ → ℝ := fun s =>
    ρ * (a - b) * (u s) ^ (ρ - 1) - (a ^ ρ - b ^ ρ) -
    m * (1 - 2 * s) * (a - b) ^ 2 with hh'_def
  set h'' : ℝ → ℝ := fun s =>
    ρ * (ρ - 1) * (a - b) ^ 2 * (u s) ^ (ρ - 2) +
    2 * m * (a - b) ^ 2 with hh''_def
  -- h is continuous on [0,1]
  have hh_cont : ContinuousOn h (Set.Icc 0 1) := by
    apply ContinuousOn.sub
    · apply ContinuousOn.sub
      · apply ContinuousOn.sub
        · apply ContinuousOn.rpow_const
          · exact (continuous_id.mul continuous_const |>.add
              ((continuous_const.sub continuous_id).mul continuous_const)).continuousOn
          · intro s hs; left; exact ne_of_gt (hu_pos s hs)
        · exact continuousOn_id.mul continuousOn_const
      · exact (continuousOn_const.sub continuousOn_id).mul continuousOn_const
    · exact ((continuousOn_const.mul continuousOn_id).mul
        (continuousOn_const.sub continuousOn_id)).mul continuousOn_const
  -- h has first derivative h' on interior
  have hh_deriv : ∀ s ∈ interior (Set.Icc (0 : ℝ) 1),
      HasDerivWithinAt h (h' s) (interior (Set.Icc 0 1)) s := by
    intro s hs; rw [interior_Icc] at hs ⊢
    obtain ⟨hs0, hs1⟩ := hs
    have hus_pos := hu_pos s ⟨hs0.le, hs1.le⟩
    have h1 : HasDerivWithinAt (fun s => (u s) ^ ρ)
        ((a - b) * ρ * (u s) ^ (ρ - 1)) (Set.Ioo 0 1) s :=
      (hu_hasderiv s).hasDerivWithinAt.rpow_const (Or.inl (ne_of_gt hus_pos))
    have h2 : HasDerivWithinAt (fun s => s * a ^ ρ) (1 * a ^ ρ) (Set.Ioo 0 1) s :=
      (hasDerivWithinAt_id s _).mul_const _
    have h3 : HasDerivWithinAt (fun s => (1 - s) * b ^ ρ) ((0 - 1) * b ^ ρ) (Set.Ioo 0 1) s :=
      ((hasDerivWithinAt_const s _ 1).sub (hasDerivWithinAt_id s _)).mul_const _
    have h4 : HasDerivWithinAt (fun s => m * s * (1 - s) * (a - b) ^ 2)
        (m * (1 - 2 * s) * (a - b) ^ 2) (Set.Ioo 0 1) s := by
      -- Compute as polynomial: m*(a-b)²*(s - s²), derivative m*(a-b)²*(1 - 2s)
      set C := m * (a - b) ^ 2
      have h_id : HasDerivAt (fun s : ℝ => C * s) (C * 1) s :=
        (hasDerivAt_id s).const_mul C
      have h_sq : HasDerivAt (fun s : ℝ => C * s ^ 2) (C * (2 * s)) s := by
        have h := (hasDerivAt_pow 2 s).const_mul C
        simp only [show (2 : ℕ) - 1 = 1 from rfl, pow_one] at h; exact h
      have h_poly : HasDerivAt (fun s : ℝ => C * s - C * s ^ 2)
          (C * 1 - C * (2 * s)) s := h_id.sub h_sq
      have h_eq_fun : (fun s : ℝ => C * s - C * s ^ 2) =
          (fun s => m * s * (1 - s) * (a - b) ^ 2) := by ext s; simp [C]; ring
      have h_eq_deriv : C * 1 - C * (2 * s) = m * (1 - 2 * s) * (a - b) ^ 2 := by
        simp [C]; ring
      exact (h_eq_fun ▸ h_eq_deriv ▸ h_poly).hasDerivWithinAt
    exact ((h1.sub h2).sub h3).sub h4 |>.congr_deriv (by ring)
  -- h has second derivative h'' on interior
  have hh'_deriv : ∀ s ∈ interior (Set.Icc (0 : ℝ) 1),
      HasDerivWithinAt h' (h'' s) (interior (Set.Icc 0 1)) s := by
    intro s hs; rw [interior_Icc] at hs ⊢
    obtain ⟨hs0, hs1⟩ := hs
    have hus_pos := hu_pos s ⟨hs0.le, hs1.le⟩
    -- d/ds [ρ(a-b) · u(s)^{ρ-1}] = ρ(a-b) · (a-b)(ρ-1) · u(s)^{ρ-2}
    have h1 : HasDerivWithinAt (fun s => ρ * (a - b) * (u s) ^ (ρ - 1))
        (ρ * (a - b) * ((a - b) * (ρ - 1) * (u s) ^ (ρ - 1 - 1))) (Set.Ioo 0 1) s :=
      ((hu_hasderiv s).hasDerivWithinAt.rpow_const
        (Or.inl (ne_of_gt hus_pos))).const_mul _
    -- d/ds [-(a^ρ - b^ρ)] = 0; d/ds [-m(1-2s)(a-b)²] = 2m(a-b)²
    have h2 : HasDerivWithinAt (fun s => -(m * (1 - 2 * s) * (a - b) ^ 2))
        (2 * m * (a - b) ^ 2) (Set.Ioo 0 1) s := by
      -- Rewrite as linear polynomial: 2*D*s - D where D = m*(a-b)²
      set D := m * (a - b) ^ 2
      have h_lin : HasDerivAt (fun s : ℝ => 2 * D * s) (2 * D) s := by
        have h := (hasDerivAt_id s).const_mul (2 * D)
        simp only [id, mul_one] at h; exact h
      have h_const : HasDerivAt (fun s : ℝ => D) (0 : ℝ) s := hasDerivAt_const s D
      have h_poly : HasDerivAt (fun s : ℝ => 2 * D * s - D) (2 * D - 0) s :=
        h_lin.sub h_const
      have h_eq_fun : (fun s : ℝ => 2 * D * s - D) =
          (fun s => -(m * (1 - 2 * s) * (a - b) ^ 2)) := by ext s; simp [D]; ring
      have h_eq_deriv : 2 * D - 0 = 2 * m * (a - b) ^ 2 := by simp [D]; ring
      exact (h_eq_fun ▸ h_eq_deriv ▸ h_poly).hasDerivWithinAt
    -- h' = term1 - const - quad, so h'' combines term1_deriv + 0 + quad_deriv
    have h3 := (h1.sub (hasDerivWithinAt_const s (Set.Ioo 0 1) (a ^ ρ - b ^ ρ))).add h2
    exact h3.congr_deriv (by show _ = h'' s; simp only [hh''_def]; ring)
  -- h'' ≤ 0 on interior: h''(s) = (a-b)² · ρ(ρ-1) · [u(s)^{ρ-2} - max^{ρ-2}]
  have hh''_nonpos : ∀ s ∈ interior (Set.Icc (0 : ℝ) 1), h'' s ≤ 0 := by
    intro s hs; rw [interior_Icc] at hs
    obtain ⟨hs0, hs1⟩ := hs
    have hus_pos := hu_pos s ⟨hs0.le, hs1.le⟩
    -- u(s) ≤ max(a,b)
    have hus_le : u s ≤ max a b := by
      simp only [hu_def]
      calc s * a + (1 - s) * b
          ≤ s * max a b + (1 - s) * max a b := by
            gcongr; exact le_max_left a b; linarith; exact le_max_right a b
        _ = max a b := by ring
    -- ρ - 2 < 0, so u^{ρ-2} ≥ max^{ρ-2}
    have hus_rpow : max a b ^ (ρ - 2) ≤ (u s) ^ (ρ - 2) :=
      rpow_le_rpow_of_nonpos hus_pos hus_le (by linarith : ρ - 2 ≤ 0)
    -- Factor h''(s) = (a-b)² · ρ(ρ-1) · [u^{ρ-2} - max^{ρ-2}]
    show h'' s ≤ 0
    simp only [hh''_def, hm_def]
    have hfactor :
        ρ * (ρ - 1) * (a - b) ^ 2 * (u s) ^ (ρ - 2) +
        2 * (ρ * (1 - ρ) / 2 * max a b ^ (ρ - 2)) * (a - b) ^ 2 =
        ρ * (ρ - 1) * ((u s) ^ (ρ - 2) - max a b ^ (ρ - 2)) * (a - b) ^ 2 := by ring
    rw [hfactor]
    -- ρ(ρ-1) < 0, diff ≥ 0, (a-b)² ≥ 0, so product ≤ 0
    have hρρ1_neg : ρ * (ρ - 1) < 0 := by nlinarith
    have hdiff_nn : 0 ≤ (u s) ^ (ρ - 2) - max a b ^ (ρ - 2) := by linarith
    exact mul_nonpos_of_nonpos_of_nonneg
      (mul_nonpos_of_nonpos_of_nonneg hρρ1_neg.le hdiff_nn) (sq_nonneg _)
  -- h is concave on [0,1]
  have hh_concave : ConcaveOn ℝ (Set.Icc 0 1) h :=
    concaveOn_of_hasDerivWithinAt2_nonpos (convex_Icc 0 1) hh_cont hh_deriv hh'_deriv hh''_nonpos
  -- h(t) ≥ 0 from concavity + zero endpoints
  exact concaveOn_nonneg_of_endpoints hh_concave (le_of_eq hh0.symm) (le_of_eq hh1.symm) ht0 ht1

Dependency Graph

Used by

Location

thesis/CESProofs/CurvatureRoles/Superadditivity.lean:143

Module Section

Superadditivity of CES (Paper 1, Section 6):

In the same file