feat(measure_theory/lp_space): bounded continuous functions are in Lp (…

…#6878)

Under appropriate conditions (finite Borel measure, second-countable), a bounded continuous function is in L^p.  The main result of this PR is `bounded_continuous_function.to_Lp`, which provides this operation as a bounded linear map.  There are also several variations.

src/data/real/ennreal.lean

@@ -373,6 +373,14 @@ lemma coe_le_iff : ↑r ≤ a ↔ (∀p:ℝ≥0, a = p → r ≤ p) := with_top.
 
 lemma lt_iff_exists_coe : a < b ↔ (∃p:ℝ≥0, a = p ∧ ↑p < b) := with_top.lt_iff_exists_coe
 
+lemma to_real_le_coe_of_le_coe {a : ℝ≥0∞} {b : ℝ≥0} (h : a ≤ b) : a.to_real ≤ b :=
+show ↑a.to_nnreal ≤ ↑b,
+begin
+  have : ↑a.to_nnreal = a := ennreal.coe_to_nnreal (lt_of_le_of_lt h coe_lt_top).ne,
+  rw ← this at h,
+  exact_mod_cast h
+end
+
 @[simp, norm_cast] lemma coe_finset_sup {s : finset α} {f : α → ℝ≥0} :
   ↑(s.sup f) = s.sup (λ x, (f x : ℝ≥0∞)) :=
 finset.comp_sup_eq_sup_comp_of_is_total _ coe_mono rfl

src/measure_theory/ae_eq_fun.lean

@@ -440,3 +440,44 @@ end pos_part
 end ae_eq_fun
 
 end measure_theory
+
+namespace continuous_map
+
+open measure_theory
+
+variables [topological_space α] [borel_space α] (μ)
+variables [topological_space β] [measurable_space β] [borel_space β]
+
+/-- The equivalence class of `μ`-almost-everywhere measurable functions associated to a continuous
+map. -/
+def to_ae_eq_fun (f : C(α, β)) : α →ₘ[μ] β :=
+ae_eq_fun.mk f f.continuous.measurable.ae_measurable
+
+lemma coe_fn_to_ae_eq_fun (f : C(α, β)) : f.to_ae_eq_fun μ =ᵐ[μ] f :=
+ae_eq_fun.coe_fn_mk f _
+
+variables [group β] [topological_group β] [second_countable_topology β]
+
+/-- The `mul_hom` from the group of continuous maps from `α` to `β` to the group of equivalence
+classes of `μ`-almost-everywhere measurable functions. -/
+@[to_additive "The `add_hom` from the group of continuous maps from `α` to `β` to the group of
+equivalence classes of `μ`-almost-everywhere measurable functions."]
+def to_ae_eq_fun_mul_hom : C(α, β) →* α →ₘ[μ] β :=
+{ to_fun := continuous_map.to_ae_eq_fun μ,
+  map_one' := rfl,
+  map_mul' := λ f g, ae_eq_fun.mk_mul_mk f g f.continuous.measurable.ae_measurable
+    g.continuous.measurable.ae_measurable }
+
+variables {𝕜 : Type*} [semiring 𝕜] [topological_space 𝕜] [measurable_space 𝕜]
+  [opens_measurable_space 𝕜]
+variables [topological_space γ] [measurable_space γ] [borel_space γ] [add_comm_group γ]
+  [semimodule 𝕜 γ] [topological_add_group γ] [has_continuous_smul 𝕜 γ]
+  [second_countable_topology γ]
+
+/-- The linear map from the group of continuous maps from `α` to `β` to the group of equivalence
+classes of `μ`-almost-everywhere measurable functions. -/
+def to_ae_eq_fun_linear_map : C(α, γ) →ₗ[𝕜] α →ₘ[μ] γ :=
+{ map_smul' := λ c f, ae_eq_fun.smul_mk c f f.continuous.measurable.ae_measurable,
+  .. to_ae_eq_fun_add_hom μ }
+
+end continuous_map

src/measure_theory/lp_space.lean

@@ -6,6 +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
 
 /-!
 # ℒp space and Lp space
@@ -37,6 +38,10 @@ that it is continuous. In particular,
 * `Lp.pos_part` is the positive part of an `Lp` function.
 * `Lp.neg_part` is the negative part of an `Lp` function.
 
+When `α` is a topological space equipped with a finite Borel measure, there is a bounded linear map
+from the normed space of bounded continuous functions (`α →ᵇ E`) to `Lp E p μ`.  We construct this
+as `bounded_continuous_function.to_Lp`.
+
 ## Notations
 
 * `α →₁[μ] E` : the type `Lp E 1 μ`.
@@ -321,6 +326,21 @@ begin
   { exact snorm'_mono_ae ennreal.to_real_nonneg h }
 end
 
+lemma snorm_le_of_ae_bound {f : α → F} {C : ℝ} (hfC : ∀ᵐ x ∂μ, ∥f x∥ ≤ C) :
+  snorm f p μ ≤ ((μ set.univ) ^ p.to_real⁻¹) * (ennreal.of_real C) :=
+begin
+  by_cases hμ : μ = 0,
+  { simp [hμ] },
+  haveI : μ.ae.ne_bot := ae_ne_bot.mpr hμ,
+  by_cases hp : p = 0,
+  { simp [hp] },
+  have hC : 0 ≤ C, from le_trans (norm_nonneg _) hfC.exists.some_spec,
+  have hC' : ∥C∥ = C := by rw [real.norm_eq_abs, abs_eq_self.mpr hC],
+  have : ∀ᵐ x ∂μ, ∥f x∥ ≤ ∥(λ _, C) x∥, from hfC.mono (λ x hx, hx.trans (le_of_eq hC'.symm)),
+  convert snorm_mono_ae this,
+  rw [snorm_const _ hp hμ, mul_comm, ← of_real_norm_eq_coe_nnnorm, hC', one_div]
+end
+
 lemma snorm_congr_norm_ae {f : α → F} {g : α → G} (hfg : ∀ᵐ x ∂μ, ∥f x∥ = ∥g x∥) :
   snorm f p μ = snorm g p μ :=
 le_antisymm (snorm_mono_ae $ eventually_eq.le hfg)
@@ -388,6 +408,11 @@ lemma mem_ℒp.of_le [measurable_space F] {f : α → E} {g : α → F}
   (hg : mem_ℒp g p μ) (hf : ae_measurable f μ) (hfg : ∀ᵐ x ∂μ, ∥f x∥ ≤ ∥g x∥) : mem_ℒp f p μ :=
 ⟨hf, (snorm_mono_ae hfg).trans_lt hg.snorm_lt_top⟩
 
+lemma mem_ℒp.of_bound [finite_measure μ] {f : α → E} (hf : ae_measurable f μ)
+  (C : ℝ) (hfC : ∀ᵐ x ∂μ, ∥f x∥ ≤ C) :
+  mem_ℒp f p μ :=
+(mem_ℒp_const C).of_le hf (hfC.mono (λ x hx, le_trans hx (le_abs_self _)))
+
 section opens_measurable_space
 variable [opens_measurable_space E]
 
@@ -1029,11 +1054,33 @@ end
 
 lemma mem_Lp_of_ae_le_mul [second_countable_topology F] [measurable_space F] [borel_space F]
   {c : ℝ} {f : α →ₘ[μ] E} {g : Lp F p μ} (h : ∀ᵐ x ∂μ, ∥f x∥ ≤ c * ∥g x∥) : f ∈ Lp E p μ :=
-mem_Lp_iff_mem_ℒp.2 $ mem_ℒp.of_le_mul (Lp.mem_ℒp g) (ae_eq_fun.ae_measurable f) h
+mem_Lp_iff_mem_ℒp.2 $ mem_ℒp.of_le_mul (Lp.mem_ℒp g) f.ae_measurable h
 
 lemma mem_Lp_of_ae_le [second_countable_topology F] [measurable_space F] [borel_space F]
   {f : α →ₘ[μ] E} {g : Lp F p μ} (h : ∀ᵐ x ∂μ, ∥f x∥ ≤ ∥g x∥) : f ∈ Lp E p μ :=
-mem_Lp_iff_mem_ℒp.2 $ mem_ℒp.of_le (Lp.mem_ℒp g) (ae_eq_fun.ae_measurable f) h
+mem_Lp_iff_mem_ℒp.2 $ mem_ℒp.of_le (Lp.mem_ℒp g) f.ae_measurable h
+
+lemma mem_Lp_of_ae_bound [finite_measure μ] {f : α →ₘ[μ] E} (C : ℝ) (hfC : ∀ᵐ x ∂μ, ∥f x∥ ≤ C) :
+  f ∈ Lp E p μ :=
+mem_Lp_iff_mem_ℒp.2 $ mem_ℒp.of_bound f.ae_measurable _ hfC
+
+lemma norm_le_of_ae_bound [finite_measure μ] {f : Lp E p μ} {C : ℝ} (hC : 0 ≤ C)
+  (hfC : ∀ᵐ x ∂μ, ∥f x∥ ≤ C) :
+  ∥f∥ ≤ (measure_univ_nnreal μ) ^ (p.to_real)⁻¹ * C :=
+begin
+  by_cases hμ : μ = 0,
+  { by_cases hp : p.to_real⁻¹ = 0,
+    { simpa [hp, hμ, norm_def] using hC },
+    { simp [hμ, norm_def, real.zero_rpow hp] } },
+  let A : ℝ≥0 := (measure_univ_nnreal μ) ^ (p.to_real)⁻¹ * ⟨C, hC⟩,
+  suffices : snorm f p μ ≤ A,
+  { exact ennreal.to_real_le_coe_of_le_coe this },
+  convert snorm_le_of_ae_bound hfC,
+  rw [← coe_measure_univ_nnreal μ, ennreal.coe_rpow_of_ne_zero (measure_univ_nnreal_pos hμ).ne',
+    ennreal.coe_mul],
+  congr,
+  rw max_eq_left hC
+end
 
 instance [hp : fact (1 ≤ p)] : normed_group (Lp E p μ) :=
 normed_group.of_core _
@@ -1066,17 +1113,22 @@ begin
   exact or.inl ⟨ennreal.coe_lt_top, f.prop⟩,
 end
 
-instance : has_scalar 𝕜 (Lp E p μ) := { smul := λ c f, ⟨c • ↑f, mem_Lp_const_smul c f⟩ }
+variables (E p μ 𝕜)
 
-lemma coe_fn_smul (c : 𝕜) (f : Lp E p μ) : ⇑(c • f) =ᵐ[μ] c • f := ae_eq_fun.coe_fn_smul _ _
+/-- The `𝕜`-submodule of elements of `α →ₘ[μ] E` whose `Lp` norm is finite.  This is `Lp E p μ`,
+with extra structure. -/
+def Lp_submodule : submodule 𝕜 (α →ₘ[μ] E) :=
+{ smul_mem' := λ c f hf, by simpa using mem_Lp_const_smul c ⟨f, hf⟩,
+  .. Lp E p μ }
+
+variables {E p μ 𝕜}
+
+lemma coe_Lp_submodule : (Lp_submodule E p μ 𝕜).to_add_subgroup = Lp E p μ := rfl
 
 instance : semimodule 𝕜 (Lp E p μ) :=
-{ one_smul := λ _, subtype.eq (one_smul 𝕜 _),
-  mul_smul := λ _ _ _, subtype.eq (mul_smul _ _ _),
-  smul_add := λ _ _ _, subtype.eq (smul_add _ _ _),
-  smul_zero := λ _, subtype.eq (smul_zero _),
-  add_smul := λ _ _ _, subtype.eq (add_smul _ _ _),
-  zero_smul := λ _, subtype.eq (zero_smul _ _) }
+{ .. (Lp_submodule E p μ 𝕜).semimodule }
+
+lemma coe_fn_smul (c : 𝕜) (f : Lp E p μ) : ⇑(c • f) =ᵐ[μ] c • f := ae_eq_fun.coe_fn_smul _ _
 
 lemma norm_const_smul (c : 𝕜) (f : Lp E p μ) : ∥c • f∥ = ∥c∥ * ∥f∥ :=
 by rw [norm_def, snorm_congr_ae (coe_fn_smul _ _), snorm_const_smul c,
@@ -1679,3 +1731,63 @@ end Lp
 end measure_theory
 
 end complete_space
+
+namespace bounded_continuous_function
+
+open_locale bounded_continuous_function
+variables [borel_space E] [second_countable_topology E]
+variables [topological_space α] [borel_space α]
+variables [finite_measure μ]
+
+/-- A bounded continuous function is in `Lp`. -/
+lemma mem_Lp (f : α →ᵇ E) :
+  f.to_continuous_map.to_ae_eq_fun μ ∈ Lp E p μ :=
+begin
+  refine Lp.mem_Lp_of_ae_bound (∥f∥) _,
+  filter_upwards [f.to_continuous_map.coe_fn_to_ae_eq_fun μ],
+  intros x hx,
+  convert f.norm_coe_le_norm x
+end
+
+/-- The `Lp`-norm of a bounded continuous function is at most a constant (depending on the measure
+of the whole space) times its sup-norm. -/
+lemma Lp_norm_le (f : α →ᵇ E) :
+  ∥(⟨f.to_continuous_map.to_ae_eq_fun μ, mem_Lp f⟩ : Lp E p μ)∥
+  ≤ (measure_univ_nnreal μ) ^ (p.to_real)⁻¹ * ∥f∥ :=
+begin
+  apply Lp.norm_le_of_ae_bound (norm_nonneg f),
+  { refine (f.to_continuous_map.coe_fn_to_ae_eq_fun μ).mono _,
+    intros x hx,
+    convert f.norm_coe_le_norm x },
+  { apply_instance }
+end
+
+/-- 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 μ) :=
+{ bound' := ⟨_, Lp_norm_le⟩,
+  .. add_monoid_hom.cod_restrict
+      ((continuous_map.to_ae_eq_fun_add_hom μ).comp (forget_boundedness_add_hom α E))
+      (Lp E p μ)
+      mem_Lp }
+
+variables (𝕜 : Type*) (E p μ) [measurable_space 𝕜]
+
+/-- The bounded linear map of considering a bounded continuous function on a finite-measure space
+as an element of `Lp`. -/
+def to_Lp [normed_field 𝕜] [opens_measurable_space 𝕜] [normed_space 𝕜 E] [fact (1 ≤ p)] :
+  (α →ᵇ E) →L[𝕜] (Lp E p μ) :=
+linear_map.mk_continuous
+  (linear_map.cod_restrict
+    (Lp.Lp_submodule E p μ 𝕜)
+    ((continuous_map.to_ae_eq_fun_linear_map μ).comp (forget_boundedness_linear_map α E))
+    mem_Lp)
+  _
+  Lp_norm_le
+
+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

src/measure_theory/measure_space.lean

@@ -85,7 +85,7 @@ measure, almost everywhere, measure space, completion, null set, null measurable
 noncomputable theory
 
 open classical set filter (hiding map) function measurable_space
-open_locale classical topological_space big_operators filter ennreal
+open_locale classical topological_space big_operators filter ennreal nnreal
 
 variables {α β γ δ ι : Type*}
 
@@ -1666,6 +1666,29 @@ lemma measure_lt_top (μ : measure α) [finite_measure μ] (s : set α) : μ s <
 lemma measure_ne_top (μ : measure α) [finite_measure μ] (s : set α) : μ s ≠ ∞ :=
 ne_of_lt (measure_lt_top μ s)
 
+/-- The measure of the whole space with respect to a finite measure, considered as `ℝ≥0`. -/
+def measure_univ_nnreal (μ : measure α) : ℝ≥0 := (μ univ).to_nnreal
+
+@[simp] lemma coe_measure_univ_nnreal (μ : measure α) [finite_measure μ] :
+  ↑(measure_univ_nnreal μ) = μ univ :=
+ennreal.coe_to_nnreal (measure_ne_top μ univ)
+
+instance finite_measure_zero : finite_measure (0 : measure α) := ⟨by simp⟩
+
+@[simp] lemma measure_univ_nnreal_zero : measure_univ_nnreal (0 : measure α) = 0 := rfl
+
+@[simp] lemma measure_univ_nnreal_eq_zero [finite_measure μ] : measure_univ_nnreal μ = 0 ↔ μ = 0 :=
+begin
+  rw [← measure_theory.measure.measure_univ_eq_zero, ← coe_measure_univ_nnreal],
+  norm_cast
+end
+
+lemma measure_univ_nnreal_pos [finite_measure μ] (hμ : μ ≠ 0) : 0 < measure_univ_nnreal μ :=
+begin
+  contrapose! hμ,
+  simpa [measure_univ_nnreal_eq_zero, le_zero_iff] using hμ
+end
+
 /-- `le_of_add_le_add_left` is normally applicable to `ordered_cancel_add_comm_monoid`,
 but it holds for measures with the additional assumption that μ is finite. -/
 lemma measure.le_of_add_le_add_left {μ ν₁ ν₂ : measure α} [finite_measure μ]

src/topology/continuous_function/bounded.lean

@@ -617,6 +617,15 @@ semimodule.of_core $
 instance : normed_space 𝕜 (α →ᵇ β) := ⟨λ c f, norm_of_normed_group_le _
   (mul_nonneg (norm_nonneg _) (norm_nonneg _)) _⟩
 
+variables (α β)
+
+/-- The linear map forgetting that a bounded continuous function is bounded. -/
+@[simps]
+def forget_boundedness_linear_map : (α →ᵇ β) →ₗ[𝕜] C(α, β) :=
+{ to_fun := forget_boundedness α β,
+  map_smul' := by { intros, ext, simp, },
+  map_add' := by { intros, ext, simp, }, }
+
 end normed_space
 
 section normed_ring