continuous_combiner_log_smoothness_bootstrap

formal source

 514upgrades to the original `C^∞` smoothness statement. The old broad axiom is
 515now a theorem; the remaining named input is the finite-order derivative
 516control above. -/
 517theorem continuous_combiner_log_smoothness_bootstrap
 518    (C : ComparisonOperator)
 519    (h : SatisfiesLawsOfLogicContinuous C)
 520    (hFinite : ContinuousCombinerMollifierFiniteSmoothness C h) :
 521    ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞)
 522      (fun t : ℝ => derivedCost C (Real.exp t)) := by
 523  exact continuous_combiner_finite_smoothness_to_top C h hFinite
 524
 525/-- The second-derivative identity extracted from the smooth Aczél equation.
 526The function `ψ` is morally `∂₂ P(u, 0)`. -/
 527def AczelSecondDerivativeIdentity (G : ℝ → ℝ) : Prop :=
 528  ∃ ψ : ℝ → ℝ,
 529    ∀ t : ℝ, 2 * deriv (deriv G) t = ψ (G t) * deriv (deriv G) 0
 530
 531/-- Affineness of `ψ` on the image of the log-cost. -/
 532def PsiAffineOnImage (G : ℝ → ℝ) (ψ : ℝ → ℝ) : Prop :=
 533  ∃ c : ℝ, ∀ t : ℝ, ψ (G t) = 2 + c * G t
 534
 535/-- **Named analysis input 2a: derivative identity for the combiner equation.**
 536
 537This is the first differentiating step in the Stetkær/Aczél proof: from a
 538smooth log-coordinate Aczél equation, extract
 539`2 G''(t) = ψ(G(t)) G''(0)`.
 540
 541This is not a theorem under the present hypotheses: the quartic log-cost
 542obstruction is formalized in
 543`Foundation.GeneralizedDAlembert.SecondDerivative`. -/
 544def ContinuousCombinerSecondDerivativeInput
 545    (C : ComparisonOperator)
 546    (_h : SatisfiesLawsOfLogicContinuous C)
 547    (_hSmooth : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞)