Theorems · Theorem · approximation theory

bernsteinApproximation_uniform

∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [inst_2 : IsTopologicalAddGroup E]
  [inst_3 : Module ℝ E] [inst_4 : ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] (f : C(↑unitInterval, E)),
  Filter.Tendsto (fun n => bernsteinApproximation n f) Filter.atTop (nhds f)

The Bernstein approximations `` ∑ k : Fin (n+1), f (k/n : ℝ) * n.choose k * x^k * (1-x)^(n-k) ` for a continuous function f : C([0,1], ℝ) converge uniformly to f as n` tends to infinity. This is the proof given in [Richard Beals' Analysis, an introduction][beals-analysis], §7D, and reproduced on wikipedia.

Defined in

Mathlib.Analysis.SpecialFunctions.Bernstein

Cited by

1 results in Mathlib

Foundations

Depth 167 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommGroupTopologicalSpaceIsTopologicalAddGroupModuleContinuousSMulLocallyConvexSpace