theorem
proved
log_aczel_data_of_laws
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.GeneralizedDAlembert on GitHub at line 158.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
isolates -
G -
G -
kernel -
smooth -
smooth -
G -
G_even_of_reciprocal_symmetry -
via -
back -
IsSymmetric -
of -
continuous_combiner_log_smoothness_bootstrap -
continuous_log_cost_of_continuousOn_positive -
LogAczelData -
mollified -
mollified_pointwise_tendsto -
SatisfiesLawsOfLogicContinuous -
ComparisonOperator -
derivedCost -
excluded_middle_implies_continuous -
identity_implies_normalized -
non_contradiction_and_scale_imply_reciprocal -
identity -
is -
of -
from -
as -
is -
of -
for -
is -
G -
kernel -
of -
is -
Cost -
normalized -
and
formal source
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
162 obtain ⟨P, hPcont, hPsym, hCons⟩ := h.route_independence
163 refine ⟨P, ?_⟩
164 have hFcont : ContinuousOn (derivedCost C) (Set.Ioi (0 : ℝ)) :=
165 excluded_middle_implies_continuous C h.excluded_middle
166 have hNorm : derivedCost C 1 = 0 :=
167 identity_implies_normalized C h.identity
168 have hSymm : IsSymmetric (derivedCost C) :=
169 non_contradiction_and_scale_imply_reciprocal C h.non_contradiction h.scale_invariant
170 refine
171 { continuous_G := continuous_log_cost_of_continuousOn_positive (derivedCost C) hFcont
172 zero_G := by simpa [derivedCost] using hNorm
173 even_G := ?_
174 continuous_P := hPcont
175 symmetric_P := hPsym
176 aczel_eq := ?_ }
177 · exact IndisputableMonolith.Cost.FunctionalEquation.G_even_of_reciprocal_symmetry
178 (derivedCost C) (by intro x hx; exact hSymm x hx)
179 · intro t u
180 have htu_pos : 0 < Real.exp t := Real.exp_pos t
181 have huu_pos : 0 < Real.exp u := Real.exp_pos u
182 have h := hCons (Real.exp t) (Real.exp u) htu_pos huu_pos
183 simpa [Real.exp_add, Real.exp_sub] using h
184
185/-! ## 2b. Piece 1 mollifier scaffold
186
187The former residual `continuous_combiner_log_smoothness_bootstrap` says
188`G(t) = F(exp t)` is `C^∞`. The classical argument is mollification: