[GOAL]
n ν : ℕ
x : ↑I
⊢ ↑(bernstein n ν) x = ↑(Nat.choose n ν) * ↑x ^ ν * (1 - ↑x) ^ (n - ν)
[PROOFSTEP]
dsimp [bernstein, Polynomial.toContinuousMapOn, Polynomial.toContinuousMap, bernsteinPolynomial]
[GOAL]
n ν : ℕ
x : ↑I
⊢ Polynomial.eval (↑x) (↑(Nat.choose n ν) * Polynomial.X ^ ν * (1 - Polynomial.X) ^ (n - ν)) =
    ↑(Nat.choose n ν) * ↑x ^ ν * (1 - ↑x) ^ (n - ν)
[PROOFSTEP]
simp
[GOAL]
n ν : ℕ
x : ↑I
⊢ 0 ≤ ↑(bernstein n ν) x
[PROOFSTEP]
simp only [bernstein_apply]
[GOAL]
n ν : ℕ
x : ↑I
⊢ 0 ≤ ↑(Nat.choose n ν) * ↑x ^ ν * (1 - ↑x) ^ (n - ν)
[PROOFSTEP]
have h₁ : (0 : ℝ) ≤ x := by unit_interval
[GOAL]
n ν : ℕ
x : ↑I
⊢ 0 ≤ ↑x
[PROOFSTEP]
unit_interval
[GOAL]
n ν : ℕ
x : ↑I
h₁ : 0 ≤ ↑x
⊢ 0 ≤ ↑(Nat.choose n ν) * ↑x ^ ν * (1 - ↑x) ^ (n - ν)
[PROOFSTEP]
have h₂ : (0 : ℝ) ≤ 1 - x := by unit_interval
[GOAL]
n ν : ℕ
x : ↑I
h₁ : 0 ≤ ↑x
⊢ 0 ≤ 1 - ↑x
[PROOFSTEP]
unit_interval
[GOAL]
n ν : ℕ
x : ↑I
h₁ : 0 ≤ ↑x
h₂ : 0 ≤ 1 - ↑x
⊢ 0 ≤ ↑(Nat.choose n ν) * ↑x ^ ν * (1 - ↑x) ^ (n - ν)
[PROOFSTEP]
positivity
[GOAL]
n : ℕ
k : Fin (n + 1)
⊢ ↑↑k / ↑n ∈ I
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
k : Fin (Nat.zero + 1)
⊢ ↑↑k / ↑Nat.zero ∈ I
[PROOFSTEP]
norm_num
[GOAL]
case succ
n : ℕ
k : Fin (Nat.succ n + 1)
⊢ ↑↑k / ↑(Nat.succ n) ∈ I
[PROOFSTEP]
have h₁ : 0 < (n.succ : ℝ) := by exact_mod_cast Nat.succ_pos _
[GOAL]
n : ℕ
k : Fin (Nat.succ n + 1)
⊢ 0 < ↑(Nat.succ n)
[PROOFSTEP]
exact_mod_cast Nat.succ_pos _
[GOAL]
case succ
n : ℕ
k : Fin (Nat.succ n + 1)
h₁ : 0 < ↑(Nat.succ n)
⊢ ↑↑k / ↑(Nat.succ n) ∈ I
[PROOFSTEP]
have h₂ : ↑k ≤ n.succ := by exact_mod_cast Fin.le_last k
[GOAL]
n : ℕ
k : Fin (Nat.succ n + 1)
h₁ : 0 < ↑(Nat.succ n)
⊢ ↑k ≤ Nat.succ n
[PROOFSTEP]
exact_mod_cast Fin.le_last k
[GOAL]
case succ
n : ℕ
k : Fin (Nat.succ n + 1)
h₁ : 0 < ↑(Nat.succ n)
h₂ : ↑k ≤ Nat.succ n
⊢ ↑↑k / ↑(Nat.succ n) ∈ I
[PROOFSTEP]
rw [Set.mem_Icc, le_div_iff h₁, div_le_iff h₁]
[GOAL]
case succ
n : ℕ
k : Fin (Nat.succ n + 1)
h₁ : 0 < ↑(Nat.succ n)
h₂ : ↑k ≤ Nat.succ n
⊢ 0 * ↑(Nat.succ n) ≤ ↑↑k ∧ ↑↑k ≤ 1 * ↑(Nat.succ n)
[PROOFSTEP]
norm_cast
[GOAL]
case succ
n : ℕ
k : Fin (Nat.succ n + 1)
h₁ : 0 < ↑(Nat.succ n)
h₂ : ↑k ≤ Nat.succ n
⊢ 0 * Nat.succ n ≤ ↑k ∧ ↑k ≤ 1 * Nat.succ n
[PROOFSTEP]
simp [h₂]
[GOAL]
n : ℕ
x : ↑I
⊢ ∑ k : Fin (n + 1), ↑(bernstein n ↑k) x = 1
[PROOFSTEP]
have := bernsteinPolynomial.sum ℝ n
[GOAL]
n : ℕ
x : ↑I
this : ∑ ν in Finset.range (n + 1), bernsteinPolynomial ℝ n ν = 1
⊢ ∑ k : Fin (n + 1), ↑(bernstein n ↑k) x = 1
[PROOFSTEP]
apply_fun fun p => Polynomial.aeval (x : ℝ) p at this 
[GOAL]
n : ℕ
x : ↑I
this : ↑(Polynomial.aeval ↑x) (∑ ν in Finset.range (n + 1), bernsteinPolynomial ℝ n ν) = ↑(Polynomial.aeval ↑x) 1
⊢ ∑ k : Fin (n + 1), ↑(bernstein n ↑k) x = 1
[PROOFSTEP]
simp [AlgHom.map_sum, Finset.sum_range] at this 
[GOAL]
n : ℕ
x : ↑I
this : ∑ x_1 : Fin (n + 1), Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑x_1) = 1
⊢ ∑ k : Fin (n + 1), ↑(bernstein n ↑k) x = 1
[PROOFSTEP]
exact this
[GOAL]
n : ℕ
h : 0 < ↑n
x : ↑I
⊢ ∑ k : Fin (n + 1), (↑x - ↑(k/ₙ)) ^ 2 * ↑(bernstein n ↑k) x = ↑x * (1 - ↑x) / ↑n
[PROOFSTEP]
have h' : (n : ℝ) ≠ 0 := ne_of_gt h
[GOAL]
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
⊢ ∑ k : Fin (n + 1), (↑x - ↑(k/ₙ)) ^ 2 * ↑(bernstein n ↑k) x = ↑x * (1 - ↑x) / ↑n
[PROOFSTEP]
have h'' := GroupWithZero.mul_right_injective h'
[GOAL]
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
⊢ ∑ k : Fin (n + 1), (↑x - ↑(k/ₙ)) ^ 2 * ↑(bernstein n ↑k) x = ↑x * (1 - ↑x) / ↑n
[PROOFSTEP]
apply h''
[GOAL]
case a
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
⊢ (fun y => y * ↑n) (∑ k : Fin (n + 1), (↑x - ↑(k/ₙ)) ^ 2 * ↑(bernstein n ↑k) x) =
    (fun y => y * ↑n) (↑x * (1 - ↑x) / ↑n)
