 128
 129/-- Log-coordinate Aczél data extracted from a continuous-combiner Law of
 130Logic witness. -/
 131structure LogAczelData (G : ℝ → ℝ) (P : ℝ → ℝ → ℝ) : Prop where
 132  continuous_G : Continuous G
 133  zero_G       : G 0 = 0
 134  even_G       : Function.Even G
 135  continuous_P : Continuous (Function.uncurry P)
 136  symmetric_P  : ∀ u v, P u v = P v u
 137  aczel_eq     : ∀ t u : ℝ, G (t + u) + G (t - u) = P (G t) (G u)
 138
 139/-- Continuity of the derived cost on positive ratios lifts to continuity of
 140the log-coordinate cost `G(t) = F(exp t)`. -/
 141theorem continuous_log_cost_of_continuousOn_positive
 142    (F : ℝ → ℝ)
 143    (hF : ContinuousOn F (Set.Ioi (0 : ℝ))) :
 144    Continuous (fun t : ℝ => F (Real.exp t)) := by
 145  have hExpOn : ContinuousOn (fun t : ℝ => Real.exp t) (Set.univ : Set ℝ) :=
 146    Real.continuous_exp.continuousOn
 147  have hMaps : Set.MapsTo (fun t : ℝ => Real.exp t)
 148      (Set.univ : Set ℝ) (Set.Ioi (0 : ℝ)) := by
 149    intro t ht
 150    exact Real.exp_pos t
 151  have hComp : ContinuousOn (F ∘ fun t : ℝ => Real.exp t) (Set.univ : Set ℝ) :=
 152    hF.comp hExpOn hMaps
 153  have hCont := continuousOn_univ.mp hComp
 154  simpa [Function.comp_def] using hCont
 155
 156/-- The continuous-combiner Law of Logic gives a continuous log-coordinate
 157Aczél equation. This is the formal input object for the smoothness bootstrap. -/
 158theorem log_aczel_data_of_laws
 159    (C : ComparisonOperator) (h : SatisfiesLawsOfLogicContinuous C) :
 160    ∃ P : ℝ → ℝ → ℝ,
 161      LogAczelData (fun t : ℝ => derivedCost C (Real.exp t)) P := by

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.