feat(analysis/special_functions/bernstein): Weierstrass' theorem: pol…

…ynomials are dense in C([0,1]) (#6497)

# Bernstein approximations and Weierstrass' theorem

We prove that 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.

Our proof follows Richard Beals' *Analysis, an introduction*, §7D.
The original proof, due to Bernstein in 1912, is probabilistic,
and relies on Bernoulli's theorem,
which gives bounds for how quickly the observed frequencies in a
Bernoulli trial approach the underlying probability.

The proof here does not directly rely on Bernoulli's theorem,
but can also be given a probabilistic account.
* Consider a weighted coin which with probability `x` produces heads,
  and with probability `1-x` produces tails.
* The value of `bernstein n k x` is the probability that
  such a coin gives exactly `k` heads in a sequence of `n` tosses.
* If such an appearance of `k` heads results in a payoff of `f(k / n)`,
  the `n`-th Bernstein approximation for `f` evaluated at `x` is the expected payoff.
* The main estimate in the proof bounds the probability that
  the observed frequency of heads differs from `x` by more than some `δ`,
  obtaining a bound of `(4 * n * δ^2)⁻¹`, irrespective of `x`.
* This ensures that for `n` large, the Bernstein approximation is (uniformly) close to the
  payoff function `f`.

(You don't need to think in these terms to follow the proof below: it's a giant `calc` block!)

This result proves Weierstrass' theorem that polynomials are dense in `C([0,1], ℝ)`,
although we defer an abstract statement of this until later.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

docs/references.bib

@@ -80,6 +80,23 @@ @Book{            axler2015
   publisher     = {Springer}
 }
 
+@Book{            beals2004,
+  author        = {Richard Beals},
+  title         = {Analysis. An introduction},
+  publisher     = {Cambridge University Press},
+  isbn          = {0521600472},
+  year          = {2004},
+}
+
+@article{         bernstein1912,
+  author        = {Bernstein, S.},
+  year          = {1912},
+  title         = {Démonstration du théorème de Weierstrass fondée sur le calcul des probabilités},
+  journal       = {Comm. Kharkov Math. Soc.},
+  volume        = {13},
+  number        = {1–2},
+}
+
 @Book{            borceux-vol1,
   title         = {Handbook of Categorical Algebra: Volume 1, Basic Category
                   Theory},

src/algebra/big_operators/order.lean

@@ -43,7 +43,7 @@ end
 
 /-- Let `{x | p x}` be an additive subsemigroup of an additive commutative monoid `M`. Let `f : M →
 N` be a map subadditive on `{x | p x}`, i.e., `p x → p y → f (x + y) ≤ f x + f y`. Let `g i`, `i ∈
-s`, be a nonempty finite family of elements of `M` such that `∀ i ∈ s, p (g i)`. Then 
+s`, be a nonempty finite family of elements of `M` such that `∀ i ∈ s, p (g i)`. Then
 `f (∑ i in s, g i) ≤ ∏ i in s, f (g i)`. -/
 add_decl_doc le_sum_nonempty_of_subadditive_on_pred
 
@@ -136,6 +136,11 @@ calc (∏ i in s, f i) ≤ (∏ i in t \ s, f i) * (∏ i in s, f i) :
 lemma prod_mono_set_of_one_le' (hf : ∀ x, 1 ≤ f x) : monotone (λ s, ∏ x in s, f x) :=
 λ s t hst, prod_le_prod_of_subset_of_one_le' hst $ λ x _ _, hf x
 
+@[to_additive sum_le_univ_sum_of_nonneg]
+lemma prod_le_univ_prod_of_one_le' [fintype ι] {s : finset ι} (w : ∀ x, 1 ≤ f x) :
+  ∏ x in s, f x ≤ ∏ x, f x :=
+prod_le_prod_of_subset_of_one_le' (subset_univ s) (λ a _ _, w a)
+
 @[to_additive sum_eq_zero_iff_of_nonneg]
 lemma prod_eq_one_iff_of_one_le' : (∀ i ∈ s, 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ i ∈ s, f i = 1) :=
 begin

src/algebra/group_power/basic.lean

@@ -690,11 +690,11 @@ by simpa only [sqr_abs] using pow_lt_pow_of_lt_left h (abs_nonneg x) (1:ℕ).suc
 theorem sqr_lt_sqr' (h1 : -y < x) (h2 : x < y) : x ^ 2 < y ^ 2 :=
 sqr_lt_sqr (abs_lt.mpr ⟨h1, h2⟩)
 
-theorem sqr_le_sqr (h : abs x ≤ y) : x ^ 2 ≤ y ^ 2 :=
+theorem sqr_le_sqr (h : abs x ≤ abs y) : x ^ 2 ≤ y ^ 2 :=
 by simpa only [sqr_abs] using pow_le_pow_of_le_left (abs_nonneg x) h 2
 
 theorem sqr_le_sqr' (h1 : -y ≤ x) (h2 : x ≤ y) : x ^ 2 ≤ y ^ 2 :=
-sqr_le_sqr (abs_le.mpr ⟨h1, h2⟩)
+sqr_le_sqr (le_trans (abs_le.mpr ⟨h1, h2⟩) (le_abs_self _))
 
 theorem abs_lt_abs_of_sqr_lt_sqr (h : x^2 < y^2) : abs x < abs y :=
 lt_of_pow_lt_pow 2 (abs_nonneg y) $ by rwa [← sqr_abs x, ← sqr_abs y] at h

src/algebra/group_with_zero/basic.lean

@@ -392,6 +392,14 @@ calc a⁻¹ * a = (a⁻¹ * a) * a⁻¹ * a⁻¹⁻¹ : by simp [inv_ne_zero h]
          ... = a⁻¹ * a⁻¹⁻¹             : by simp [h]
          ... = 1                       : by simp [inv_ne_zero h]
 
+lemma group_with_zero.mul_left_injective {x : G₀} (h : x ≠ 0) :
+  function.injective (λ y, x * y) :=
+λ y y' w, by simpa only [←mul_assoc, inv_mul_cancel h, one_mul] using congr_arg (λ y, x⁻¹ * y) w
+
+lemma group_with_zero.mul_right_injective {x : G₀} (h : x ≠ 0) :
+  function.injective (λ y, y * x) :=
+λ y y' w, by simpa only [mul_assoc, mul_inv_cancel h, mul_one] using congr_arg (λ y, y * x⁻¹) w
+
 @[simp] lemma inv_mul_cancel_right' {b : G₀} (h : b ≠ 0) (a : G₀) :
   (a * b⁻¹) * b = a :=
 calc (a * b⁻¹) * b = a * (b⁻¹ * b) : mul_assoc _ _ _

src/algebra/group_with_zero/power.lean

@@ -267,3 +267,17 @@ lemma monoid_with_zero_hom.map_fpow {G₀ G₀' : Type*} [group_with_zero G₀]
   ∀ n : ℤ, f (x ^ n) = f x ^ n
 | (n : ℕ) := f.to_monoid_hom.map_pow x n
 | -[1+n] := (f.map_inv' _).trans $ congr_arg _ $ f.to_monoid_hom.map_pow x _
+
+-- I haven't been able to find a better home for this:
+-- it belongs with other lemmas on `linear_ordered_field`, but
+-- we need to wait until `fpow` has been defined in this file.
+section
+variables {R : Type*} [linear_ordered_field R] {a : R}
+
+lemma pow_minus_two_nonneg : 0 ≤ a^(-2 : ℤ) :=
+begin
+  simp only [inv_nonneg, fpow_neg],
+  apply pow_two_nonneg,
+end
+
+end

src/algebra/ordered_monoid.lean

@@ -820,6 +820,9 @@ instance canonically_ordered_monoid.has_exists_mul_of_le (α : Type u)
 
 end canonically_ordered_monoid
 
+lemma pos_of_gt {M : Type*} [canonically_ordered_add_monoid M] {n m : M} (h : n < m) : 0 < m :=
+lt_of_le_of_lt (zero_le _) h
+
 /-- A canonically linear-ordered additive monoid is a canonically ordered additive monoid
     whose ordering is a linear order. -/
 @[protect_proj, ancestor canonically_ordered_add_monoid linear_order]

src/algebra/ordered_ring.lean

@@ -82,6 +82,10 @@ calc
   a * b ≤ c * b : mul_le_mul_of_nonneg_right hac nn_b
     ... ≤ c * d : mul_le_mul_of_nonneg_left hbd nn_c
 
+lemma mul_nonneg_le_one_le {α : Type*} [ordered_semiring α] {a b c : α}
+  (h₁ : 0 ≤ c) (h₂ : a ≤ c) (h₃ : 0 ≤ b) (h₄ : b ≤ 1) : a * b ≤ c :=
+by simpa only [mul_one] using mul_le_mul h₂ h₄ h₃ h₁
+
 lemma mul_nonneg (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a * b :=
 have h : 0 * b ≤ a * b, from mul_le_mul_of_nonneg_right ha hb,
 by rwa [zero_mul] at h