[PROOFSTEP]
apply h''
[GOAL]
case a.a
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
⊢ (fun y => y * ↑n) ((fun y => y * ↑n) (∑ k : Fin (n + 1), (↑x - ↑(k/ₙ)) ^ 2 * ↑(bernstein n ↑k) x)) =
    (fun y => y * ↑n) ((fun y => y * ↑n) (↑x * (1 - ↑x) / ↑n))
[PROOFSTEP]
dsimp
[GOAL]
case a.a
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
⊢ (∑ k : Fin (n + 1), (↑x - ↑(k/ₙ)) ^ 2 * ↑(bernstein n ↑k) x) * ↑n * ↑n = ↑x * (1 - ↑x) / ↑n * ↑n * ↑n
[PROOFSTEP]
conv_lhs => simp only [Finset.sum_mul, z]
[GOAL]
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
| (∑ k : Fin (n + 1), (↑x - ↑(k/ₙ)) ^ 2 * ↑(bernstein n ↑k) x) * ↑n * ↑n
[PROOFSTEP]
simp only [Finset.sum_mul, z]
[GOAL]
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
| (∑ k : Fin (n + 1), (↑x - ↑(k/ₙ)) ^ 2 * ↑(bernstein n ↑k) x) * ↑n * ↑n
[PROOFSTEP]
simp only [Finset.sum_mul, z]
[GOAL]
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
| (∑ k : Fin (n + 1), (↑x - ↑(k/ₙ)) ^ 2 * ↑(bernstein n ↑k) x) * ↑n * ↑n
[PROOFSTEP]
simp only [Finset.sum_mul, z]
[GOAL]
case a.a
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
⊢ ∑ x_1 : Fin (n + 1), (↑x - ↑↑x_1 / ↑n) ^ 2 * ↑(bernstein n ↑x_1) x * ↑n * ↑n = ↑x * (1 - ↑x) / ↑n * ↑n * ↑n
[PROOFSTEP]
conv_rhs => rw [div_mul_cancel _ h']
[GOAL]
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
| ↑x * (1 - ↑x) / ↑n * ↑n * ↑n
[PROOFSTEP]
rw [div_mul_cancel _ h']
[GOAL]
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
| ↑x * (1 - ↑x) / ↑n * ↑n * ↑n
[PROOFSTEP]
rw [div_mul_cancel _ h']
[GOAL]
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
| ↑x * (1 - ↑x) / ↑n * ↑n * ↑n
[PROOFSTEP]
rw [div_mul_cancel _ h']
[GOAL]
case a.a
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
⊢ ∑ x_1 : Fin (n + 1), (↑x - ↑↑x_1 / ↑n) ^ 2 * ↑(bernstein n ↑x_1) x * ↑n * ↑n = ↑x * (1 - ↑x) * ↑n
[PROOFSTEP]
have := bernsteinPolynomial.variance ℝ n
[GOAL]
case a.a
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
this :
  ∑ ν in Finset.range (n + 1), (n • Polynomial.X - ↑ν) ^ 2 * bernsteinPolynomial ℝ n ν =
    n • Polynomial.X * (1 - Polynomial.X)
⊢ ∑ x_1 : Fin (n + 1), (↑x - ↑↑x_1 / ↑n) ^ 2 * ↑(bernstein n ↑x_1) x * ↑n * ↑n = ↑x * (1 - ↑x) * ↑n
[PROOFSTEP]
apply_fun fun p => Polynomial.aeval (x : ℝ) p at this 
[GOAL]
case a.a
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
this :
  ↑(Polynomial.aeval ↑x) (∑ ν in Finset.range (n + 1), (n • Polynomial.X - ↑ν) ^ 2 * bernsteinPolynomial ℝ n ν) =
    ↑(Polynomial.aeval ↑x) (n • Polynomial.X * (1 - Polynomial.X))
⊢ ∑ x_1 : Fin (n + 1), (↑x - ↑↑x_1 / ↑n) ^ 2 * ↑(bernstein n ↑x_1) x * ↑n * ↑n = ↑x * (1 - ↑x) * ↑n
[PROOFSTEP]
simp [AlgHom.map_sum, Finset.sum_range, ← Polynomial.nat_cast_mul] at this 
[GOAL]
case a.a
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
this :
  ∑ x_1 : Fin (n + 1), (↑n * ↑x - ↑↑x_1) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑x_1) = ↑n * ↑x * (1 - ↑x)
⊢ ∑ x_1 : Fin (n + 1), (↑x - ↑↑x_1 / ↑n) ^ 2 * ↑(bernstein n ↑x_1) x * ↑n * ↑n = ↑x * (1 - ↑x) * ↑n
[PROOFSTEP]
convert this using 1
[GOAL]
case h.e'_2
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
this :
  ∑ x_1 : Fin (n + 1), (↑n * ↑x - ↑↑x_1) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑x_1) = ↑n * ↑x * (1 - ↑x)
⊢ ∑ x_1 : Fin (n + 1), (↑x - ↑↑x_1 / ↑n) ^ 2 * ↑(bernstein n ↑x_1) x * ↑n * ↑n =
    ∑ x_1 : Fin (n + 1), (↑n * ↑x - ↑↑x_1) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑x_1)
[PROOFSTEP]
congr 1
[GOAL]
case h.e'_2.e_f
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
this :
  ∑ x_1 : Fin (n + 1), (↑n * ↑x - ↑↑x_1) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑x_1) = ↑n * ↑x * (1 - ↑x)
