pith. machine review for the scientific record. sign in
theorem proved tactic proof

log_aczel_data_of_laws

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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

proof body

Tactic-mode proof.

 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:
 189convolve `G` with a `ContDiffBump` kernel to produce a smooth approximant
 190`G_φ` and then push smoothness back to `G` through the Aczél equation.
 191
 192The scaffold below packages the parts Mathlib hands us for free and
 193isolates the genuine analytic content for later work.
 194
 195In this section we prove:
 196
 197* `mollified G φ` exists as a measurable function and is continuous.
 198* `mollified_pointwise_tendsto`: as the bump support shrinks, the
 199  mollification converges to `G` pointwise (via Mathlib's
 200  `ContDiffBump.convolution_tendsto_right_of_continuous`).
 201
 202Smoothness of `G` itself still needs the equation-side argument, but
 203`G_φ` already inherits arbitrary regularity from the bump kernel.
 204-/
 205
 206open scoped Convolution
 207open MeasureTheory
 208
 209/-- Mollification of a continuous function on `ℝ` by a normalized
 210`ContDiffBump` kernel, written as a left convolution to align with
 211`ContDiffBump.convolution_tendsto_right_of_continuous`. -/

depends on (40)

Lean names referenced from this declaration's body.

… and 10 more