Formal target: Corpus.PaperVoronovskajaTypeFormula.voronovskaja_theorem.bezier_bernstein_operators.variants.eventually_smooth.limit_exists
Existence-only version of the eventual-smoothness variant.
Exact formal statement
∀ (α : Real),
LT.lt.{0} 0 α →
Ne.{1} α 1 →
Filter.Eventually.{0}
(fun m =>
∀ (f : Real → Real) (x : Real),
Membership.mem.{0, 0} unitInterval x →
ContDiffOn.{0, 0, 0} Real (Nat.cast.{0} m) f unitInterval →
Exists.{1} fun L =>
Filter.Tendsto.{0, 0}
(fun n =>
HMul.hMul.{0, 0, 0} (Nat.cast.{0} n).sqrt
(HSub.hSub.{0, 0, 0} (Corpus.PaperVoronovskajaTypeFormula.bezierBernstein n α f x) (f x)))
Filter.atTop.{0} (nhds.{0} L))
Filter.atTop.{0}This target is a formal statement, not a proof of the problem.
Environment availability: available.