IndisputableMonolith.Cost.Convexity

   1import Mathlib.Analysis.Convex.Deriv
   2import Mathlib.Analysis.Calculus.Deriv.Inv
   3import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
   4import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
   5import IndisputableMonolith.Cost
   6
   7/-!
   8# Convexity of J
   9
  10This module proves that:
  111. Jlog(t) = cosh t - 1 is strictly convex on ℝ
  122. Jcost(x) = ½(x + x⁻¹) - 1 is strictly convex on ℝ₊
  13
  14These are foundational for the uniqueness theorem T5.
  15-/
  16
  17namespace IndisputableMonolith
  18namespace Cost
  19
  20open Real Set
  21
  22open scoped Real
  23
  24/-- cosh is strictly convex on ℝ.
  25
  26    Proof: cosh'' = cosh > 0 everywhere. A function with positive second
  27    derivative on a convex set is strictly convex. -/
  28theorem cosh_strictly_convex : StrictConvexOn ℝ univ Real.cosh := by
  29  apply strictConvexOn_of_deriv2_pos convex_univ
  30  · -- cosh is continuous
  31    exact Real.continuous_cosh.continuousOn
  32  · -- cosh'' = cosh > 0 on interior (which is univ)
  33    intro x _
  34    -- deriv^[2] cosh = cosh
  35    show 0 < deriv^[2] Real.cosh x
  36    rw [Function.iterate_succ, Function.iterate_one, Function.comp_apply]
  37    -- First derivative of cosh is sinh
  38    have h1 : deriv Real.cosh = Real.sinh := Real.deriv_cosh
  39    -- Second derivative: deriv sinh = cosh
  40    have h2 : deriv Real.sinh = Real.cosh := Real.deriv_sinh
  41    -- So deriv (deriv cosh) x = cosh x > 0
  42    rw [h1, congrFun h2 x]
  43    exact Real.cosh_pos x
  44
  45/-- Strict convexity of `Real.cosh` on the whole line. -/
  46theorem strictConvexOn_cosh : StrictConvexOn ℝ univ Real.cosh := cosh_strictly_convex
  47
  48lemma Jlog_eq_cosh_sub_one (t : ℝ) : Jlog t = Real.cosh t - 1 :=
  49  Jlog_as_cosh t
  50
  51/-- Strict convexity of `Jlog` on `ℝ`. -/
  52theorem Jlog_strictConvexOn : StrictConvexOn ℝ univ Jlog := by
  53  -- Jlog = cosh - 1, and cosh is strictly convex
  54  -- Subtracting a constant preserves strict convexity
  55  have h : Jlog = fun t => Real.cosh t - 1 := by ext t; exact Jlog_eq_cosh_sub_one t
  56  rw [h]
  57  exact strictConvexOn_cosh.add_const (-1)
  58
  59/-- First derivative of Jcost: J'(x) = (1 - x⁻²)/2 -/
  60noncomputable def JcostDeriv (x : ℝ) : ℝ := (1 - x ^ (-2 : ℤ)) / 2
  61
  62lemma hasDerivAt_Jcost_pos {x : ℝ} (hx : 0 < x) :
  63    HasDerivAt Jcost (JcostDeriv x) x := by
  64  -- Jcost x = (x + x⁻¹)/2 - 1
  65  -- Jcost' x = (1 - x⁻²)/2
  66  unfold Jcost JcostDeriv
  67  have hne : x ≠ 0 := hx.ne'
  68  -- d/dx (x + x⁻¹)/2 - 1 = (1 - x⁻²)/2
  69  have h1 : HasDerivAt (fun y => y) 1 x := hasDerivAt_id x
  70  have h2 : HasDerivAt (fun y => y⁻¹) (-(x^2)⁻¹) x := by
  71    have hinv := hasDerivAt_inv hne
  72    simp only [neg_neg] at hinv
  73    convert hinv using 1
  74  have h3 : HasDerivAt (fun y => y + y⁻¹) (1 + (-(x^2)⁻¹)) x := h1.add h2
  75  have h4 : HasDerivAt (fun y => (y + y⁻¹) / 2) ((1 + (-(x^2)⁻¹)) / 2) x := h3.div_const 2
  76  have h5 : HasDerivAt (fun y => (y + y⁻¹) / 2 - 1) ((1 + (-(x^2)⁻¹)) / 2) x := h4.sub_const 1
  77  convert h5 using 1
  78
  79lemma deriv_Jcost {x : ℝ} (hx : 0 < x) :
  80    deriv Jcost x = JcostDeriv x := (hasDerivAt_Jcost_pos hx).deriv
  81
  82/-- Second derivative of Jcost: J''(x) = x⁻³ -/
  83noncomputable def JcostDeriv' (x : ℝ) : ℝ := x ^ (-3 : ℤ)
  84
  85lemma hasDerivAt_JcostDeriv {x : ℝ} (hx : 0 < x) :
  86    HasDerivAt JcostDeriv (JcostDeriv' x) x := by
  87  -- JcostDeriv x = (1 - x⁻²)/2
  88  -- JcostDeriv' x = x⁻³
  89  -- d/dx (1 - x⁻²)/2 = -(-2x⁻³)/2 = x⁻³
  90  unfold JcostDeriv JcostDeriv'
  91  have hne : x ≠ 0 := hx.ne'
  92  have h1 : HasDerivAt (fun y => (1 : ℝ)) 0 x := hasDerivAt_const x 1
  93  have h2 : HasDerivAt (fun y => y ^ (-2 : ℤ)) ((-2 : ℤ) * x ^ (-2 - 1 : ℤ)) x := by
  94    exact hasDerivAt_zpow (-2) x (Or.inl hne)
  95  have h3 : HasDerivAt (fun y => 1 - y ^ (-2 : ℤ)) (0 - (-2 : ℤ) * x ^ (-3 : ℤ)) x := h1.sub h2
  96  have h4 : HasDerivAt (fun y => (1 - y ^ (-2 : ℤ)) / 2) ((0 - (-2 : ℤ) * x ^ (-3 : ℤ)) / 2) x :=
  97    h3.div_const 2
  98  convert h4 using 1
  99  simp only [sub_neg_eq_add, zero_add, Int.cast_neg, Int.cast_ofNat]
 100  field_simp
 101  ring
 102
 103lemma deriv_JcostDeriv {x : ℝ} (hx : 0 < x) :
 104    deriv JcostDeriv x = JcostDeriv' x := (hasDerivAt_JcostDeriv hx).deriv
 105
 106/-- Second derivative of Jcost at x > 0: J''(x) = x⁻³ -/
 107lemma deriv2_Jcost {x : ℝ} (hx : 0 < x) :
 108    deriv (deriv Jcost) x = x ^ (-3 : ℤ) := by
 109  have h_event : ∀ᶠ y in nhds x, deriv Jcost y = JcostDeriv y := by
 110    have h_mem : Set.Ioi (0 : ℝ) ∈ nhds x := Ioi_mem_nhds hx
 111    filter_upwards [h_mem] with y hy using deriv_Jcost hy
 112  have h_deriv2 : deriv (deriv Jcost) x = deriv JcostDeriv x :=
 113    Filter.EventuallyEq.deriv_eq h_event
 114  rw [h_deriv2, deriv_JcostDeriv hx]
 115  rfl
 116
 117/-- Second derivative of Jcost at 1 equals 1: J''(1) = 1 -/
 118theorem deriv2_Jcost_one : deriv (deriv Jcost) 1 = 1 := by
 119  rw [deriv2_Jcost one_pos]
 120  simp
 121
 122/-- Strict convexity of `Jcost` on `(0, ∞)`. -/
 123theorem Jcost_strictConvexOn_pos : StrictConvexOn ℝ (Ioi (0 : ℝ)) Jcost := by
 124  -- A function is strictly convex if its derivative is strictly increasing
 125  apply strictConvexOn_of_deriv2_pos (convex_Ioi 0)
 126  · -- Continuity on (0, ∞)
 127    unfold Jcost
 128    apply ContinuousOn.sub
 129    · apply ContinuousOn.div_const
 130      apply ContinuousOn.add continuousOn_id
 131      exact continuousOn_inv₀.mono (fun x hx => ne_of_gt hx)
 132    · exact continuousOn_const
 133  · -- Positive second derivative on interior
 134    intro x hx
 135    rw [interior_Ioi] at hx
 136    -- deriv^[2] Jcost x = x⁻³ > 0
 137    show 0 < deriv^[2] Jcost x
 138    rw [Function.iterate_succ, Function.iterate_one, Function.comp_apply]
 139    -- In a neighborhood of x, deriv Jcost = JcostDeriv
 140    have h_event : ∀ᶠ y in nhds x, deriv Jcost y = JcostDeriv y := by
 141      have h_mem : Ioi (0 : ℝ) ∈ nhds x := Ioi_mem_nhds hx
 142      filter_upwards [h_mem] with y hy using deriv_Jcost hy
 143    have h_deriv2 : deriv (deriv Jcost) x = deriv JcostDeriv x := Filter.EventuallyEq.deriv_eq h_event
 144    rw [h_deriv2, deriv_JcostDeriv hx]
 145    unfold JcostDeriv'
 146    -- x ^ (-3) > 0 for x > 0
 147    have hx_pos : 0 < x := hx
 148    exact zpow_pos hx_pos (-3)
 149
 150/-- Helper: Jcost on positive reals via composition with exp -/
 151lemma Jcost_as_composition {x : ℝ} (hx : 0 < x) :
 152  Jcost x = Jlog (log x) := by
 153  -- Jlog t = Jcost (exp t), so Jlog (log x) = Jcost (exp (log x)) = Jcost x
 154  unfold Jlog
 155  congr 1
 156  exact (Real.exp_log hx).symm
 157
 158end Cost
 159end IndisputableMonolith
 160