-- Mathlib/Analysis/SpecialFunctions/Bernstein.lean
theorem bernsteinApproximation_uniform (f : C(I, ℝ)) :
    Tendsto (fun n : ℕ => bernsteinApproximation n f) atTop (𝓝 f)

Proof state:
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * δ ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
⊢ ∑ k ∈ S, ε / 2 * (bernstein n ↑k) x = ε / 2 * ∑ k ∈ S, (bernstein n ↑k) x

Tactic:
rw [Finset.mul_sum]

Result:
no goals

Proof state:
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‖ * δ ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
x : ↑I
⊢ ‖(bernsteinApproximation n f - f) x‖ < ε

Tactic:
let S := S f ε h n x

Result:
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‖ * δ ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
⊢ ‖(bernsteinApproximation n f - f) x‖ < ε

Proof state:
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * δ ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
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|

Tactic:
rw [bernstein.probability]

Result:
no goals

Proof state:
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * δ ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
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

Tactic:
rw [variance npos]

Result:
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * δ ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
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

Proof state:
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * δ ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
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|

Tactic:
rw [mul_one]

Result:
no goals

Proof state:
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * δ ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
⊢ ε / 2 * ∑ k : Fin (n + 1), (bernstein n ↑k) x = ε / 2

Tactic:
rw [bernstein.probability, mul_one]

Result:
no goals

Proof state:
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * δ ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
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

Tactic:
gcongr <;> unit_interval

Result:
no goals

Proof state:
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * δ ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
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

Tactic:
simp_rw [abs_mul, abs_eq_self.mpr bernstein_nonneg]

Result:
no goals

Proof state:
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‖ * δ ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
⊢ S ⊆ Finset.univ

Tactic:
exact S.subset_univ

Result:
no goals

Proof state:
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * δ ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
⊢ ∑ k ∈ Sᶜ, 2 * ‖f‖ * (bernstein n ↑k) x = 2 * ‖f‖ * ∑ k ∈ Sᶜ, (bernstein n ↑k) x

Tactic:
rw [Finset.mul_sum]

Result:
no goals

Proof state:
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * δ ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
⊢ 2 * ‖f‖ * ∑ k ∈ Sᶜ, (bernstein n ↑k) x ≤ 2 * ‖f‖ * ∑ k ∈ Sᶜ, δ ^ (-2) * (↑x - ↑k/ₙ) ^ 2 * (bernstein n ↑k) x

Tactic:
gcongr with _ m

Result:
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‖ * δ ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
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

Proof state:
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‖ * δ ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
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

Tactic:
conv_lhs => rw [← one_mul (bernstein _ _ _)]

Result:
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‖ * δ ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
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

Proof state:
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)
n : ℕ
nh : 2 * ‖f‖ * δ ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
x : ↑I
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
⊢ ∑ k ∈ S, |f k/ₙ - f x| * (bernstein n ↑k) x ≤ ∑ k ∈ S, ε / 2 * (bernstein n ↑k) x

Tactic:
gcongr with _ m

Result:
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‖ * δ ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
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

Proof state:
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‖ * δ ^ (-2) / ↑n < ε / 2
npos' : 0 < n
npos : 0 < ↑n
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

Tactic:
exact le_of_lt (lt_of_mem_S m)

Result:
no goals