⊢ (fun x_1 => (↑x - ↑↑x_1 / ↑n) ^ 2 * ↑(bernstein n ↑x_1) x * ↑n * ↑n) = fun x_1 =>
    (↑n * ↑x - ↑↑x_1) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑x_1)
[PROOFSTEP]
funext k
[GOAL]
case h.e'_2.e_f.h
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
this :
  ∑ x_1 : Fin (n + 1), (↑n * ↑x - ↑↑x_1) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑x_1) = ↑n * ↑x * (1 - ↑x)
k : Fin (n + 1)
⊢ (↑x - ↑↑k / ↑n) ^ 2 * ↑(bernstein n ↑k) x * ↑n * ↑n =
    (↑n * ↑x - ↑↑k) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑k)
[PROOFSTEP]
rw [mul_comm _ (n : ℝ), mul_comm _ (n : ℝ), ← mul_assoc, ← mul_assoc]
[GOAL]
case h.e'_2.e_f.h
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
this :
  ∑ x_1 : Fin (n + 1), (↑n * ↑x - ↑↑x_1) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑x_1) = ↑n * ↑x * (1 - ↑x)
k : Fin (n + 1)
⊢ ↑n * ↑n * (↑x - ↑↑k / ↑n) ^ 2 * ↑(bernstein n ↑k) x =
    (↑n * ↑x - ↑↑k) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑k)
