a b : ℝ
f : ℝ → ℝ
c : ContinuousOn f (Set.Icc a b)
ε : ℝ
pos : 0 < ε
f' : C(↑(Set.Icc a b), ℝ) := ContinuousMap.mk fun x => f ↑x
⊢ ∃ p, ∀ (x : ℝ), x ∈ Set.Icc a b → Abs.abs (Polynomial.eval x p - f x) < ε
a b : ℝ
f : ℝ → ℝ
c : ContinuousOn f (Set.Icc a b)
ε : ℝ
pos : 0 < ε
⊢ ∃ p, ∀ (x : ℝ), x ∈ Set.Icc a b → Abs.abs (Polynomial.eval x p - f x) < ε
let f' : C(Set.Icc a b, ℝ) := ⟨fun x => f x, continuousOn_iff_continuous_restrict.mp c⟩
case intro
a b✝ : ℝ
f : ℝ → ℝ
c : ContinuousOn f (Set.Icc a b✝)
ε : ℝ
pos : 0 < ε
f' : C(↑(Set.Icc a b✝), ℝ) := ContinuousMap.mk fun x => f ↑x
p : ℝ[X]
b : ‖Polynomial.toContinuousMapOn p (Set.Icc a b✝) - f'‖ < ε
⊢ ∃ p, ∀ (x : ℝ), x ∈ Set.Icc a b✝ → Abs.abs (Polynomial.eval x p - f x) < ε
a b : ℝ
f : ℝ → ℝ
c : ContinuousOn f (Set.Icc a b)
ε : ℝ
pos : 0 < ε
f' : C(↑(Set.Icc a b), ℝ) := ContinuousMap.mk fun x => f ↑x
⊢ ∃ p, ∀ (x : ℝ), x ∈ Set.Icc a b → Abs.abs (Polynomial.eval x p - f x) < ε
obtain ⟨p, b⟩ := exists_polynomial_near_continuousMap a b f' ε pos
case intro
a b✝ : ℝ
f : ℝ → ℝ
c : ContinuousOn f (Set.Icc a b✝)
ε : ℝ
pos : 0 < ε
f' : C(↑(Set.Icc a b✝), ℝ) := ContinuousMap.mk fun x => f ↑x
p : ℝ[X]
b : ‖Polynomial.toContinuousMapOn p (Set.Icc a b✝) - f'‖ < ε
⊢ ∀ (x : ℝ), x ∈ Set.Icc a b✝ → Abs.abs (Polynomial.eval x p - f x) < ε
case intro
a b✝ : ℝ
f : ℝ → ℝ
c : ContinuousOn f (Set.Icc a b✝)
ε : ℝ
pos : 0 < ε
f' : C(↑(Set.Icc a b✝), ℝ) := ContinuousMap.mk fun x => f ↑x
p : ℝ[X]
b : ‖Polynomial.toContinuousMapOn p (Set.Icc a b✝) - f'‖ < ε
⊢ ∃ p, ∀ (x : ℝ), x ∈ Set.Icc a b✝ → Abs.abs (Polynomial.eval x p - f x) < ε
use p
case intro
a b✝ : ℝ
f : ℝ → ℝ
c : ContinuousOn f (Set.Icc a b✝)
ε : ℝ
pos : 0 < ε
f' : C(↑(Set.Icc a b✝), ℝ) := ContinuousMap.mk fun x => f ↑x
p : ℝ[X]
b : ∀ (x : ↑(Set.Icc a b✝)), ‖↑(Polynomial.toContinuousMapOn p (Set.Icc a b✝) - f') x‖ < ε
⊢ ∀ (x : ℝ), x ∈ Set.Icc a b✝ → Abs.abs (Polynomial.eval x p - f x) < ε
case intro
a b✝ : ℝ
f : ℝ → ℝ
c : ContinuousOn f (Set.Icc a b✝)
ε : ℝ
pos : 0 < ε
f' : C(↑(Set.Icc a b✝), ℝ) := ContinuousMap.mk fun x => f ↑x
p : ℝ[X]
b : ‖Polynomial.toContinuousMapOn p (Set.Icc a b✝) - f'‖ < ε
⊢ ∀ (x : ℝ), x ∈ Set.Icc a b✝ → Abs.abs (Polynomial.eval x p - f x) < ε
rw [norm_lt_iff _ pos] at b
case intro
a b✝ : ℝ
f : ℝ → ℝ
c : ContinuousOn f (Set.Icc a b✝)
ε : ℝ
pos : 0 < ε
f' : C(↑(Set.Icc a b✝), ℝ) := ContinuousMap.mk fun x => f ↑x
p : ℝ[X]
b : ∀ (x : ↑(Set.Icc a b✝)), ‖↑(Polynomial.toContinuousMapOn p (Set.Icc a b✝) - f') x‖ < ε
x : ℝ
m : x ∈ Set.Icc a b✝
⊢ Abs.abs (Polynomial.eval x p - f x) < ε
case intro
a b✝ : ℝ
f : ℝ → ℝ
c : ContinuousOn f (Set.Icc a b✝)
ε : ℝ
pos : 0 < ε
f' : C(↑(Set.Icc a b✝), ℝ) := ContinuousMap.mk fun x => f ↑x
p : ℝ[X]
b : ∀ (x : ↑(Set.Icc a b✝)), ‖↑(Polynomial.toContinuousMapOn p (Set.Icc a b✝) - f') x‖ < ε
⊢ ∀ (x : ℝ), x ∈ Set.Icc a b✝ → Abs.abs (Polynomial.eval x p - f x) < ε
intro x m
no goals
case intro
a b✝ : ℝ
f : ℝ → ℝ
c : ContinuousOn f (Set.Icc a b✝)
ε : ℝ
pos : 0 < ε
f' : C(↑(Set.Icc a b✝), ℝ) := ContinuousMap.mk fun x => f ↑x
p : ℝ[X]
b : ∀ (x : ↑(Set.Icc a b✝)), ‖↑(Polynomial.toContinuousMapOn p (Set.Icc a b✝) - f') x‖ < ε
x : ℝ
m : x ∈ Set.Icc a b✝
⊢ Abs.abs (Polynomial.eval x p - f x) < ε
exact b ⟨x, m⟩