primitive_to_uniqueness_of_kernel

formal source

  93The public statement now takes the primitive cost hypotheses directly and uses
  94`AczelRegularityKernel` as the sole regularity bridge. This makes the T5 seam
  95explicit without routing through `JensenSketch`. -/
  96theorem primitive_to_uniqueness_of_kernel (F : ℝ → ℝ)
  97    (hF : PrimitiveCostHypotheses F)
  98    (hKernel : AczelRegularityKernel (H F)) :
  99    ∀ x : ℝ, 0 < x → F x = Cost.Jcost x := by
 100  have h_H0 : H F 0 = 1 := H_one_of_normalized F hF.normalized
 101  have h_H_cont : Continuous (H F) :=
 102    H_continuous_of_positive_continuous F hF.continuous
 103  have h_H_dAlembert : ∀ t u, H F (t + u) + H F (t - u) = 2 * H F t * H F u :=
 104    H_dAlembert_of_composition F hF.composition
 105  have h_smooth : ContDiff ℝ ⊤ (H F) :=
 106    hKernel.smooth h_H0 h_H_cont h_H_dAlembert
 107  exact washburn_uniqueness F
 108    hF.reciprocal hF.normalized hF.composition hF.calibrated hF.continuous
 109    hKernel.smooth hKernel.ode
 110    (ode_regularity_continuous_of_smooth h_smooth)
 111    (ode_regularity_differentiable_of_smooth h_smooth)
 112    (ode_regularity_bootstrap_of_smooth h_smooth)
 113
 114/-- Convenience form of the canonical T5 theorem using the current Aczél
 115smoothness package to supply the regularity kernel automatically. -/
 116theorem primitive_to_uniqueness_aczel [AczelSmoothnessPackage] (F : ℝ → ℝ)
 117    (hF : PrimitiveCostHypotheses F) :
 118    ∀ x : ℝ, 0 < x → F x = Cost.Jcost x :=
 119  primitive_to_uniqueness_of_kernel F hF (aczelRegularityKernel (H F))
 120
 121end FunctionalEquation
 122end Cost
 123end IndisputableMonolith