[PROOFSTEP]
congr 1
[GOAL]
case h.e'_2.e_f.h.e_a
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
this :
  ∑ x_1 : Fin (n + 1), (↑n * ↑x - ↑↑x_1) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑x_1) = ↑n * ↑x * (1 - ↑x)
k : Fin (n + 1)
⊢ ↑n * ↑n * (↑x - ↑↑k / ↑n) ^ 2 = (↑n * ↑x - ↑↑k) ^ 2
[PROOFSTEP]
field_simp [h]
[GOAL]
case h.e'_2.e_f.h.e_a
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
this :
  ∑ x_1 : Fin (n + 1), (↑n * ↑x - ↑↑x_1) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑x_1) = ↑n * ↑x * (1 - ↑x)
k : Fin (n + 1)
⊢ ↑n * ↑n * (↑x * ↑n - ↑↑k) ^ 2 = (↑n * ↑x - ↑↑k) ^ 2 * ↑n ^ 2
[PROOFSTEP]
ring
[GOAL]
case h.e'_3
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
this :
  ∑ x_1 : Fin (n + 1), (↑n * ↑x - ↑↑x_1) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑x_1) = ↑n * ↑x * (1 - ↑x)
⊢ ↑x * (1 - ↑x) * ↑n = ↑n * ↑x * (1 - ↑x)
[PROOFSTEP]
ring
[GOAL]
n : ℕ
f : C(↑I, ℝ)
x : ↑I
⊢ ↑(bernsteinApproximation n f) x = ∑ k : Fin (n + 1), ↑f k/ₙ * ↑(bernstein n ↑k) x
[PROOFSTEP]
simp [bernsteinApproximation]
[GOAL]
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
n : ℕ
x : ↑I
k : Fin (n + 1)
m : k ∈ S f ε h n x
⊢ |↑f k/ₙ - ↑f x| < ε / 2
[PROOFSTEP]
apply
  f.dist_lt_of_dist_lt_modulus (ε / 2)
    (half_pos h)
      -- Porting note: `simp` fails to apply `Set.mem_toFinset` on its own
[GOAL]
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
n : ℕ
x : ↑I
k : Fin (n + 1)
m : k ∈ S f ε h n x
⊢ dist k/ₙ x < ContinuousMap.modulus f (ε / 2) (_ : 0 < ε / 2)
[PROOFSTEP]
simpa [S, (Set.mem_toFinset)] using m
[GOAL]
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
n : ℕ
x : ↑I
k : Fin (n + 1)
m : k ∈ (S f ε h n x)ᶜ
⊢ 1 ≤ δ f ε h ^ (-2) * (↑x - ↑k/ₙ) ^ 2
[PROOFSTEP]
simp only [Finset.mem_compl, not_lt, (Set.mem_toFinset), Set.mem_setOf_eq, S] at m 
[GOAL]
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
n : ℕ
x : ↑I
k : Fin (n + 1)
m : δ f ε h ≤ dist k/ₙ x
⊢ 1 ≤ δ f ε h ^ (-2) * (↑x - ↑k/ₙ) ^ 2
[PROOFSTEP]
rw [zpow_neg, ← div_eq_inv_mul, zpow_two, ← pow_two, one_le_div (pow_pos δ_pos 2), sq_le_sq, abs_of_pos δ_pos]
[GOAL]
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
n : ℕ
x : ↑I
k : Fin (n + 1)
m : δ f ε h ≤ dist k/ₙ x
⊢ δ f ε h ≤ |↑x - ↑k/ₙ|
[PROOFSTEP]
rwa [dist_comm] at m 
[GOAL]
f : C(↑I, ℝ)
⊢ Tendsto (fun n => bernsteinApproximation n f) atTop (𝓝 f)
[PROOFSTEP]
simp only [Metric.nhds_basis_ball.tendsto_right_iff, Metric.mem_ball, dist_eq_norm]
[GOAL]
f : C(↑I, ℝ)
⊢ ∀ (i : ℝ), 0 < i → ∀ᶠ (x : ℕ) in atTop, ‖bernsteinApproximation x f - f‖ < i
[PROOFSTEP]
intro ε h
[GOAL]
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
⊢ ∀ᶠ (x : ℕ) in atTop, ‖bernsteinApproximation x f - f‖ < ε
[PROOFSTEP]
let δ := δ f ε h
[GOAL]
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
⊢ ∀ᶠ (x : ℕ) in atTop, ‖bernsteinApproximation x f - f‖ < ε
[PROOFSTEP]
have nhds_zero := tendsto_const_div_atTop_nhds_0_nat (2 * ‖f‖ * δ ^ (-2 : ℤ))
[GOAL]
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
⊢ ∀ᶠ (x : ℕ) in atTop, ‖bernsteinApproximation x f - f‖ < ε
[PROOFSTEP]
filter_upwards [nhds_zero.eventually (gt_mem_nhds (half_pos h)), eventually_gt_atTop 0] with n nh npos'
[GOAL]
case h
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
⊢ ‖bernsteinApproximation n f - f‖ < ε
[PROOFSTEP]
have npos : 0 < (n : ℝ) := by positivity
[GOAL]
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
⊢ 0 < ↑n
[PROOFSTEP]
positivity
[GOAL]
case h
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
⊢ ‖bernsteinApproximation n f - f‖ < ε
[PROOFSTEP]
have w₂ : 0 ≤ δ ^ (-2 : ℤ) :=
  zpow_neg_two_nonneg
    _
      -- TODO: need a positivity extension for `zpow`
        -- As `[0,1]` is compact, it suffices to check the inequality pointwise.
