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

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
S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x
⊢ ‖(bernsteinApproximation n f - f) x‖ < ε

Tactic:
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 ∈ S, |f k/ₙ - f x| * bernstein n k x) + ∑ k ∈ 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 ε

Result:
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‖ * δ ^ (-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

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

Proof state:
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
⊢ ∀ᶠ (x : ℕ) in atTop, ‖bernsteinApproximation x f - f‖ < ε

Tactic:
have nhds_zero := tendsto_const_div_atTop_nhds_zero_nat (2 * ‖f‖ * δ ^ (-2 : ℤ))

Result:
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‖ < ε

Proof state:
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‖ * δ ^ (-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 * bernstein n k x := by
    gcongr with _ m
    exact le_of_lt (lt_of_mem_S m)
  _ = ε / 2 * ∑ k ∈ S, bernstein n k x := by rw [Finset.mul_sum]
  _ ≤ ε / 2 * ∑ k : Fin (n + 1), bernstein n k x := by gcongr; exact S.subset_univ
  _ = ε / 2 := by rw [bernstein.probability, mul_one]

Result:
no goals

Proof state:
f : C(↑I, ℝ)
⊢ Tendsto (fun n => bernsteinApproximation n f) atTop (𝓝 f)

Tactic:
simp only [Metric.nhds_basis_ball.tendsto_right_iff, Metric.mem_ball, dist_eq_norm]

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

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 * ∑ k : Fin (n + 1), (bernstein n ↑k) x| =
    |∑ k : Fin (n + 1), (f k/ₙ - f x) * (bernstein n ↑k) x|

Tactic:
simp [bernsteinApproximation, Finset.mul_sum, sub_mul]

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
⊢ 0 < ↑n

Tactic:
positivity

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 ∈ S, (bernstein n ↑k) x ≤ ε / 2 * ∑ k : Fin (n + 1), (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‖ * ∑ 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

Tactic:
conv_rhs =>
  rw [mul_assoc, Finset.mul_sum]
  simp only [← mul_assoc]

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:
intro 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
⊢ ‖(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
⊢ ∑ k ∈ Sᶜ, |f k/ₙ - f x| * (bernstein n ↑k) x ≤ ∑ k ∈ Sᶜ, 2 * ‖f‖ * (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
i✝ : Fin (n + 1)
a✝ : i✝ ∈ Sᶜ
⊢ |f i✝/ₙ - f x| ≤ 2 * ‖f‖

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

Tactic:
let δ := δ f ε h

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