IndisputableMonolith.Cost.JcostCore

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace Cost
   5
   6noncomputable def Jcost (x : ℝ) : ℝ := (x + x⁻¹) / 2 - 1
   7
   8structure CostRequirements (F : ℝ → ℝ) : Type where
   9  symmetric : ∀ {x}, 0 < x → F x = F x⁻¹
  10  unit0 : F 1 = 0
  11
  12lemma Jcost_unit0 : Jcost 1 = 0 := by
  13  simp [Jcost]
  14
  15lemma Jcost_symm {x : ℝ} (hx : 0 < x) : Jcost x = Jcost x⁻¹ := by
  16  have hx0 : x ≠ 0 := ne_of_gt hx
  17  unfold Jcost
  18  have : (x + x⁻¹) = (x⁻¹ + (x⁻¹)⁻¹) := by
  19    field_simp [hx0]
  20    ring
  21  simp [this]
  22
  23lemma Jcost_eq_sq {x : ℝ} (hx : x ≠ 0) :
  24    Jcost x = (x - 1) ^ 2 / (2 * x) := by
  25  have hx2 : (2 * x) ≠ 0 := mul_ne_zero two_ne_zero hx
  26  have hL : Jcost x * (2 * x) = (x - 1) ^ 2 := by
  27    unfold Jcost
  28    have : ((x + x⁻¹) / 2 - 1) * (2 * x) = (x - 1) ^ 2 := by
  29      field_simp [hx]
  30      ring
  31    simpa using this
  32  have hR : ((x - 1) ^ 2 / (2 * x)) * (2 * x) = (x - 1) ^ 2 := by
  33    field_simp [hx]
  34  refine (mul_right_cancel₀ hx2) ?_;
  35  calc
  36    Jcost x * (2 * x) = (x - 1) ^ 2 := hL
  37    _ = ((x - 1) ^ 2 / (2 * x)) * (2 * x) := by simpa using hR.symm
  38
  39lemma Jcost_nonneg {x : ℝ} (hx : 0 < x) : 0 ≤ Jcost x := by
  40  have hx0 : x ≠ 0 := ne_of_gt hx
  41  have hrepr := Jcost_eq_sq (x := x) hx0
  42  have hnum : 0 ≤ (x - 1) ^ 2 := by exact sq_nonneg (x - 1)
  43  have hden : 0 < 2 * x := mul_pos (by norm_num : (0 : ℝ) < 2) hx
  44  have hfrac : 0 ≤ (x - 1) ^ 2 / (2 * x) :=
  45    div_nonneg hnum (le_of_lt hden)
  46  simpa [hrepr] using hfrac
  47
  48lemma Jcost_one_plus_eps_quadratic (ε : ℝ) (hε : |ε| ≤ (1 : ℝ) / 2) :
  49    ∃ (c : ℝ), Jcost (1 + ε) = ε ^ 2 / 2 + c * ε ^ 3 ∧ |c| ≤ 2 := by
  50  classical
  51  have hbounds := abs_le.mp hε
  52  have hpos : 0 < 1 + ε := by
  53    have : -(1 : ℝ) / 2 ≤ ε := by simpa [neg_div] using hbounds.1
  54    linarith
  55  have hne : 1 + ε ≠ 0 := ne_of_gt hpos
  56  have hcalc : Jcost (1 + ε) = ε ^ 2 / (2 * (1 + ε)) := by
  57    simpa [pow_two, add_comm, add_left_comm, add_assoc, sub_eq_add_neg]
  58      using (Jcost_eq_sq (x := 1 + ε) hne)
  59  let c : ℝ := -1 / (2 * (1 + ε))
  60  have h_eq :
  61      Jcost (1 + ε) = ε ^ 2 / 2 + c * ε ^ 3 := by
  62    have : ε ^ 2 / (2 * (1 + ε)) = ε ^ 2 / 2 + (-1 / (2 * (1 + ε))) * ε ^ 3 := by
  63      field_simp [hne]
  64      ring
  65    simpa [hcalc, c] using this
  66  have hden_pos : 0 < 2 * (1 + ε) := by nlinarith [hpos]
  67  have habs : |c| = 1 / (2 * (1 + ε)) := by
  68    simp [c, div_eq_mul_inv, abs_mul, abs_inv, abs_of_pos hpos]
  69  -- Use 1/(2(1+ε)) ≤ 1 from (1+ε) ≥ 1/2
  70  have hone_le : (1 : ℝ) ≤ 2 * (1 + ε) := by
  71    have : (1 / 2 : ℝ) ≤ 1 + ε := by linarith
  72    simpa [two_mul] using mul_le_mul_of_nonneg_left this (by norm_num : (0 : ℝ) ≤ 2)
  73  have hdiv_le_one : 1 / (2 * (1 + ε)) ≤ 1 := by
  74    have hpos1 : 0 < (1 : ℝ) := by norm_num
  75    simpa [one_div] using one_div_le_one_div_of_le hpos1 hone_le
  76  have hbound : |c| ≤ 2 := by
  77    have h1 : |c| ≤ 1 := by simpa [habs] using hdiv_le_one
  78    have h12 : (1 : ℝ) ≤ 2 := by norm_num
  79    exact le_trans h1 h12
  80  exact ⟨c, h_eq, hbound⟩
  81
  82lemma Jcost_small_strain_bound (ε : ℝ) (hε : |ε| ≤ (1 : ℝ) / 10) :
  83    |Jcost (1 + ε) - ε ^ 2 / 2| ≤ ε ^ 2 / 10 := by
  84  classical
  85  have hbounds := abs_le.mp hε
  86  have hpos : 0 < 1 + ε := by
  87    have : -(1 : ℝ) / 10 ≤ ε := by simpa [neg_div] using hbounds.1
  88    linarith
  89  have hne : 1 + ε ≠ 0 := ne_of_gt hpos
  90  have hform : Jcost (1 + ε) = ε ^ 2 / (2 * (1 + ε)) := by
  91    simpa [pow_two, add_comm, add_left_comm, add_assoc, sub_eq_add_neg]
  92      using (Jcost_eq_sq (x := 1 + ε) hne)
  93  have hden_pos : 0 < 2 * (1 + ε) := by nlinarith [hpos]
  94  -- Exact difference and absolute value
  95  have h1 : Jcost (1 + ε) - ε ^ 2 / 2
  96      = ε ^ 2 / (2 * (1 + ε)) - ε ^ 2 / 2 := by
  97    simpa [hform]
  98  have hx : (2 : ℝ) * (1 + ε) ≠ 0 := mul_ne_zero two_ne_zero hne
  99  have h2 : ε ^ 2 / (2 * (1 + ε)) - ε ^ 2 / 2 = -ε ^ 3 / (2 * (1 + ε)) := by
 100    field_simp [hx]
 101    ring
 102  have hdiff : Jcost (1 + ε) - ε ^ 2 / 2 = -ε ^ 3 / (2 * (1 + ε)) := h1.trans h2
 103  have habs : |Jcost (1 + ε) - ε ^ 2 / 2| = |ε| ^ 3 / (2 * (1 + ε)) := by
 104    have hposden : 0 < 2 * (1 + ε) := hden_pos
 105    simpa [abs_div, abs_neg, abs_pow, abs_of_pos hposden] using
 106      congrArg (fun z => |z|) hdiff
 107  -- Now bound using |ε|/(2(1+ε)) ≤ 1/18 from below
 108  have hx_lower : (9 : ℝ) / 10 ≤ 1 + ε := by linarith [show -(1 : ℝ) / 10 ≤ ε from by simpa [neg_div] using hbounds.1]
 109  have hx_pos : 0 < (9 : ℝ) / 10 := by norm_num
 110  have hx_inv : 1 / (1 + ε) ≤ (10 : ℝ) / 9 := by
 111    have := one_div_le_one_div_of_le hx_pos hx_lower
 112    simpa using this
 113  have hrec_bound : 1 / (2 * (1 + ε)) ≤ (5 : ℝ) / 9 := by
 114    have hmul : (1 / 2 : ℝ) * (1 / (1 + ε)) ≤ (1 / 2) * ((10 : ℝ) / 9) :=
 115      mul_le_mul_of_nonneg_left hx_inv (by norm_num)
 116    have hleft : 1 / (2 * (1 + ε)) = (1 / 2) * (1 / (1 + ε)) := by
 117      simp [div_eq_mul_inv, mul_comm, mul_left_comm, mul_assoc]
 118    have hright : (5 : ℝ) / 9 = (1 / 2) * ((10 : ℝ) / 9) := by norm_num
 119    simpa [hleft, hright] using hmul
 120  have hrec_nonneg : 0 ≤ 1 / (2 * (1 + ε)) := by
 121    have : 0 ≤ 2 * (1 + ε) := le_of_lt (by nlinarith [hpos])
 122    exact one_div_nonneg.mpr this
 123  have hA : |ε| / (2 * (1 + ε)) ≤ (1 : ℝ) / 10 * (1 / (2 * (1 + ε))) := by
 124    simpa [div_eq_mul_inv, mul_comm, mul_left_comm, mul_assoc]
 125      using mul_le_mul_of_nonneg_right hε hrec_nonneg
 126  have hB : (1 : ℝ) / 10 * (1 / (2 * (1 + ε))) ≤ (1 : ℝ) / 18 := by
 127    have hmul := mul_le_mul_of_nonneg_left hrec_bound (by norm_num : (0 : ℝ) ≤ (1 : ℝ) / 10)
 128    have hright : (1 : ℝ) / 18 = (1 : ℝ) / 10 * ((5 : ℝ) / 9) := by norm_num
 129    simpa [hright] using hmul
 130  have hfrac : |ε| / (2 * (1 + ε)) ≤ (1 : ℝ) / 18 := hA.trans hB
 131  -- Conclude
 132  have hineq : |Jcost (1 + ε) - ε ^ 2 / 2| ≤ |ε| ^ 2 / 18 := by
 133    have hnn : 0 ≤ |ε| ^ 2 := by
 134      have := sq_nonneg (|ε|); simpa [pow_two] using this
 135    have hmul := mul_le_mul_of_nonneg_left hfrac hnn
 136    calc
 137      |Jcost (1 + ε) - ε ^ 2 / 2| = |ε| ^ 3 / (2 * (1 + ε)) := by simpa [habs]
 138      _ ≤ |ε| ^ 2 * (1 / 18) := by
 139        simpa [pow_succ, pow_two, mul_comm, mul_left_comm, mul_assoc, div_eq_mul_inv] using hmul
 140      _ = |ε| ^ 2 / 18 := by simp [div_eq_mul_inv]
 141  have hratio : (1 : ℝ) / 18 ≤ 1 / 10 := by norm_num
 142  have hsq : |ε| ^ 2 = ε ^ 2 := by
 143    have h1 : |ε| * |ε| = |ε * ε| := by simpa [abs_mul]
 144    calc
 145      |ε| ^ 2 = |ε| * |ε| := by simpa [pow_two]
 146      _ = |ε * ε| := h1
 147      _ = |ε ^ 2| := by simpa [pow_two]
 148      _ = ε ^ 2 := by simpa [abs_of_nonneg (sq_nonneg ε)]
 149  have hcompare : |ε| ^ 2 / 18 ≤ ε ^ 2 / 10 := by
 150    have := mul_le_mul_of_nonneg_left hratio (by exact sq_nonneg ε)
 151    simpa [hsq, pow_two] using this
 152  exact (hineq.trans hcompare)
 153
 154def AgreesOnExp (F : ℝ → ℝ) : Prop := ∀ t : ℝ, F (Real.exp t) = Jcost (Real.exp t)
 155
 156@[simp] lemma Jcost_exp (t : ℝ) :
 157  Jcost (Real.exp t) = ((Real.exp t) + (Real.exp (-t))) / 2 - 1 := by
 158  have h : (Real.exp t)⁻¹ = Real.exp (-t) := by
 159    symm; simp [Real.exp_neg t]
 160  simp [Jcost, h]
 161
 162class SymmUnit (F : ℝ → ℝ) : Prop where
 163  symmetric : ∀ {x}, 0 < x → F x = F x⁻¹
 164  unit0 : F 1 = 0
 165
 166class AveragingAgree (F : ℝ → ℝ) : Prop where
 167  agrees : AgreesOnExp F
 168
 169class AveragingDerivation (F : ℝ → ℝ) : Prop extends SymmUnit F where
 170  agrees : AgreesOnExp F
 171
 172class AveragingBounds (F : ℝ → ℝ) : Prop extends SymmUnit F where
 173  upper : ∀ t : ℝ, F (Real.exp t) ≤ Jcost (Real.exp t)
 174  lower : ∀ t : ℝ, Jcost (Real.exp t) ≤ F (Real.exp t)
 175
 176def mkAveragingBounds (F : ℝ → ℝ)
 177  (symm : SymmUnit F)
 178  (upper : ∀ t : ℝ, F (Real.exp t) ≤ Jcost (Real.exp t))
 179  (lower : ∀ t : ℝ, Jcost (Real.exp t) ≤ F (Real.exp t)) :
 180  AveragingBounds F :=
 181{ toSymmUnit := symm, upper := upper, lower := lower }
 182
 183class JensenSketch (F : ℝ → ℝ) : Prop extends SymmUnit F where
 184  axis_upper : ∀ t : ℝ, F (Real.exp t) ≤ Jcost (Real.exp t)
 185  axis_lower : ∀ t : ℝ, Jcost (Real.exp t) ≤ F (Real.exp t)
 186
 187noncomputable def F_ofLog (G : ℝ → ℝ) : ℝ → ℝ := fun x => G (Real.log x)
 188
 189class LogModel (G : ℝ → ℝ) : Prop where
 190  even_log : ∀ t : ℝ, G (-t) = G t
 191  base0 : G 0 = 0
 192  upper_cosh : ∀ t : ℝ, G t ≤ ((Real.exp t + Real.exp (-t)) / 2 - 1)
 193  lower_cosh : ∀ t : ℝ, ((Real.exp t + Real.exp (-t)) / 2 - 1) ≤ G t
 194
 195@[simp] theorem Jcost_agrees_on_exp : AgreesOnExp Jcost := by
 196  intro t; rfl
 197
 198instance : AveragingAgree Jcost := ⟨Jcost_agrees_on_exp⟩
 199
 200instance : SymmUnit Jcost :=
 201  { symmetric := by
 202      intro x hx
 203      simp [Jcost_symm (x:=x) hx]
 204    , unit0 := Jcost_unit0 }
 205
 206instance : AveragingDerivation Jcost :=
 207  { toSymmUnit := (inferInstance : SymmUnit Jcost)
 208  , agrees := Jcost_agrees_on_exp }
 209
 210instance : JensenSketch Jcost :=
 211  { toSymmUnit := (inferInstance : SymmUnit Jcost)
 212  , axis_upper := by intro t; exact le_of_eq rfl
 213  , axis_lower := by intro t; exact le_of_eq rfl }
 214
 215/-!
 216## Small-strain Taylor expansion
 217This section provides small-strain expansions used by Axiom A4.
 218-/
 219
 220/-! ## Monotonicity Properties -/
 221
 222/-- J-cost derivative: d/dx J(x) = 1/2 - 1/(2x²) -/
 223lemma Jcost_deriv (x : ℝ) (hx : x ≠ 0) :
 224    deriv Jcost x = (1 - x⁻¹ ^ 2) / 2 := by
 225  unfold Jcost
 226  have hdiff : DifferentiableAt ℝ (fun y => (y + y⁻¹) / 2 - 1) x := by
 227    apply DifferentiableAt.sub
 228    · apply DifferentiableAt.div_const
 229      apply DifferentiableAt.add differentiableAt_id (differentiableAt_inv hx)
 230    · exact differentiableAt_const 1
 231  have h : deriv (fun y => (y + y⁻¹) / 2 - 1) x = (1 - x⁻¹ ^ 2) / 2 := by
 232    have h1 : HasDerivAt (fun y => y) 1 x := hasDerivAt_id x
 233    have h2 : HasDerivAt (fun y => y⁻¹) (-(x^2)⁻¹) x := hasDerivAt_inv hx
 234    have h3 : HasDerivAt (fun y => y + y⁻¹) (1 + -(x^2)⁻¹) x := h1.add h2
 235    have h4 : HasDerivAt (fun y => (y + y⁻¹) / 2) ((1 + -(x^2)⁻¹) / 2) x := h3.div_const 2
 236    have h5 : HasDerivAt (fun y => (y + y⁻¹) / 2 - 1) ((1 + -(x^2)⁻¹) / 2) x := h4.sub_const 1
 237    rw [h5.deriv]
 238    field_simp [hx]
 239    ring
 240  exact h
 241
 242/-- J-cost is strictly increasing on (1, ∞) -/
 243lemma Jcost_strict_mono_on_one_infty (x y : ℝ) (hx : 0 < x) (hy : 0 < y)
 244    (hx1 : 1 ≤ x) (hxy : x < y) :
 245    Jcost x < Jcost y := by
 246  -- Use the squared form: Jcost x = (x-1)²/(2x)
 247  have hx0 : x ≠ 0 := ne_of_gt hx
 248  have hy0 : y ≠ 0 := ne_of_gt hy
 249  rw [Jcost_eq_sq hx0, Jcost_eq_sq hy0]
 250  -- Need: (x-1)²/(2x) < (y-1)²/(2y)
 251  have h2x : 0 < 2 * x := by linarith
 252  have h2y : 0 < 2 * y := by linarith
 253  rw [div_lt_div_iff₀ h2x h2y]
 254  -- Need: (x-1)² * (2y) < (y-1)² * (2x)
 255  have hx_sub : 0 ≤ x - 1 := by linarith
 256  have hy_sub : 0 < y - 1 := by linarith
 257  -- Expand: 2y(x-1)² < 2x(y-1)²
 258  -- Simplify: y(x-1)² < x(y-1)²
 259  have hmain : (x - 1) ^ 2 * (2 * y) < (y - 1) ^ 2 * (2 * x) := by
 260    -- Use calculus or direct algebra
 261    -- (x-1)²·y < (y-1)²·x ⟺ (x-1)²/x < (y-1)²/y for x,y > 0
 262    -- Let f(t) = (t-1)²/t = t - 2 + 1/t. Then f'(t) = 1 - 1/t² > 0 for t > 1
 263    -- So f is increasing on (1,∞)
 264    let f : ℝ → ℝ := fun t => (t - 1) ^ 2 / t
 265    have hf_mono : ∀ a b : ℝ, 1 ≤ a → a < b → f a < f b := by
 266      intro a b ha hab
 267      simp only [f]
 268      have ha0 : (0 : ℝ) < a := by linarith
 269      have hb0 : (0 : ℝ) < b := by linarith
 270      have ha' : a ≠ 0 := ne_of_gt ha0
 271      have hb' : b ≠ 0 := ne_of_gt hb0
 272      rw [div_lt_div_iff₀ ha0 hb0]
 273      -- (a-1)²·b < (b-1)²·a
 274      have : (a - 1) ^ 2 * b - (b - 1) ^ 2 * a < 0 := by
 275        have hcalc : (a - 1) ^ 2 * b - (b - 1) ^ 2 * a = (a - b) * (a * b - 1) := by ring
 276        rw [hcalc]
 277        have h1 : a - b < 0 := by linarith
 278        have h2 : a * b - 1 > 0 := by nlinarith
 279        nlinarith
 280      linarith
 281    have := hf_mono x y hx1 hxy
 282    simp only [f] at this
 283    have hx0' : 0 < x := hx
 284    have hy0' : 0 < y := hy
 285    rw [div_lt_div_iff₀ hx0' hy0'] at this
 286    -- this : (x - 1) ^ 2 * y < (y - 1) ^ 2 * x
 287    -- goal : (x - 1) ^ 2 * (2 * y) < (y - 1) ^ 2 * (2 * x)
 288    have h2 : (0 : ℝ) < 2 := by norm_num
 289    calc (x - 1) ^ 2 * (2 * y)
 290        = 2 * ((x - 1) ^ 2 * y) := by ring
 291      _ < 2 * ((y - 1) ^ 2 * x) := by nlinarith
 292      _ = (y - 1) ^ 2 * (2 * x) := by ring
 293  exact hmain
 294
 295/-- J(x) > 0 for x ≠ 1 and x > 0 -/
 296lemma Jcost_pos_of_ne_one (x : ℝ) (hx : 0 < x) (hx1 : x ≠ 1) : 0 < Jcost x := by
 297  have hx0 : x ≠ 0 := ne_of_gt hx
 298  rw [Jcost_eq_sq hx0]
 299  apply div_pos
 300  · have hne : (x - 1) ≠ 0 := sub_ne_zero.mpr hx1
 301    exact sq_pos_of_ne_zero hne
 302  · have h2 : (0 : ℝ) < 2 := by norm_num
 303    exact mul_pos h2 hx
 304
 305end Cost
 306end IndisputableMonolith
 307