[GOAL]
case h
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
w₂ : 0 ≤ δ ^ (-2)
⊢ ‖bernsteinApproximation n f - f‖ < ε
[PROOFSTEP]
rw [ContinuousMap.norm_lt_iff _ h]
[GOAL]
case h
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
w₂ : 0 ≤ δ ^ (-2)
⊢ ∀ (x : ↑I), ‖↑(bernsteinApproximation n f - f) x‖ < ε
[PROOFSTEP]
intro x
[GOAL]
case h
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
w₂ : 0 ≤ δ ^ (-2)
x : ↑I
⊢ ‖↑(bernsteinApproximation n f - f) x‖ < ε
[PROOFSTEP]
let S := S f ε h n x
[GOAL]
case h
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
w₂ : 0 ≤ δ ^ (-2)
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
⊢ ‖↑(bernsteinApproximation n f - f) x‖ < ε
[PROOFSTEP]
calc
  |(bernsteinApproximation n f - f) x| = |bernsteinApproximation n f x - f x| := rfl
  _ = |bernsteinApproximation n f x - f x * 1| := by rw [mul_one]
  _ = |bernsteinApproximation n f x - f x * ∑ k : Fin (n + 1), bernstein n k x| := by rw [bernstein.probability]
  _ = |∑ k : Fin (n + 1), (f k/ₙ - f x) * bernstein n k x| := by simp [bernsteinApproximation, Finset.mul_sum, sub_mul]
  _ ≤ ∑ k : Fin (n + 1), |(f k/ₙ - f x) * bernstein n k x| := (Finset.abs_sum_le_sum_abs _ _)
  _ = ∑ k : Fin (n + 1), |f k/ₙ - f x| * bernstein n k x := by simp_rw [abs_mul, abs_eq_self.mpr bernstein_nonneg]
  _ = (∑ k in S, |f k/ₙ - f x| * bernstein n k x) + ∑ k in Sᶜ, |f k/ₙ - f x| * bernstein n k x :=
    (S.sum_add_sum_compl _).symm
  _ < ε / 2 + ε / 2 := (add_lt_add_of_le_of_lt ?_ ?_)
  _ = ε := add_halves ε
[GOAL]
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
w₂ : 0 ≤ δ ^ (-2)
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
⊢ |↑(bernsteinApproximation n f) x - ↑f x| = |↑(bernsteinApproximation n f) x - ↑f x * 1|
[PROOFSTEP]
rw [mul_one]
[GOAL]
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
w₂ : 0 ≤ δ ^ (-2)
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
⊢ |↑(bernsteinApproximation n f) x - ↑f x * 1| =
    |↑(bernsteinApproximation n f) x - ↑f x * ∑ k : Fin (n + 1), ↑(bernstein n ↑k) x|
[PROOFSTEP]
rw [bernstein.probability]
[GOAL]
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
w₂ : 0 ≤ δ ^ (-2)
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
⊢ |↑(bernsteinApproximation n f) x - ↑f x * ∑ k : Fin (n + 1), ↑(bernstein n ↑k) x| =
    |∑ k : Fin (n + 1), (↑f k/ₙ - ↑f x) * ↑(bernstein n ↑k) x|
