[GOAL]
⊢ Subalgebra.topologicalClosure (polynomialFunctions I) = ⊤
[PROOFSTEP]
apply eq_top_iff.mpr
[GOAL]
⊢ ⊤ ≤ Subalgebra.topologicalClosure (polynomialFunctions I)
[PROOFSTEP]
rintro f -
[GOAL]
f : C(↑I, ℝ)
⊢ f ∈ Subalgebra.topologicalClosure (polynomialFunctions I)
[PROOFSTEP]
refine' Filter.Frequently.mem_closure _
[GOAL]
f : C(↑I, ℝ)
⊢ ∃ᶠ (x : C(↑I, ℝ)) in nhds f, x ∈ ↑(polynomialFunctions I)
[PROOFSTEP]
refine' Filter.Tendsto.frequently (bernsteinApproximation_uniform f) _
[GOAL]
f : C(↑I, ℝ)
⊢ ∃ᶠ (x : ℕ) in atTop, bernsteinApproximation x f ∈ ↑(polynomialFunctions I)
[PROOFSTEP]
apply frequently_of_forall
[GOAL]
case h
f : C(↑I, ℝ)
⊢ ∀ (x : ℕ), bernsteinApproximation x f ∈ ↑(polynomialFunctions I)
[PROOFSTEP]
intro n
[GOAL]
case h
f : C(↑I, ℝ)
n : ℕ
⊢ bernsteinApproximation n f ∈ ↑(polynomialFunctions I)
[PROOFSTEP]
simp only [SetLike.mem_coe]
[GOAL]
case h
f : C(↑I, ℝ)
n : ℕ
⊢ bernsteinApproximation n f ∈ polynomialFunctions I
[PROOFSTEP]
apply Subalgebra.sum_mem
[GOAL]
case h.h
f : C(↑I, ℝ)
n : ℕ
⊢ ∀ (x : Fin (n + 1)), x ∈ Finset.univ → ↑f (bernstein.z x) • bernstein n ↑x ∈ polynomialFunctions I
[PROOFSTEP]
rintro n -
[GOAL]
case h.h
f : C(↑I, ℝ)
n✝ : ℕ
n : Fin (n✝ + 1)
⊢ ↑f (bernstein.z n) • bernstein n✝ ↑n ∈ polynomialFunctions I
[PROOFSTEP]
apply Subalgebra.smul_mem
[GOAL]
case h.h.hx
f : C(↑I, ℝ)
n✝ : ℕ
n : Fin (n✝ + 1)
⊢ bernstein n✝ ↑n ∈ polynomialFunctions I
[PROOFSTEP]
dsimp [bernstein, polynomialFunctions]
[GOAL]
case h.h.hx
f : C(↑I, ℝ)
n✝ : ℕ
n : Fin (n✝ + 1)
⊢ Polynomial.toContinuousMapOn (bernsteinPolynomial ℝ n✝ ↑n) I ∈ Subalgebra.map (Polynomial.toContinuousMapOnAlgHom I) ⊤
[PROOFSTEP]
simp
[GOAL]
a b : ℝ
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
[PROOFSTEP]
cases' lt_or_le a b with h h
[GOAL]
case inl
a b : ℝ
h : a < b
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
[PROOFSTEP]
let W : C(Set.Icc a b, ℝ) →ₐ[ℝ] C(I, ℝ) := compRightAlgHom ℝ ℝ (iccHomeoI a b h).symm.toContinuousMap
[GOAL]
case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) :=
  compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
[PROOFSTEP]
let W' : C(Set.Icc a b, ℝ) ≃ₜ C(I, ℝ) := compRightHomeomorph ℝ (iccHomeoI a b h).symm
[GOAL]
case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) :=
  compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := compRightHomeomorph ℝ (Homeomorph.symm (iccHomeoI a b h))
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
[PROOFSTEP]
have w : (W : C(Set.Icc a b, ℝ) → C(I, ℝ)) = W' := rfl
[GOAL]
case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) :=
  compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := compRightHomeomorph ℝ (Homeomorph.symm (iccHomeoI a b h))
w : ↑W = ↑W'
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
[PROOFSTEP]
have p := polynomialFunctions_closure_eq_top'
[GOAL]
case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) :=
  compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := compRightHomeomorph ℝ (Homeomorph.symm (iccHomeoI a b h))
w : ↑W = ↑W'
p : Subalgebra.topologicalClosure (polynomialFunctions I) = ⊤
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
[PROOFSTEP]
apply_fun fun s => s.comap W at p 
[GOAL]
case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) :=
  compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := compRightHomeomorph ℝ (Homeomorph.symm (iccHomeoI a b h))
w : ↑W = ↑W'
p : Subalgebra.comap W (Subalgebra.topologicalClosure (polynomialFunctions I)) = Subalgebra.comap W ⊤
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
[PROOFSTEP]
simp only [Algebra.comap_top] at p 
[GOAL]
case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) :=
  compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := compRightHomeomorph ℝ (Homeomorph.symm (iccHomeoI a b h))
w : ↑W = ↑W'
p :
  Subalgebra.comap (compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h))))
      (Subalgebra.topologicalClosure (polynomialFunctions I)) =
    ⊤
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
[PROOFSTEP]
rw [Subalgebra.topologicalClosure_comap_homeomorph _ W W' w] at p 
[GOAL]
case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) :=
  compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := compRightHomeomorph ℝ (Homeomorph.symm (iccHomeoI a b h))
