IndisputableMonolith.Cost.FlogEL

   1import Mathlib
   2import IndisputableMonolith.Cost
   3
   4namespace IndisputableMonolith
   5namespace Cost
   6
   7/-- Log-domain cost: Jcost composed with exp -/
   8noncomputable def Jlog (t : ℝ) : ℝ := Jcost (Real.exp t)
   9
  10lemma Jlog_eq_zero_iff (t : ℝ) : Jlog t = 0 ↔ t = 0 := by
  11  simp [Jlog, Jcost_unit0]
  12  have h : Real.exp t = 1 ↔ t = 0 := Real.exp_eq_one_iff
  13  exact h
  14
  15lemma Jlog_nonneg (t : ℝ) : 0 ≤ Jlog t := by
  16  simp [Jlog]
  17  -- Jcost is nonnegative: for x > 0, by AM-GM: x + 1/x ≥ 2, so 1/2(x + 1/x) - 1 ≥ 0
  18  have hx : 0 < Real.exp t := Real.exp_pos t
  19  have hamgm : Real.exp t + (Real.exp t)⁻¹ ≥ 2 := by
  20    have := Real.add_ge_two_mul_sqrt (Real.exp t) (Real.exp t)⁻¹
  21    · simp at this; exact this
  22    · exact hx
  23    · have : 0 < (Real.exp t)⁻¹ := inv_pos.mpr hx
  24      exact this
  25  calc
  26    Jcost (Real.exp t) = (1/2) * (Real.exp t + (Real.exp t)⁻¹) - 1 := rfl
  27    _ ≥ (1/2) * 2 - 1 := mul_le_mul_of_nonneg_left hamgm (by norm_num)
  28    _ = 0 := by norm_num
  29
  30lemma hasDerivAt_Jlog (t : ℝ) : HasDerivAt Jlog (Real.sinh t) t := by
  31  -- Jlog(t) = Jcost (exp t) = (exp t + exp (-t))/2 - 1 = cosh t - 1
  32  have hcosh : HasDerivAt Real.cosh (Real.sinh t) t := Real.hasDerivAt_cosh t
  33  have h : HasDerivAt (fun s => Real.cosh s - 1) (Real.sinh t) t := hcosh.sub_const 1
  34  -- Identify Jlog with cosh − 1 pointwise
  35  have heq : (fun s => Jlog s) = (fun s => Real.cosh s - 1) := by
  36    funext s
  37    unfold Jlog
  38    -- Jcost (exp s) = ((exp s) + (exp s)⁻¹)/2 - 1 and (exp s)⁻¹ = exp (−s)
  39    simp [Jcost, Real.cosh, Real.exp_neg]
  40  simpa [heq]
  41
  42/-- Typeclass for averaging derivation -/
  43class AveragingDerivation (F : ℝ → ℝ) : Prop extends SymmUnit F where
  44  agrees : ∀ t : ℝ, F (Real.exp t) = Jcost (Real.exp t)
  45
  46/-- Flog definition -/
  47noncomputable def Flog (F : ℝ → ℝ) (t : ℝ) : ℝ := F (Real.exp t)
  48
  49lemma Flog_eq_Jlog_pt {F : ℝ → ℝ} [AveragingDerivation F] (t : ℝ) :
  50  Flog F t = Jlog t := by
  51  dsimp [Flog, Jlog]
  52  exact AveragingDerivation.agrees t
  53
  54lemma Flog_eq_Jlog {F : ℝ → ℝ} [AveragingDerivation F] :
  55  (fun t => Flog F t) = Jlog := by
  56  funext t; simpa using (Flog_eq_Jlog_pt (F:=F) t)
  57
  58lemma hasDerivAt_Flog_of_derivation {F : ℝ → ℝ} [AveragingDerivation F] (t : ℝ) :
  59  HasDerivAt (Flog F) (Real.sinh t) t := by
  60  have h := hasDerivAt_Jlog t
  61  have hfun := (Flog_eq_Jlog (F:=F))
  62  -- rewrite derivative of Jlog to derivative of Flog via function equality
  63  simpa [hfun] using h
  64
  65@[simp] lemma deriv_Flog_zero_of_derivation {F : ℝ → ℝ} [AveragingDerivation F] :
  66  deriv (Flog F) 0 = 0 := by
  67  classical
  68  simpa using (hasDerivAt_Flog_of_derivation (F:=F) 0).deriv
  69
  70lemma Flog_nonneg_of_derivation {F : ℝ → ℝ} [AveragingDerivation F] (t : ℝ) :
  71  0 ≤ Flog F t := by
  72  have := Jlog_nonneg t
  73  simpa [Flog_eq_Jlog_pt (F:=F) t] using this
  74
  75lemma Flog_eq_zero_iff_of_derivation {F : ℝ → ℝ} [AveragingDerivation F] (t : ℝ) :
  76  Flog F t = 0 ↔ t = 0 := by
  77  have := Jlog_eq_zero_iff t
  78  simpa [Flog_eq_Jlog_pt (F:=F) t] using this
  79
  80theorem T5_EL_equiv_general {F : ℝ → ℝ} [AveragingDerivation F] :
  81  deriv (Flog F) 0 = 0 ∧ (∀ t : ℝ, Flog F 0 ≤ Flog F t) ∧ (∀ t : ℝ, Flog F t = 0 ↔ t = 0) := by
  82  refine ⟨deriv_Flog_zero_of_derivation (F:=F), ?_, ?_⟩
  83  · intro t; exact Flog_nonneg_of_derivation (F:=F) t
  84  · intro t; exact Flog_eq_zero_iff_of_derivation (F:=F) t
  85
  86end Cost
  87end IndisputableMonolith
  88