[PROOFSTEP]
simp [bernsteinApproximation, Finset.mul_sum, sub_mul]
[GOAL]
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
w₂ : 0 ≤ δ ^ (-2)
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
⊢ ∑ k : Fin (n + 1), |(↑f k/ₙ - ↑f x) * ↑(bernstein n ↑k) x| = ∑ k : Fin (n + 1), |↑f k/ₙ - ↑f x| * ↑(bernstein n ↑k) x
[PROOFSTEP]
simp_rw [abs_mul, abs_eq_self.mpr bernstein_nonneg]
[GOAL]
case h.calc_1
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
w₂ : 0 ≤ δ ^ (-2)
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
⊢ ∑ k in S, |↑f k/ₙ - ↑f x| * ↑(bernstein n ↑k) x ≤ ε / 2
[PROOFSTEP]
calc
  ∑ k in S, |f k/ₙ - f x| * bernstein n k x ≤ ∑ k in S, ε / 2 * bernstein n k x :=
    by
    gcongr with _ m
    exact le_of_lt (lt_of_mem_S m)
  _ = ε / 2 * ∑ k in S, bernstein n k x := by
    rw [Finset.mul_sum]
      -- 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`.
  _ ≤ ε / 2 * ∑ k : Fin (n + 1), bernstein n k x := by
    gcongr
    exact Finset.sum_le_univ_sum_of_nonneg fun k => bernstein_nonneg
  _ = ε / 2 := by rw [bernstein.probability, mul_one]
[GOAL]
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
w₂ : 0 ≤ δ ^ (-2)
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
⊢ ∑ k in S, |↑f k/ₙ - ↑f x| * ↑(bernstein n ↑k) x ≤ ∑ k in S, ε / 2 * ↑(bernstein n ↑k) x
[PROOFSTEP]
gcongr with _ m
[GOAL]
case h.h
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
w₂ : 0 ≤ δ ^ (-2)
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
i✝ : Fin (n + 1)
m : i✝ ∈ S
⊢ |↑f i✝/ₙ - ↑f x| ≤ ε / 2
[PROOFSTEP]
exact le_of_lt (lt_of_mem_S m)
[GOAL]
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
w₂ : 0 ≤ δ ^ (-2)
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
⊢ ∑ k in S, ε / 2 * ↑(bernstein n ↑k) x = ε / 2 * ∑ k in S, ↑(bernstein n ↑k) x
[PROOFSTEP]
rw [Finset.mul_sum]
  -- 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`.
[GOAL]
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
w₂ : 0 ≤ δ ^ (-2)
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
⊢ ε / 2 * ∑ k in S, ↑(bernstein n ↑k) x ≤ ε / 2 * ∑ k : Fin (n + 1), ↑(bernstein n ↑k) x
[PROOFSTEP]
gcongr
[GOAL]
case h
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
w₂ : 0 ≤ δ ^ (-2)
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
⊢ ∑ k in S, ↑(bernstein n ↑k) x ≤ ∑ k : Fin (n + 1), ↑(bernstein n ↑k) x
[PROOFSTEP]
exact Finset.sum_le_univ_sum_of_nonneg fun k => bernstein_nonneg
[GOAL]
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
w₂ : 0 ≤ δ ^ (-2)
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
⊢ ε / 2 * ∑ k : Fin (n + 1), ↑(bernstein n ↑k) x = ε / 2
[PROOFSTEP]
rw [bernstein.probability, mul_one]
[GOAL]
case h.calc_2
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
w₂ : 0 ≤ δ ^ (-2)
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
⊢ ∑ k in Sᶜ, |↑f k/ₙ - ↑f x| * ↑(bernstein n ↑k) x < ε / 2
[PROOFSTEP]
calc
  ∑ k in Sᶜ, |f k/ₙ - f x| * bernstein n k x ≤ ∑ k in Sᶜ, 2 * ‖f‖ * bernstein n k x :=
    by
    gcongr
    apply f.dist_le_two_norm
  _ = 2 * ‖f‖ * ∑ k in Sᶜ, bernstein n k x := by rw [Finset.mul_sum]
  _ ≤ 2 * ‖f‖ * ∑ k in Sᶜ, δ ^ (-2 : ℤ) * ((x : ℝ) - k/ₙ) ^ 2 * bernstein n k x :=
    by
    gcongr with _ m
    conv_lhs => rw [← one_mul (bernstein _ _ _)]
    gcongr
    exact le_of_mem_S_compl m
  _ ≤ 2 * ‖f‖ * ∑ k : Fin (n + 1), δ ^ (-2 : ℤ) * ((x : ℝ) - k/ₙ) ^ 2 * bernstein n k x :=
    by
    gcongr
    refine Finset.sum_le_univ_sum_of_nonneg <| fun k => ?_
    positivity
  _ = 2 * ‖f‖ * δ ^ (-2 : ℤ) * ∑ k : Fin (n + 1), ((x : ℝ) - k/ₙ) ^ 2 * bernstein n k x := by
    conv_rhs =>
      rw [mul_assoc, Finset.mul_sum]
      simp only [← mul_assoc]
        -- `bernstein.variance` and `x ∈ [0,1]` gives the uniform bound
  _ = 2 * ‖f‖ * δ ^ (-2 : ℤ) * x * (1 - x) / n := by rw [variance npos]; ring
  _ ≤ 2 * ‖f‖ * δ ^ (-2 : ℤ) * 1 * 1 / n := by gcongr <;> unit_interval
  _ < ε / 2 := by simp only [mul_one]; exact nh
