Jcost_continuous_pos

formal source

 127  ode_bootstrap : FunctionalEquation.ode_linear_regularity_bootstrap_hypothesis (FunctionalEquation.H F)
 128
 129/-- Jcost is continuous on ℝ₊ -/
 130lemma Jcost_continuous_pos : ContinuousOn Jcost (Ioi 0) := by
 131  classical
 132  have h1 : ContinuousOn (fun x : ℝ => x) (Ioi 0) := continuousOn_id
 133  have h2 : ContinuousOn (fun x : ℝ => x⁻¹) (Ioi 0) := by
 134    refine ContinuousOn.inv₀ (f:=fun x : ℝ => x) (s:=Ioi 0) h1 ?hneq
 135    intro x hx; exact ne_of_gt hx
 136  have h3 : ContinuousOn (fun x : ℝ => x + x⁻¹) (Ioi 0) := h1.add h2
 137  have h4 : ContinuousOn (fun x : ℝ => (1 / 2 : ℝ) * (x + x⁻¹)) (Ioi 0) :=
 138    (continuousOn_const).mul h3
 139  have h5 : ContinuousOn (fun x : ℝ => (1 / 2 : ℝ) * (x + x⁻¹) - 1) (Ioi 0) :=
 140    h4.sub continuousOn_const
 141  simpa [Jcost, one_div, div_eq_mul_inv, mul_comm, mul_left_comm, mul_assoc, sub_eq_add_neg]
 142    using h5
 143
 144/-- `Jcost` satisfies reciprocal symmetry in the theorem-surface format. -/
 145theorem Jcost_is_reciprocal : FunctionalEquation.IsReciprocalCost Jcost :=
 146  fun x hx => Jcost_symm hx
 147
 148/-- `Jcost` is normalized at `1`. -/
 149theorem Jcost_is_normalized : FunctionalEquation.IsNormalized Jcost :=
 150  Jcost_unit0
 151
 152/-- `Jcost` satisfies the Recognition Composition Law. -/
 153theorem Jcost_satisfies_composition_law : FunctionalEquation.SatisfiesCompositionLaw Jcost :=
 154  (FunctionalEquation.composition_law_equiv_coshAdd Jcost).2 FunctionalEquation.Jcost_cosh_add_identity
 155
 156/-- `Jcost` satisfies the standard calibration condition in log coordinates. -/
 157theorem Jcost_is_calibrated : FunctionalEquation.IsCalibrated Jcost := by
 158  change deriv (deriv (fun t : ℝ => Jcost (Real.exp t))) 0 = 1
 159  exact IndisputableMonolith.CPM.LawOfExistence.RS.Jcost_log_second_deriv_normalized
 160