English
Let f be a continuous function on the unit interval I = [0,1] taking values in a locally convex real space E. Then the Bernstein approximations converge uniformly to f as the degree n tends to infinity.
Русский
Пусть f непрерывна на единичном интервале I = [0,1] и принимает значения в локально выпуклом вещественном пространстве E. Тогда бернштейновы аппроксимации сходятся по униформной метрике к f при росте степени n.
LaTeX
$$$\lim_{n\to\infty} \sup_{x\in [0,1]} \|\mathrm{bernsteinApproximation}_n f(x) - f(x)\| = 0$$$
Lean4
/-- 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.
-/
theorem bernsteinApproximation_uniform [LocallyConvexSpace ℝ E] (f : C(I, E)) :
Tendsto (fun n : ℕ => bernsteinApproximation n f) atTop (𝓝 f) :=
by
letI : UniformSpace E := IsTopologicalAddGroup.toUniformSpace E
have : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup
suffices ∀ U ∈ 𝓝 (0 : E), Convex ℝ U → ∀ᶠ n in atTop, ∀ x : I, gauge U (bernsteinApproximation n f x - f x) < 1
by
rw [(LocallyConvexSpace.convex_basis_zero ℝ
E).uniformity_of_nhds_zero_swapped |>.compactConvergenceUniformity_of_compact |>
nhds_basis_uniformity |>.tendsto_right_iff]
rintro U ⟨hU₀, hcU⟩
filter_upwards [this U hU₀ hcU] with n hn x
exact gauge_lt_one_subset_self hcU (mem_of_mem_nhds hU₀) (absorbent_nhds_zero hU₀) (hn x)
intro U hU₀ hUc
obtain ⟨C, hC⟩ : ∃ C, ∀ x y, gauge U (f x - f y) ≤ C :=
by
have : Continuous fun (x, y) ↦ gauge U (f x - f y) := by fun_prop (disch := assumption)
simpa only [BddAbove, Set.Nonempty, mem_upperBounds, Set.forall_mem_range, Prod.forall] using
isCompact_range this |>.bddAbove
have hC₀ : 0 ≤ C :=
le_trans (gauge_nonneg _)
(hC 0 0)
/- Use uniform continuity of `f` to hcoose `δ > 0` such that `‖f x - f y‖_U < 1 / 2`
whenever `dist x y < δ`. -/
obtain ⟨δ, hδ₀, hδ⟩ : ∃ δ > 0, ∀ x y : I, dist x y < δ → gauge U (f x - f y) < 1 / 2 :=
by
have := CompactSpace.uniformContinuous_of_continuous (map_continuous f)
rw [Metric.uniformity_basis_dist.uniformContinuous_iff (basis_sets _).uniformity_of_nhds_zero_swapped] at this
exact
this {z | gauge U z < 1 / 2} <|
tendsto_gauge_nhds_zero hU₀ |>.eventually_lt_const <| by
positivity
-- Take `n ≠ 0` such that `C / δ ^ 2 / n < 1 / 2`.
have nhds_zero := tendsto_const_div_atTop_nhds_zero_nat (C / δ ^ 2)
filter_upwards [nhds_zero.eventually_lt_const (half_pos one_pos), eventually_ne_atTop 0] with n nh hn₀ x
set S : Finset (Fin (n + 1)) := {k : Fin (n + 1) | dist k/ₙ x < δ}
calc
gauge U (bernsteinApproximation n f x - f x) = gauge U (∑ k : Fin (n + 1), bernstein n k x • (f k/ₙ - f x)) := by
simp [bernsteinApproximation.apply, smul_sub, ← Finset.sum_smul]
_ ≤ ∑ k : Fin (n + 1), gauge U (bernstein n k x • (f k/ₙ - f x)) := (gauge_sum_le hUc (absorbent_nhds_zero hU₀) _ _)
_ = ∑ k : Fin (n + 1), bernstein n k x * gauge U (f k/ₙ - f x) := by
simp only [gauge_smul_of_nonneg, bernstein_nonneg, smul_eq_mul]
_ = (∑ k ∈ S, bernstein n k x * gauge U (f k/ₙ - f x)) + ∑ k ∈ Sᶜ, bernstein n k x * gauge U (f k/ₙ - f x) :=
(S.sum_add_sum_compl _).symm
_ < 1 / 2 + 1 / 2 := (add_lt_add_of_le_of_lt ?_ ?_)
_ = 1 := add_halves 1
· -- We now work on the terms in `S`: uniform continuity and `bernstein.probability`
-- quickly give us a bound.
calc
∑ k ∈ S, bernstein n k x * gauge U (f k/ₙ - f x) ≤ ∑ k ∈ S, bernstein n k x * (1 / 2) :=
by
gcongr with k hk
refine (hδ _ _ ?_).le
simpa [S] using hk
_ = 1 / 2 * ∑ k ∈ S, bernstein n k x := by
rw [mul_comm, Finset.sum_mul]
-- In this step we increase the sum over `S` back to a sum over all of `Fin (n+1)`,
-- so that we can use `bernstein.probability`.
_ ≤ 1 / 2 * ∑ k : Fin (n + 1), bernstein n k x := by gcongr; exact S.subset_univ
_ = 1 / 2 := by rw [bernstein.probability, mul_one]
· -- We now turn to working on `Sᶜ`: we control the difference term just using `C`,
-- and then insert a `(x - k/n)^2 / δ^2` factor
-- (which is at least one because we are not in `S`).
calc
∑ k ∈ Sᶜ, bernstein n k x * gauge U (f k/ₙ - f x) ≤ ∑ k ∈ Sᶜ, C * bernstein n k x :=
by
simp only [mul_comm (bernstein n _ x)]
gcongr
apply hC
_ = C * ∑ k ∈ Sᶜ, bernstein n k x := by rw [Finset.mul_sum]
_ ≤ C * ∑ k ∈ Sᶜ, ((x : ℝ) - k/ₙ) ^ 2 / δ ^ 2 * bernstein n k x :=
by
gcongr with k hk
conv_lhs => rw [← one_mul (bernstein _ _ _)]
gcongr
simpa [one_le_div₀, hδ₀, sq_le_sq, S, abs_of_pos, ← Real.dist_eq, dist_comm (x : ℝ)] using hk
_ ≤ C * ∑ k : Fin (n + 1), ((x : ℝ) - k/ₙ) ^ 2 / δ ^ 2 * bernstein n k x := by gcongr; exact Sᶜ.subset_univ
_ = C * (∑ k : Fin (n + 1), ((x : ℝ) - k/ₙ) ^ 2 * bernstein n k x) / δ ^ 2 := by
simp only [← mul_div_right_comm, ← mul_div_assoc, ← Finset.sum_div]
-- `bernstein.variance` and `x ∈ [0,1]` gives the uniform bound
_ = C / δ ^ 2 * x * (1 - x) / n := by rw [variance hn₀]; ring
_ ≤ C / δ ^ 2 * 1 * 1 / n := by gcongr <;> unit_interval
_ < 1 / 2 := by simpa only [mul_one]