[GOAL]
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
w₂ : 0 ≤ δ ^ (-2)
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
⊢ ∑ k in Sᶜ, |↑f k/ₙ - ↑f x| * ↑(bernstein n ↑k) x ≤ ∑ k in Sᶜ, 2 * ‖f‖ * ↑(bernstein n ↑k) x
[PROOFSTEP]
gcongr
[GOAL]
case h.h
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
w₂ : 0 ≤ δ ^ (-2)
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
i✝ : Fin (n + 1)
a✝ : i✝ ∈ Sᶜ
⊢ |↑f i✝/ₙ - ↑f x| ≤ 2 * ‖f‖
[PROOFSTEP]
apply f.dist_le_two_norm
[GOAL]
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
w₂ : 0 ≤ δ ^ (-2)
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
⊢ ∑ k in Sᶜ, 2 * ‖f‖ * ↑(bernstein n ↑k) x = 2 * ‖f‖ * ∑ k in Sᶜ, ↑(bernstein n ↑k) x
[PROOFSTEP]
rw [Finset.mul_sum]
[GOAL]
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
w₂ : 0 ≤ δ ^ (-2)
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
⊢ 2 * ‖f‖ * ∑ k in Sᶜ, ↑(bernstein n ↑k) x ≤ 2 * ‖f‖ * ∑ k in Sᶜ, δ ^ (-2) * (↑x - ↑k/ₙ) ^ 2 * ↑(bernstein n ↑k) x
[PROOFSTEP]
gcongr with _ m
[GOAL]
case h.h
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
w₂ : 0 ≤ δ ^ (-2)
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
i✝ : Fin (n + 1)
m : i✝ ∈ Sᶜ
⊢ ↑(bernstein n ↑i✝) x ≤ δ ^ (-2) * (↑x - ↑i✝/ₙ) ^ 2 * ↑(bernstein n ↑i✝) x
[PROOFSTEP]
conv_lhs => rw [← one_mul (bernstein _ _ _)]
[GOAL]
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
w₂ : 0 ≤ δ ^ (-2)
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
i✝ : Fin (n + 1)
m : i✝ ∈ Sᶜ
| ↑(bernstein n ↑i✝) x
[PROOFSTEP]
rw [← one_mul (bernstein _ _ _)]
[GOAL]
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
w₂ : 0 ≤ δ ^ (-2)
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
i✝ : Fin (n + 1)
m : i✝ ∈ Sᶜ
| ↑(bernstein n ↑i✝) x
[PROOFSTEP]
rw [← one_mul (bernstein _ _ _)]
[GOAL]
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
w₂ : 0 ≤ δ ^ (-2)
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
i✝ : Fin (n + 1)
m : i✝ ∈ Sᶜ
| ↑(bernstein n ↑i✝) x
[PROOFSTEP]
rw [← one_mul (bernstein _ _ _)]
[GOAL]
case h.h
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
w₂ : 0 ≤ δ ^ (-2)
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
i✝ : Fin (n + 1)
m : i✝ ∈ Sᶜ
⊢ 1 * ↑(bernstein n ↑i✝) x ≤ δ ^ (-2) * (↑x - ↑i✝/ₙ) ^ 2 * ↑(bernstein n ↑i✝) x
[PROOFSTEP]
gcongr
[GOAL]
case h.h.h
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
w₂ : 0 ≤ δ ^ (-2)
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
i✝ : Fin (n + 1)
m : i✝ ∈ Sᶜ
⊢ 1 ≤ δ ^ (-2) * (↑x - ↑i✝/ₙ) ^ 2
[PROOFSTEP]
exact le_of_mem_S_compl m
[GOAL]
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
w₂ : 0 ≤ δ ^ (-2)
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
⊢ 2 * ‖f‖ * ∑ k in Sᶜ, δ ^ (-2) * (↑x - ↑k/ₙ) ^ 2 * ↑(bernstein n ↑k) x ≤
    2 * ‖f‖ * ∑ k : Fin (n + 1), δ ^ (-2) * (↑x - ↑k/ₙ) ^ 2 * ↑(bernstein n ↑k) x
[PROOFSTEP]
gcongr
[GOAL]
case h
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
w₂ : 0 ≤ δ ^ (-2)
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
⊢ ∑ k in Sᶜ, δ ^ (-2) * (↑x - ↑k/ₙ) ^ 2 * ↑(bernstein n ↑k) x ≤
    ∑ k : Fin (n + 1), δ ^ (-2) * (↑x - ↑k/ₙ) ^ 2 * ↑(bernstein n ↑k) x
