feat(topology/continuous_function/stone_weierstrass): complex Stone-W…

…eierstrass (#8012)

src/analysis/complex/basic.lean

@@ -73,6 +73,11 @@ by rw [norm_real, real.norm_eq_abs]
 lemma norm_int_of_nonneg {n : ℤ} (hn : 0 ≤ n) : ∥(n : ℂ)∥ = n :=
 by rw [norm_int, _root_.abs_of_nonneg]; exact int.cast_nonneg.2 hn
 
+@[continuity] lemma continuous_abs : continuous abs := continuous_norm
+
+@[continuity] lemma continuous_norm_sq : continuous norm_sq :=
+by simpa [← norm_sq_eq_abs] using continuous_abs.pow 2
+
 open continuous_linear_map
 
 /-- Continuous linear map version of the real part function, from `ℂ` to `ℝ`. -/

src/topology/algebra/module.lean

@@ -122,6 +122,11 @@ lemma submodule.topological_closure_minimal
   s.topological_closure ≤ t :=
 closure_minimal h ht
 
+lemma submodule.topological_closure_mono {s : submodule R M} {t : submodule R M} (h : s ≤ t) :
+  s.topological_closure ≤ t.topological_closure :=
+s.topological_closure_minimal (h.trans t.submodule_topological_closure)
+  t.is_closed_topological_closure
+
 end closure
 
 /-- Continuous linear maps between modules. We only put the type classes that are necessary for the
@@ -237,6 +242,14 @@ lemma ext_on [t2_space M₂] {s : set M} (hs : dense (submodule.span R s : set M
   f = g :=
 ext $ λ x, eq_on_closure_span h (hs x)
 
+/-- Under a continuous linear map, the image of the `topological_closure` of a submodule is
+contained in the `topological_closure` of its image. -/
+lemma _root_.submodule.topological_closure_map [topological_space R] [has_continuous_smul R M]
+  [has_continuous_add M] [has_continuous_smul R M₂] [has_continuous_add M₂] (f : M →L[R] M₂)
+  (s : submodule R M) :
+  (s.topological_closure.map f.to_linear_map) ≤ (s.map f.to_linear_map).topological_closure :=
+image_closure_subset_closure_image f.continuous
+
 /-- The continuous map that is constantly zero. -/
 instance: has_zero (M →L[R] M₂) := ⟨⟨0, continuous_zero⟩⟩
 instance : inhabited (M →L[R] M₂) := ⟨0⟩

src/topology/continuous_function/algebra.lean

@@ -438,6 +438,9 @@ def continuous_map.coe_fn_alg_hom : C(α, A) →ₐ[R] (α → A) :=
   map_add' := continuous_map.coe_add,
   map_mul' := continuous_map.coe_mul }
 
+instance: is_scalar_tower R A C(α, A) :=
+{ smul_assoc := λ _ _ _, by { ext, simp } }
+
 variables {R}
 
 /--

src/topology/continuous_function/bounded.lean

@@ -3,7 +3,7 @@ Copyright (c) 2018 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel, Mario Carneiro, Yury Kudryashov, Heather Macbeth
 -/
-import analysis.normed_space.basic
+import analysis.normed_space.operator_norm
 import topology.continuous_function.algebra
 
 /-!
@@ -605,10 +605,13 @@ In this section, if `β` is a normed space, then we show that the space of bound
 continuous functions from `α` to `β` inherits a normed space structure, by using
 pointwise operations and checking that they are compatible with the uniform distance. -/
 
-variables {𝕜 : Type*} [normed_field 𝕜]
-variables [topological_space α] [normed_group β] [normed_space 𝕜 β]
+variables {𝕜 : Type*}
+variables [topological_space α] [normed_group β]
 variables {f g : α →ᵇ β} {x : α} {C : ℝ}
 
+section normed_field
+variables [normed_field 𝕜] [normed_space 𝕜 β]
+
 instance : has_scalar 𝕜 (α →ᵇ β) :=
 ⟨λ c f, of_normed_group (c • f) (f.continuous.const_smul c) (∥c∥ * ∥f∥) $ λ x,
   trans_rel_right _ (norm_smul _ _)
@@ -647,6 +650,35 @@ def forget_boundedness_linear_map : (α →ᵇ β) →ₗ[𝕜] C(α, β) :=
   map_smul' := by { intros, ext, simp, },
   map_add' := by { intros, ext, simp, }, }
 
+end normed_field
+
+variables [nondiscrete_normed_field 𝕜] [normed_space 𝕜 β]
+variables [normed_group γ] [normed_space 𝕜 γ]
+
+variables (α)
+/--
+Postcomposition of bounded continuous functions into a normed module by a continuous linear map is
+a continuous linear map.
+Upgraded version of `continuous_linear_map.comp_left_continuous`, similar to
+`linear_map.comp_left`. -/
+protected def _root_.continuous_linear_map.comp_left_continuous_bounded (g : β →L[𝕜] γ) :
+  (α →ᵇ β) →L[𝕜] (α →ᵇ γ) :=
+linear_map.mk_continuous
+  { to_fun := λ f, of_normed_group
+      (g ∘ f)
+      (g.continuous.comp f.continuous)
+      (∥g∥ * ∥f∥)
+      (λ x, (g.le_op_norm_of_le (f.norm_coe_le_norm x))),
+    map_add' := λ f g, by ext; simp,
+    map_smul' := λ c f, by ext; simp }
+  ∥g∥
+  (λ f, norm_of_normed_group_le _ (mul_nonneg (norm_nonneg g) (norm_nonneg f)) _)
+
+@[simp] lemma _root_.continuous_linear_map.comp_left_continuous_bounded_apply (g : β →L[𝕜] γ)
+  (f : α →ᵇ β) (x : α) :
+  (g.comp_left_continuous_bounded α f) x = g (f x) :=
+rfl
+
 end normed_space
 
 section normed_ring

src/topology/continuous_function/compact.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import topology.continuous_function.bounded
-import analysis.normed_space.linear_isometry
 import topology.uniform_space.compact_separated
 import tactic.equiv_rw
 
@@ -203,6 +202,17 @@ def linear_isometry_bounded_of_compact :
   norm_map' := λ f, rfl,
   ..add_equiv_bounded_of_compact α β }
 
+-- this lemma and the next are the analogues of those autogenerated by `@[simps]` for
+-- `equiv_bounded_of_compact`, `add_equiv_bounded_of_compact`
+@[simp] lemma linear_isometry_bounded_of_compact_symm_apply (f : α →ᵇ β) :
+  (linear_isometry_bounded_of_compact α β 𝕜).symm f = f.forget_boundedness α β :=
+rfl
+
+@[simp] lemma linear_isometry_bounded_of_compact_apply_apply (f : C(α, β)) (a : α) :
+  ((linear_isometry_bounded_of_compact α β 𝕜) f) a = f a :=
+rfl
+
+
 @[simp]
 lemma linear_isometry_bounded_of_compact_to_isometric :
   (linear_isometry_bounded_of_compact α β 𝕜).to_isometric =
@@ -268,6 +278,39 @@ classical.some_spec (classical.some_spec (uniform_continuity f ε h)) w
 
 end uniform_continuity
 
+end continuous_map
+
+section comp_left
+variables (X : Type*) {𝕜 β γ : Type*} [topological_space X] [compact_space X]
+  [nondiscrete_normed_field 𝕜]
+variables [normed_group β] [normed_space 𝕜 β] [normed_group γ] [normed_space 𝕜 γ]
+
+open continuous_map
+
+/--
+Postcomposition of continuous functions into a normed module by a continuous linear map is a
+continuous linear map.
+Transferred version of `continuous_linear_map.comp_left_continuous_bounded`,
+upgraded version of `continuous_linear_map.comp_left_continuous`,
+similar to `linear_map.comp_left`. -/
+protected def continuous_linear_map.comp_left_continuous_compact (g : β →L[𝕜] γ) :
+  C(X, β) →L[𝕜] C(X, γ) :=
+(linear_isometry_bounded_of_compact X γ 𝕜).symm.to_linear_isometry.to_continuous_linear_map.comp $
+(g.comp_left_continuous_bounded X).comp $
+(linear_isometry_bounded_of_compact X β 𝕜).to_linear_isometry.to_continuous_linear_map
+
+@[simp] lemma continuous_linear_map.to_linear_comp_left_continuous_compact (g : β →L[𝕜] γ) :
+  (g.comp_left_continuous_compact X : C(X, β) →ₗ[𝕜] C(X, γ)) = g.comp_left_continuous 𝕜 X :=
+by { ext f, simp [continuous_linear_map.comp_left_continuous_compact] }
+
+@[simp] lemma continuous_linear_map.comp_left_continuous_compact_apply (g : β →L[𝕜] γ)
+  (f : C(X, β)) (x : X) :
+  g.comp_left_continuous_compact X f x = g (f x) :=
+rfl
+
+end comp_left
+
+namespace continuous_map
 /-!
 We now setup variations on `comp_right_* f`, where `f : C(X, Y)`
 (that is, precomposition by a continuous map),

src/topology/continuous_function/stone_weierstrass.lean

@@ -1,9 +1,10 @@
 /-
 Copyright (c) 2021 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Scott Morrison, Heather Macbeth
 -/
 import topology.continuous_function.weierstrass
+import analysis.complex.basic
 
 /-!
 # The Stone-Weierstrass theorem
@@ -28,12 +29,12 @@ We argue as follows.
 * Finally we put these pieces together. `L = A.topological_closure` is a nonempty sublattice
   which separates points since `A` does, and so is dense (in fact equal to `⊤`).
 
-## Future work
-
-Prove the complex version for self-adjoint subalgebras `A`, by separately approximating
+We then prove the complex version for self-adjoint subalgebras `A`, by separately approximating
 the real and imaginary parts using the real subalgebra of real-valued functions in `A`
 (which still separates points, by taking the norm-square of a separating function).
 
+## Future work
+
 Extend to cover the case of subalgebras of the continuous functions vanishing at infinity,
 on non-compact spaces.
 
@@ -355,5 +356,101 @@ begin
   rwa norm_lt_iff _ pos at b,
 end
 
+end continuous_map
+
+section complex
+open complex
+
+-- Redefine `X`, since for the next few lemmas it need not be compact
+variables {X : Type*} [topological_space X]
+
+namespace continuous_map
+
+/-- A real subalgebra of `C(X, ℂ)` is `conj_invariant`, if it contains all its conjugates. -/
+def conj_invariant_subalgebra (A : subalgebra ℝ C(X, ℂ)) : Prop :=
+A.map (conj_ae.to_alg_hom.comp_left_continuous ℝ conj_cle.continuous) ≤ A
+
+lemma mem_conj_invariant_subalgebra {A : subalgebra ℝ C(X, ℂ)} (hA : conj_invariant_subalgebra A)
+  {f : C(X, ℂ)} (hf : f ∈ A) :
+  (conj_ae.to_alg_hom.comp_left_continuous ℝ conj_cle.continuous) f ∈ A :=
+hA ⟨f, hf, rfl⟩
 
 end continuous_map
+
+open continuous_map
+
+/-- If a conjugation-invariant subalgebra of `C(X, ℂ)` separates points, then the real subalgebra
+of its purely real-valued elements also separates points. -/
+lemma subalgebra.separates_points.complex_to_real {A : subalgebra ℂ C(X, ℂ)}
+  (hA : A.separates_points) (hA' : conj_invariant_subalgebra (A.restrict_scalars ℝ)) :
+  ((A.restrict_scalars ℝ).comap'
+    (of_real_am.comp_left_continuous ℝ continuous_of_real)).separates_points :=
+begin
+  intros x₁ x₂ hx,
+  -- Let `f` in the subalgebra `A` separate the points `x₁`, `x₂`
+  obtain ⟨_, ⟨f, hfA, rfl⟩, hf⟩ := hA hx,
+  let F : C(X, ℂ) := f - const (f x₂),
+  -- Subtract the constant `f x₂` from `f`; this is still an element of the subalgebra
+  have hFA : F ∈ A,
+  { refine A.sub_mem hfA _,
+    convert A.smul_mem A.one_mem (f x₂),
+    ext1,
+    simp },
+  -- Consider now the function `λ x, |f x - f x₂| ^ 2`
+  refine ⟨_, ⟨(⟨complex.norm_sq, continuous_norm_sq⟩ : C(ℂ, ℝ)).comp F, _, rfl⟩, _⟩,
+  { -- This is also an element of the subalgebra, and takes only real values
+    rw [set_like.mem_coe, subalgebra.mem_comap],
+    convert (A.restrict_scalars ℝ).mul_mem (mem_conj_invariant_subalgebra hA' hFA) hFA,
+    ext1,
+    exact complex.norm_sq_eq_conj_mul_self },
+  { -- And it also separates the points `x₁`, `x₂`
+    have : f x₁ - f x₂ ≠ 0 := sub_ne_zero.mpr hf,
+    simpa using this },
+end
+
+variables [compact_space X]
+
+/--
+The Stone-Weierstrass approximation theorem, complex version,
+that a subalgebra `A` of `C(X, ℂ)`, where `X` is a compact topological space,
+is dense if it is conjugation-invariant and separates points.
+-/
+theorem continuous_map.subalgebra_complex_topological_closure_eq_top_of_separates_points
+  (A : subalgebra ℂ C(X, ℂ)) (hA : A.separates_points)
+  (hA' : conj_invariant_subalgebra (A.restrict_scalars ℝ)) :
+  A.topological_closure = ⊤ :=
+begin
+  rw algebra.eq_top_iff,
+  -- Let `I` be the natural inclusion of `C(X, ℝ)` into `C(X, ℂ)`
+  let I : C(X, ℝ) →ₗ[ℝ] C(X, ℂ) := of_real_clm.comp_left_continuous ℝ X,
+  -- The main point of the proof is that its range (i.e., every real-valued function) is contained
+  -- in the closure of `A`
+  have key : I.range ≤ (A.to_submodule.restrict_scalars ℝ).topological_closure,
+  { -- Let `A₀` be the subalgebra of `C(X, ℝ)` consisting of `A`'s purely real elements; it is the
+    -- preimage of `A` under `I`.  In this argument we only need its submodule structure.
+    let A₀ : submodule ℝ C(X, ℝ) := (A.to_submodule.restrict_scalars ℝ).comap I,
+    -- By `subalgebra.separates_points.complex_to_real`, this subalgebra also separates points, so
+    -- we may apply the real Stone-Weierstrass result to it.
+    have SW : A₀.topological_closure = ⊤,
+    { have := subalgebra_topological_closure_eq_top_of_separates_points _ (hA.complex_to_real hA'),
+      exact congr_arg subalgebra.to_submodule this },
+    rw [← submodule.map_top, ← SW],
+    -- So it suffices to prove that the image under `I` of the closure of `A₀` is contained in the
+    -- closure of `A`, which follows by abstract nonsense
+    have h₁ := A₀.topological_closure_map (of_real_clm.comp_left_continuous_compact X),
+    have h₂ := (A.to_submodule.restrict_scalars ℝ).map_comap_le I,
+    exact h₁.trans (submodule.topological_closure_mono h₂) },
+  -- In particular, for a function `f` in `C(X, ℂ)`, the real and imaginary parts of `f` are in the
+  -- closure of `A`
+  intros f,
+  let f_re : C(X, ℝ) := (⟨complex.re, complex.re_clm.continuous⟩ : C(ℂ, ℝ)).comp f,
+  let f_im : C(X, ℝ) := (⟨complex.im, complex.im_clm.continuous⟩ : C(ℂ, ℝ)).comp f,
+  have h_f_re : I f_re ∈ A.topological_closure := key ⟨f_re, rfl⟩,
+  have h_f_im : I f_im ∈ A.topological_closure := key ⟨f_im, rfl⟩,
+  -- So `f_re + complex.I • f_im` is in the closure of `A`
+  convert A.topological_closure.add_mem h_f_re (A.topological_closure.smul_mem h_f_im complex.I),
+  -- And this, of course, is just `f`
+  ext; simp [I]
+end
+
+end complex