feat(measure_theory/lp_space): continuous functions on compact space …

…are in Lp (#6919)

Continuous functions on a compact space equipped with a finite Borel measure are in Lp, and the inclusion is a bounded linear map.  This follows directly by transferring the construction in #6878 for bounded continuous functions, using the fact that continuous function on a compact space are bounded.

src/analysis/normed_space/linear_isometry.lean

@@ -185,6 +185,8 @@ def of_bounds (e : E ≃ₗ[R] F) (h₁ : ∀ x, ∥e x∥ ≤ ∥x∥) (h₂ :
 /-- Reinterpret a `linear_isometry_equiv` as a `linear_isometry`. -/
 def to_linear_isometry : E →ₗᵢ[R] F := ⟨e.1, e.2⟩
 
+@[simp] lemma coe_to_linear_isometry : ⇑e.to_linear_isometry = e := rfl
+
 protected lemma isometry : isometry e := e.to_linear_isometry.isometry
 
 /-- Reinterpret a `linear_isometry_equiv` as an `isometric`. -/

src/analysis/normed_space/operator_norm.lean

@@ -9,6 +9,7 @@ import analysis.normed_space.riesz_lemma
 import analysis.normed_space.normed_group_hom
 import analysis.asymptotics.asymptotics
 import algebra.algebra.tower
+import data.equiv.transfer_instance
 
 /-!
 # Operator norm on the space of continuous linear maps
@@ -423,6 +424,14 @@ def prodₗᵢ (R : Type*) [ring R] [topological_space R] [module R F] [module R
 protected theorem uniform_continuous : uniform_continuous f :=
 f.lipschitz.uniform_continuous
 
+@[simp, nontriviality] lemma op_norm_subsingleton [subsingleton E] : ∥f∥ = 0 :=
+begin
+  refine le_antisymm _ (norm_nonneg _),
+  apply op_norm_le_bound _ rfl.ge,
+  intros x,
+  simp [subsingleton.elim x 0]
+end
+
 /-- A continuous linear map is an isometry if and only if it preserves the norm. -/
 lemma isometry_iff_norm : isometry f ↔ ∀x, ∥f x∥ = ∥x∥ :=
 f.to_linear_map.to_add_monoid_hom.isometry_iff_norm
@@ -650,6 +659,28 @@ f.to_continuous_linear_map.homothety_norm $ by simp
 
 end linear_isometry
 
+namespace continuous_linear_map
+
+/-- Precomposition with a linear isometry preserves the operator norm. -/
+lemma op_norm_comp_linear_isometry_equiv (f : F →L[𝕜] G) (g : E ≃ₗᵢ[𝕜] F) :
+  ∥f.comp g.to_linear_isometry.to_continuous_linear_map∥ = ∥f∥ :=
+begin
+  casesI subsingleton_or_nontrivial E,
+  { haveI := g.symm.to_linear_equiv.to_equiv.subsingleton,
+    simp },
+  refine le_antisymm _ _,
+  { convert f.op_norm_comp_le g.to_linear_isometry.to_continuous_linear_map,
+    simp [g.to_linear_isometry.norm_to_continuous_linear_map] },
+  { convert (f.comp g.to_linear_isometry.to_continuous_linear_map).op_norm_comp_le
+      g.symm.to_linear_isometry.to_continuous_linear_map,
+    { ext,
+      simp },
+    haveI := g.symm.to_linear_equiv.to_equiv.nontrivial,
+    simp [g.symm.to_linear_isometry.norm_to_continuous_linear_map] },
+end
+
+end continuous_linear_map
+
 namespace linear_map
 
 /-- If a continuous linear map is constructed from a linear map via the constructor `mk_continuous`,

src/measure_theory/lp_space.lean

@@ -6,7 +6,7 @@ Authors: Rémy Degenne, Sébastien Gouëzel
 import measure_theory.ess_sup
 import measure_theory.ae_eq_fun
 import analysis.mean_inequalities
-import topology.continuous_function.bounded
+import topology.continuous_function.compact
 
 /-!
 # ℒp space and Lp space
@@ -1762,6 +1762,8 @@ begin
   { apply_instance }
 end
 
+variables (E p μ)
+
 /-- The normed group homomorphism of considering a bounded continuous function on a finite-measure
 space as an element of `Lp`. -/
 def to_Lp_hom [fact (1 ≤ p)] : normed_group_hom (α →ᵇ E) (Lp E p μ) :=
@@ -1771,7 +1773,7 @@ def to_Lp_hom [fact (1 ≤ p)] : normed_group_hom (α →ᵇ E) (Lp E p μ) :=
       (Lp E p μ)
       mem_Lp }
 
-variables (𝕜 : Type*) (E p μ) [measurable_space 𝕜]
+variables (𝕜 : Type*) [measurable_space 𝕜]
 
 /-- The bounded linear map of considering a bounded continuous function on a finite-measure space
 as an element of `Lp`. -/
@@ -1785,9 +1787,60 @@ linear_map.mk_continuous
   _
   Lp_norm_le
 
+variables {E p 𝕜}
+
 lemma to_Lp_norm_le [nondiscrete_normed_field 𝕜] [opens_measurable_space 𝕜] [normed_space 𝕜 E]
   [fact (1 ≤ p)] :
   ∥to_Lp E p μ 𝕜∥ ≤ (measure_univ_nnreal μ) ^ (p.to_real)⁻¹ :=
 linear_map.mk_continuous_norm_le _ ((measure_univ_nnreal μ) ^ (p.to_real)⁻¹).coe_nonneg _
 
 end bounded_continuous_function
+
+namespace continuous_map
+
+open_locale bounded_continuous_function
+
+variables [borel_space E] [second_countable_topology E]
+variables [topological_space α] [compact_space α] [borel_space α]
+variables [finite_measure μ]
+
+variables (𝕜 : Type*) [measurable_space 𝕜] (E p μ) [fact (1 ≤ p)]
+
+/-- The bounded linear map of considering a continuous function on a compact finite-measure
+space `α` as an element of `Lp`.  By definition, the norm on `C(α, E)` is the sup-norm, transferred
+from the space `α →ᵇ E` of bounded continuous functions, so this construction is just a matter of
+transferring the structure from `bounded_continuous_function.to_Lp` along the isometry. -/
+def to_Lp [normed_field 𝕜] [opens_measurable_space 𝕜] [normed_space 𝕜 E] :
+  C(α, E) →L[𝕜] (Lp E p μ) :=
+(bounded_continuous_function.to_Lp E p μ 𝕜).comp
+  (linear_isometry_bounded_of_compact α E 𝕜).to_linear_isometry.to_continuous_linear_map
+
+variables {E p 𝕜}
+
+lemma to_Lp_def [normed_field 𝕜] [opens_measurable_space 𝕜] [normed_space 𝕜 E] (f : C(α, E)) :
+  to_Lp E p μ 𝕜 f
+  = bounded_continuous_function.to_Lp E p μ 𝕜 (linear_isometry_bounded_of_compact α E 𝕜 f) :=
+rfl
+
+@[simp] lemma to_Lp_comp_forget_boundedness [normed_field 𝕜] [opens_measurable_space 𝕜]
+  [normed_space 𝕜 E] (f : α →ᵇ E) :
+  to_Lp E p μ 𝕜 (bounded_continuous_function.forget_boundedness α E f)
+  = bounded_continuous_function.to_Lp E p μ 𝕜 f :=
+rfl
+
+@[simp] lemma coe_to_Lp [normed_field 𝕜] [opens_measurable_space 𝕜] [normed_space 𝕜 E]
+  (f : C(α, E)) :
+  (to_Lp E p μ 𝕜 f : α →ₘ[μ] E) = f.to_ae_eq_fun μ :=
+rfl
+
+variables [nondiscrete_normed_field 𝕜] [opens_measurable_space 𝕜] [normed_space 𝕜 E]
+
+lemma to_Lp_norm_eq_to_Lp_norm_coe :
+  ∥to_Lp E p μ 𝕜∥ = ∥bounded_continuous_function.to_Lp E p μ 𝕜∥ :=
+(bounded_continuous_function.to_Lp E p μ 𝕜).op_norm_comp_linear_isometry_equiv _
+
+/-- Bound for the operator norm of `continuous_map.to_Lp`. -/
+lemma to_Lp_norm_le : ∥to_Lp E p μ 𝕜∥ ≤ (measure_univ_nnreal μ) ^ (p.to_real)⁻¹ :=
+by { rw to_Lp_norm_eq_to_Lp_norm_coe, exact bounded_continuous_function.to_Lp_norm_le μ }
+
+end continuous_map

src/topology/continuous_function/basic.lean

@@ -83,6 +83,16 @@ def const (b : β) : C(α, β) := ⟨λ x, b⟩
 @[simp] lemma const_coe (b : β) : (const b : α → β) = (λ x, b) := rfl
 lemma const_apply (b : β) (a : α) : const b a = b := rfl
 
+instance [nonempty α] [nontrivial β] : nontrivial C(α, β) :=
+{ exists_pair_ne := begin
+    obtain ⟨b₁, b₂, hb⟩ := exists_pair_ne β,
+    refine ⟨const b₁, const b₂, _⟩,
+    contrapose! hb,
+    inhabit α,
+    change const b₁ (default α) = const b₂ (default α),
+    simp [hb]
+  end }
+
 section
 variables [linear_ordered_add_comm_group β] [order_topology β]
 

src/topology/continuous_function/compact.lean

@@ -125,31 +125,31 @@ variables (α 𝕜)
 
 /--
 When `α` is compact and `𝕜` is a normed field,
-the `𝕜`-algebra of bounded continuous maps `α →ᵇ 𝕜` is
-`𝕜`-linearly isometric to `C(α, 𝕜)`.
+the `𝕜`-algebra of bounded continuous maps `α →ᵇ β` is
+`𝕜`-linearly isometric to `C(α, β)`.
 -/
 def linear_isometry_bounded_of_compact :
-  C(α, 𝕜) ≃ₗᵢ[𝕜] (α →ᵇ 𝕜) :=
+  C(α, β) ≃ₗᵢ[𝕜] (α →ᵇ β) :=
 { map_smul' := λ c f, by { ext, simp, },
   norm_map' := λ f, rfl,
-  ..add_equiv_bounded_of_compact α 𝕜 }
+  ..add_equiv_bounded_of_compact α β }
 
 @[simp]
 lemma linear_isometry_bounded_of_compact_to_isometric :
-  (linear_isometry_bounded_of_compact α 𝕜).to_isometric =
-    isometric_bounded_of_compact α 𝕜 :=
+  (linear_isometry_bounded_of_compact α β 𝕜).to_isometric =
+    isometric_bounded_of_compact α β :=
 rfl
 
 @[simp]
 lemma linear_isometry_bounded_of_compact_to_add_equiv :
-  (linear_isometry_bounded_of_compact α 𝕜).to_linear_equiv.to_add_equiv =
-    add_equiv_bounded_of_compact α 𝕜 :=
+  (linear_isometry_bounded_of_compact α β 𝕜).to_linear_equiv.to_add_equiv =
+    add_equiv_bounded_of_compact α β :=
 rfl
 
 @[simp]
 lemma linear_isometry_bounded_of_compact_of_compact_to_equiv :
-  (linear_isometry_bounded_of_compact α 𝕜).to_linear_equiv.to_equiv =
-    equiv_bounded_of_compact α 𝕜 :=
+  (linear_isometry_bounded_of_compact α β 𝕜).to_linear_equiv.to_equiv =
+    equiv_bounded_of_compact α β :=
 rfl
 
 end