theorem
proved
term proof
primitive_to_uniqueness_of_kernel
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Term-mode proof.
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. -/
used by (2)
depends on (33)
-
H -
reciprocal -
of -
kernel -
AczelRegularityKernel -
H_continuous_of_positive_continuous -
H_dAlembert_of_composition -
H_one_of_normalized -
PrimitiveCostHypotheses -
smooth -
smooth -
H -
ode_regularity_bootstrap_of_smooth -
ode_regularity_continuous_of_smooth -
ode_regularity_differentiable_of_smooth -
washburn_uniqueness -
ode_regularity_bootstrap_of_smooth -
ode_regularity_continuous_of_smooth -
ode_regularity_differentiable_of_smooth -
canonical -
of -
reciprocal -
of -
of -
canonical -
kernel -
of -
Cost -
canonical -
normalized