f : C(↑I, ℝ)
⊢ ∀ (i : ℝ), 0 < i → ∀ᶠ (x : ℕ) in atTop, ‖bernsteinApproximation x f - f‖ < i
f : C(↑I, ℝ)
⊢ Tendsto (fun n => bernsteinApproximation n f) atTop (𝓝 f)
simp only [Metric.nhds_basis_ball.tendsto_right_iff, Metric.mem_ball, dist_eq_norm]
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
⊢ ∀ᶠ (x : ℕ) in atTop, ‖bernsteinApproximation x f - f‖ < ε
f : C(↑I, ℝ)
⊢ ∀ (i : ℝ), 0 < i → ∀ᶠ (x : ℕ) in atTop, ‖bernsteinApproximation x f - f‖ < i
intro ε h
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
⊢ ∀ᶠ (x : ℕ) in atTop, ‖bernsteinApproximation x f - f‖ < ε
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
⊢ ∀ᶠ (x : ℕ) in atTop, ‖bernsteinApproximation x f - f‖ < ε
let δ := δ f ε h
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‖ < ε
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
δ : ℝ := bernsteinApproximation.δ f ε h
⊢ ∀ᶠ (x : ℕ) in atTop, ‖bernsteinApproximation x f - f‖ < ε
have nhds_zero := tendsto_const_div_atTop_nhds_0_nat (2 * ‖f‖ * δ ^ (-2 : ℤ))
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‖ < ε
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‖ < ε
filter_upwards [nhds_zero.eventually (gt_mem_nhds (half_pos h)), eventually_gt_atTop 0] with n nh
  npos'
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‖ < ε
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‖ < ε
have npos : 0 < (n : ℝ) := by positivity
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‖ < ε
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‖ < ε
have w₂ : 0 ≤ δ ^ (-2:ℤ) := zpow_neg_two_nonneg _
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‖ < ε
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‖ < ε
rw [ContinuousMap.norm_lt_iff _ h]
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‖ < ε
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‖ < ε
intro x
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‖ < ε
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‖ < ε
let S := S f ε h n x
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, abs (↑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‖ * 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ᶜ, abs (↑f k/ₙ - ↑f x) * ↑(bernstein n ↑k) x < ε / 2
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‖ < ε
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 ε
no goals
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
positivity
no goals
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
⊢ abs (↑(bernsteinApproximation n f) x - ↑f x) = abs (↑(bernsteinApproximation n f) x - ↑f x * 1)
rw [mul_one]
no goals
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
⊢ abs (↑(bernsteinApproximation n f) x - ↑f x * 1) =
    abs (↑(bernsteinApproximation n f) x - ↑f x * ∑ k : Fin (n + 1), ↑(bernstein n ↑k) x)
rw [bernstein.probability]
no goals
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
⊢ abs (↑(bernsteinApproximation n f) x - ↑f x * ∑ k : Fin (n + 1), ↑(bernstein n ↑k) x) =
    abs (∑ k : Fin (n + 1), (↑f k/ₙ - ↑f x) * ↑(bernstein n ↑k) x)
simp [bernsteinApproximation, Finset.mul_sum, sub_mul]
no goals
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), abs ((↑f k/ₙ - ↑f x) * ↑(bernstein n ↑k) x) =
    ∑ k : Fin (n + 1), abs (↑f k/ₙ - ↑f x) * ↑(bernstein n ↑k) x
simp_rw [abs_mul, abs_eq_self.mpr bernstein_nonneg]
no goals
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, abs (↑f k/ₙ - ↑f x) * ↑(bernstein n ↑k) x ≤ ε / 2
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]
  _ ≤ ε / 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]
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
⊢ abs (↑f i✝/ₙ - ↑f x) ≤ ε / 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, abs (↑f k/ₙ - ↑f x) * ↑(bernstein n ↑k) x ≤ ∑ k in S, ε / 2 * ↑(bernstein n ↑k) x
gcongr with _ m
no goals
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
⊢ abs (↑f i✝/ₙ - ↑f x) ≤ ε / 2
exact le_of_lt (lt_of_mem_S m)
no goals
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
rw [Finset.mul_sum]
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
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
gcongr
no goals
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
exact Finset.sum_le_univ_sum_of_nonneg fun k => bernstein_nonneg
no goals
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
rw [bernstein.probability, mul_one]
no goals
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ᶜ, abs (↑f k/ₙ - ↑f x) * ↑(bernstein n ↑k) x < ε / 2
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]
  _ = 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
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ᶜ
⊢ abs (↑f i✝/ₙ - ↑f x) ≤ 2 * ‖f‖
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ᶜ, abs (↑f k/ₙ - ↑f x) * ↑(bernstein n ↑k) x ≤ ∑ k in Sᶜ, 2 * ‖f‖ * ↑(bernstein n ↑k) x
gcongr
no goals
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ᶜ
⊢ abs (↑f i✝/ₙ - ↑f x) ≤ 2 * ‖f‖
apply f.dist_le_two_norm
no goals
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
rw [Finset.mul_sum]
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
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
gcongr with _ m
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
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
conv_lhs => rw [← one_mul (bernstein _ _ _)]
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
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
gcongr
no goals
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
exact le_of_mem_S_compl m
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
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
gcongr
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
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
refine Finset.sum_le_univ_sum_of_nonneg <| fun k => ?_
no goals
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
positivity
no goals
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
conv_rhs =>
  rw [mul_assoc, Finset.mul_sum]
  simp only [← mul_assoc]
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
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
rw [variance npos]
no goals
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
ring
no goals
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
gcongr <;> unit_interval
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
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
simp only [mul_one]
no goals
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
exact nh