bernsteinApproximation_uniform
theorem bernsteinApproximation_uniform :
∀ (f : C(↑unitInterval, ℝ)), Filter.Tendsto (fun n => bernsteinApproximation n f) Filter.atTop (nhds f)
The theorem `bernsteinApproximation_uniform` states that for any continuous function `f` defined on the interval `[0,1]` with real values, the Bernstein approximations of `f` tend to `f` uniformly as `n` approaches infinity. Here, the Bernstein approximation of `f` is given by the sum over all `k` in `Fin (n+1)` of `f(k/n) * n.choose k * x^k * (1-x)^(n-k)`. In other words, as we take more and more terms in the Bernstein approximation (i.e., as `n` tends to infinity), the approximation gets closer and closer to the actual function `f` in the sense of uniform convergence. This theorem is proven in Richard Beals' *Analysis, an introduction*, and also mentioned on Wikipedia.
More concisely: For any continuous function `f` on `[0,1]`, the Bernstein polynomials of `f` converge uniformly to `f` as the degree approaches infinity.
|
bernsteinApproximation.lt_of_mem_S
theorem bernsteinApproximation.lt_of_mem_S :
∀ {f : C(↑unitInterval, ℝ)} {ε : ℝ} {h : 0 < ε} {n : ℕ} {x : ↑unitInterval} {k : Fin (n + 1)},
k ∈ bernsteinApproximation.S f ε h n x → |f (bernstein.z k) - f x| < ε / 2
The theorem `bernsteinApproximation.lt_of_mem_S` states that for any continuous function `f` mapping the unit interval to the real numbers, any positive real number `ε`, any natural number `n`, any point `x` in the unit interval, and any `k` in the set `S` (which is defined as the set of points `k` such that `k/n` is within `δ` of `x`), the absolute difference between `f(k/n)` and `f(x)` is less than `ε/2`. In other words, if `k` is in `S`, then the function's value at `k/n` is close to its value at `x`.
More concisely: For any continuous function `f` mapping the unit interval to the real numbers, and for any `x` in the interval, `ε` > 0, and natural number `n`, if `k` is in the set `S` of points such that `|k/n - x| <= δ`, then `|f(k/n) - f(x)| < ε/2`.
|
bernsteinApproximation.le_of_mem_S_compl
theorem bernsteinApproximation.le_of_mem_S_compl :
∀ {f : C(↑unitInterval, ℝ)} {ε : ℝ} {h : 0 < ε} {n : ℕ} {x : ↑unitInterval} {k : Fin (n + 1)},
k ∈ (bernsteinApproximation.S f ε h n x)ᶜ →
1 ≤ bernsteinApproximation.δ f ε h ^ (-2) * (↑x - ↑(bernstein.z k)) ^ 2
The theorem `bernsteinApproximation.le_of_mem_S_compl` states that for a continuous function `f` from the unit interval `[0,1]` to real numbers `ℝ`, given a positive real number `ε`, a natural number `n`, a point `x` in the unit interval, and a point `k` from the set of equally spaced points in the unit interval (defined by `bernstein.z`), if `k` is not in the set `S` (which contains points `k` such that `k/n` is within `δ` of `x`), then the inequality `1 ≤ δ^-2 * (x - k/n)^2` holds. Here, `δ` is the modulus of (uniform) continuity for `f`, chosen so `|f(x) - f(y)| < ε/2` when `|x - y| < δ`. This particular formulation will be useful in subsequent proofs.
More concisely: For a continuous function `f` on `[0,1]`, given `ε > 0`, `n > 0`, `x ∈ [0,1]`, `k ∈ [0,1]` not in `S` where `S = {k/n | k ∈ ℕ, |k/n - x| < δ}`, and `δ` is the modulus of continuity for `f` such that `|f(x) - f(y)| < ε/2` for `|x - y| < δ`, the inequality `1 ≤ δ² * (x - k/n)²` holds.
|