[PROOFSTEP]
refine Finset.sum_le_univ_sum_of_nonneg <| fun k => ?_
[GOAL]
case h
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
w₂ : 0 ≤ δ ^ (-2)
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
k : Fin (n + 1)
⊢ 0 ≤ δ ^ (-2) * (↑x - ↑k/ₙ) ^ 2 * ↑(bernstein n ↑k) x
[PROOFSTEP]
positivity
[GOAL]
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
w₂ : 0 ≤ δ ^ (-2)
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
⊢ 2 * ‖f‖ * ∑ k : Fin (n + 1), δ ^ (-2) * (↑x - ↑k/ₙ) ^ 2 * ↑(bernstein n ↑k) x =
    2 * ‖f‖ * δ ^ (-2) * ∑ k : Fin (n + 1), (↑x - ↑k/ₙ) ^ 2 * ↑(bernstein n ↑k) x
[PROOFSTEP]
conv_rhs =>
  rw [mul_assoc, Finset.mul_sum]
  simp only [← mul_assoc]
    -- `bernstein.variance` and `x ∈ [0,1]` gives the uniform bound
[GOAL]
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
w₂ : 0 ≤ δ ^ (-2)
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
| 2 * ‖f‖ * δ ^ (-2) * ∑ k : Fin (n + 1), (↑x - ↑k/ₙ) ^ 2 * ↑(bernstein n ↑k) x
[PROOFSTEP]
  rw [mul_assoc, Finset.mul_sum]
  simp only [← mul_assoc]
    -- `bernstein.variance` and `x ∈ [0,1]` gives the uniform bound
[GOAL]
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
w₂ : 0 ≤ δ ^ (-2)
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
| 2 * ‖f‖ * δ ^ (-2) * ∑ k : Fin (n + 1), (↑x - ↑k/ₙ) ^ 2 * ↑(bernstein n ↑k) x
[PROOFSTEP]
  rw [mul_assoc, Finset.mul_sum]
  simp only [← mul_assoc]
    -- `bernstein.variance` and `x ∈ [0,1]` gives the uniform bound
[GOAL]
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
w₂ : 0 ≤ δ ^ (-2)
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
| 2 * ‖f‖ * δ ^ (-2) * ∑ k : Fin (n + 1), (↑x - ↑k/ₙ) ^ 2 * ↑(bernstein n ↑k) x
[PROOFSTEP]
rw [mul_assoc, Finset.mul_sum]
[GOAL]
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
w₂ : 0 ≤ δ ^ (-2)
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
| 2 * ‖f‖ * ∑ x_1 : Fin (n + 1), δ ^ (-2) * ((↑x - ↑x_1/ₙ) ^ 2 * ↑(bernstein n ↑x_1) x)
[PROOFSTEP]
simp only [← mul_assoc]
  -- `bernstein.variance` and `x ∈ [0,1]` gives the uniform bound
[GOAL]
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
w₂ : 0 ≤ δ ^ (-2)
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
⊢ 2 * ‖f‖ * δ ^ (-2) * ∑ k : Fin (n + 1), (↑x - ↑k/ₙ) ^ 2 * ↑(bernstein n ↑k) x =
    2 * ‖f‖ * δ ^ (-2) * ↑x * (1 - ↑x) / ↑n
[PROOFSTEP]
rw [variance npos]
[GOAL]
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
w₂ : 0 ≤ δ ^ (-2)
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
⊢ 2 * ‖f‖ * δ ^ (-2) * (↑x * (1 - ↑x) / ↑n) = 2 * ‖f‖ * δ ^ (-2) * ↑x * (1 - ↑x) / ↑n
[PROOFSTEP]
ring
[GOAL]
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
w₂ : 0 ≤ δ ^ (-2)
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
⊢ 2 * ‖f‖ * δ ^ (-2) * ↑x * (1 - ↑x) / ↑n ≤ 2 * ‖f‖ * δ ^ (-2) * 1 * 1 / ↑n
[PROOFSTEP]
gcongr
[GOAL]
case h.c0
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
w₂ : 0 ≤ δ ^ (-2)
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
⊢ 0 ≤ 1 - ↑x
[PROOFSTEP]
unit_interval
[GOAL]
case h.h₁.h
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
w₂ : 0 ≤ δ ^ (-2)
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
⊢ ↑x ≤ 1
[PROOFSTEP]
unit_interval
[GOAL]
case h.h₂
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
w₂ : 0 ≤ δ ^ (-2)
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
⊢ 1 - ↑x ≤ 1
[PROOFSTEP]
unit_interval
[GOAL]
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
w₂ : 0 ≤ δ ^ (-2)
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
⊢ 2 * ‖f‖ * δ ^ (-2) * 1 * 1 / ↑n < ε / 2
[PROOFSTEP]
simp only [mul_one]
[GOAL]
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
w₂ : 0 ≤ δ ^ (-2)
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
⊢ 2 * ‖f‖ * bernsteinApproximation.δ f ε h ^ (-2) / ↑n < ε / 2
[PROOFSTEP]
exact nh
