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

Proof state:
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‖ * δ ^ (-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 < ε / 2

Tactic:
calc
  ∑ k ∈ Sᶜ, |f k/ₙ - f x| * bernstein n k x ≤ ∑ k ∈ Sᶜ, 2 * ‖f‖ * bernstein n k x := by
    gcongr
    apply f.dist_le_two_norm
  _ = 2 * ‖f‖ * ∑ k ∈ Sᶜ, bernstein n k x := by rw [Finset.mul_sum]
  _ ≤ 2 * ‖f‖ * ∑ k ∈ 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; exact Sᶜ.subset_univ
  _ = 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]
  _ = 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

Result:
no goals

Proof state:
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‖ < ε

Tactic:
filter_upwards [nhds_zero.eventually (gt_mem_nhds (half_pos h)), eventually_gt_atTop 0] with n nh
  npos'

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
⊢ ‖bernsteinApproximation n f - f‖ < ε

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)
a✝ : i✝ ∈ Sᶜ
⊢ |f i✝/ₙ - f x| ≤ 2 * ‖f‖

Tactic:
apply f.dist_le_two_norm

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) * 1 * 1 / ↑n < ε / 2

Tactic:
simp only [mul_one]

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) / ↑n < ε / 2

Proof state:
f : C(↑I, ℝ)
⊢ ∀ (i : ℝ), 0 < i → ∀ᶠ (x : ℕ) in atTop, ‖bernsteinApproximation x f - f‖ < i

Tactic:
intro ε h

Result:
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
⊢ ∀ᶠ (x : ℕ) in atTop, ‖bernsteinApproximation x f - f‖ < ε

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ᶜ
⊢ 1 * (bernstein n ↑i✝) x ≤ δ ^ (-2) * (↑x - ↑i✝/ₙ) ^ 2 * (bernstein n ↑i✝) x

Tactic:
gcongr

Result:
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‖ * δ ^ (-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 ≤ δ ^ (-2) * (↑x - ↑i✝/ₙ) ^ 2

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ᶜ, δ ^ (-2) * (↑x - ↑k/ₙ) ^ 2 * (bernstein n ↑k) x ≤
    2 * ‖f‖ * ∑ k : Fin (n + 1), δ ^ (-2) * (↑x - ↑k/ₙ) ^ 2 * (bernstein n ↑k) x

Tactic:
gcongr

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
⊢ Sᶜ ⊆ Finset.univ

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) * ↑x * (1 - ↑x) / ↑n

Tactic:
ring

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) / ↑n < ε / 2

Tactic:
exact nh

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
⊢ ‖bernsteinApproximation n f - f‖ < ε

Tactic:
rw [ContinuousMap.norm_lt_iff _ h]

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), ‖(bernsteinApproximation n f - f) x‖ < ε

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
⊢ ‖bernsteinApproximation n f - f‖ < ε

Tactic:
have npos : 0 < (n : ℝ) := by positivity

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
⊢ ‖bernsteinApproximation n f - f‖ < ε

Proof state:
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‖ * δ ^ (-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 ≤ δ ^ (-2) * (↑x - ↑i✝/ₙ) ^ 2

Tactic:
exact le_of_mem_S_compl m

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