w : ↑W = ↑W'
p : Subalgebra.topologicalClosure (Subalgebra.comap W (polynomialFunctions I)) = ⊤
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
[PROOFSTEP]
rw [polynomialFunctions.comap_compRightAlgHom_iccHomeoI] at p 
[GOAL]
case inl
a b : ℝ
h : a < b
W : C(↑(Set.Icc a b), ℝ) →ₐ[ℝ] C(↑I, ℝ) :=
  compRightAlgHom ℝ ℝ (Homeomorph.toContinuousMap (Homeomorph.symm (iccHomeoI a b h)))
W' : C(↑(Set.Icc a b), ℝ) ≃ₜ C(↑I, ℝ) := compRightHomeomorph ℝ (Homeomorph.symm (iccHomeoI a b h))
w : ↑W = ↑W'
p : Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
[PROOFSTEP]
exact p
[GOAL]
case inr
a b : ℝ
h : b ≤ a
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
[PROOFSTEP]
have : Subsingleton (Set.Icc a b) := (Set.subsingleton_coe _).mpr $ Set.subsingleton_Icc_of_ge h
[GOAL]
case inr
a b : ℝ
h : b ≤ a
this : Subsingleton ↑(Set.Icc a b)
⊢ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b)) = ⊤
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
⊢ f ∈ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc a b))
[PROOFSTEP]
rw [polynomialFunctions_closure_eq_top _ _]
[GOAL]
a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
⊢ f ∈ ⊤
[PROOFSTEP]
simp
[GOAL]
a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
ε : ℝ
pos : 0 < ε
⊢ ∃ p, ‖Polynomial.toContinuousMapOn p (Set.Icc a b) - f‖ < ε
[PROOFSTEP]
have w := mem_closure_iff_frequently.mp (continuousMap_mem_polynomialFunctions_closure _ _ f)
[GOAL]
a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
ε : ℝ
pos : 0 < ε
w : ∃ᶠ (x : C(↑(Set.Icc a b), ℝ)) in nhds f, x ∈ ↑(polynomialFunctions (Set.Icc a b))
⊢ ∃ p, ‖Polynomial.toContinuousMapOn p (Set.Icc a b) - f‖ < ε
[PROOFSTEP]
rw [Metric.nhds_basis_ball.frequently_iff] at w 
[GOAL]
a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
ε : ℝ
pos : 0 < ε
w : ∀ (i : ℝ), 0 < i → ∃ x, x ∈ Metric.ball f i ∧ x ∈ ↑(polynomialFunctions (Set.Icc a b))
⊢ ∃ p, ‖Polynomial.toContinuousMapOn p (Set.Icc a b) - f‖ < ε
[PROOFSTEP]
obtain ⟨-, H, ⟨m, ⟨-, rfl⟩⟩⟩ := w ε pos
[GOAL]
case intro.intro.intro.intro
a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
ε : ℝ
pos : 0 < ε
w : ∀ (i : ℝ), 0 < i → ∃ x, x ∈ Metric.ball f i ∧ x ∈ ↑(polynomialFunctions (Set.Icc a b))
m : ℝ[X]
H : ↑↑(Polynomial.toContinuousMapOnAlgHom (Set.Icc a b)) m ∈ Metric.ball f ε
⊢ ∃ p, ‖Polynomial.toContinuousMapOn p (Set.Icc a b) - f‖ < ε
[PROOFSTEP]
rw [Metric.mem_ball, dist_eq_norm] at H 
[GOAL]
case intro.intro.intro.intro
a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
ε : ℝ
pos : 0 < ε
w : ∀ (i : ℝ), 0 < i → ∃ x, x ∈ Metric.ball f i ∧ x ∈ ↑(polynomialFunctions (Set.Icc a b))
m : ℝ[X]
H : ‖↑↑(Polynomial.toContinuousMapOnAlgHom (Set.Icc a b)) m - f‖ < ε
⊢ ∃ p, ‖Polynomial.toContinuousMapOn p (Set.Icc a b) - f‖ < ε
[PROOFSTEP]
exact ⟨m, H⟩
[GOAL]
a b : ℝ
f : ℝ → ℝ
c : ContinuousOn f (Set.Icc a b)
ε : ℝ
pos : 0 < ε
⊢ ∃ p, ∀ (x : ℝ), x ∈ Set.Icc a b → |Polynomial.eval x p - f x| < ε
[PROOFSTEP]
let f' : C(Set.Icc a b, ℝ) := ⟨fun x => f x, continuousOn_iff_continuous_restrict.mp c⟩
[GOAL]
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 → |Polynomial.eval x p - f x| < ε
[PROOFSTEP]
obtain ⟨p, b⟩ := exists_polynomial_near_continuousMap a b f' ε pos
[GOAL]
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✝ → |Polynomial.eval x p - f x| < ε
[PROOFSTEP]
use p
[GOAL]
case h
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✝ → |Polynomial.eval x p - f x| < ε
[PROOFSTEP]
rw [norm_lt_iff _ pos] at b 
[GOAL]
case h
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✝ → |Polynomial.eval x p - f x| < ε
[PROOFSTEP]
intro x m
[GOAL]
case h
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✝
⊢ |Polynomial.eval x p - f x| < ε
[PROOFSTEP]
exact b ⟨x, m⟩
