ContinuousCombinerMollifierFiniteSmoothness

formal source

 490the bump family exists and converges pointwise by theorem above; what remains
 491is controlling derivatives on compact intervals strongly enough to pass the
 492limit back to `G`. -/
 493def ContinuousCombinerMollifierFiniteSmoothness
 494    (C : ComparisonOperator)
 495    (_h : SatisfiesLawsOfLogicContinuous C) : Prop :=
 496    ∀ n : ℕ, ContDiff ℝ n (fun t : ℝ => derivedCost C (Real.exp t))
 497
 498/-- **Residual input 1b: finite-order smoothness promotes to full top-level
 499smoothness for this log-cost.**
 500
 501Lean's `ContDiff` index used by Mathlib distinguishes the imported `⊤ : ℕ∞`
 502from the outer `⊤ : WithTop ℕ∞` expected by downstream APIs. This input is the
 503formal promotion step from the finite-order certificates produced by the
 504mollifier route to the top-level smoothness statement consumed below. -/
 505theorem continuous_combiner_finite_smoothness_to_top
 506    (C : ComparisonOperator)
 507    (_h : SatisfiesLawsOfLogicContinuous C)
 508    (hFinite : ∀ n : ℕ, ContDiff ℝ n (fun t : ℝ => derivedCost C (Real.exp t))) :
 509    ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞)
 510      (fun t : ℝ => derivedCost C (Real.exp t)) := by
 511  exact SmoothnessTop.contDiff_top_of_contDiff_nat hFinite
 512
 513/-- **Residual input 1 assembled:** finite-order mollifier derivative control
 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