feat(measure_theory/conditional_expectation): define the Lp subspace …

…of functions measurable wrt a sigma-algebra, prove completeness (#7945)

This is the first step towards defining the conditional expectation:
- in this PR a subspace of L^p is shown to be complete, which is necessary to define an orthogonal projection on that subspace;
- the conditional expectation of functions in L^2 will be the orthogonal projection;
- the definition will be extended to L^1 through simple functions (as is done for the integral definition).

src/analysis/normed_space/linear_isometry.lean

@@ -205,6 +205,9 @@ def to_isometric : E ≃ᵢ F := ⟨e.to_linear_equiv.to_equiv, e.isometry⟩
 
 @[simp] lemma coe_to_isometric : ⇑e.to_isometric = e := rfl
 
+lemma range_eq_univ (e : E ≃ₗᵢ[R] F) : set.range e = set.univ :=
+by { rw ← coe_to_isometric, exact isometric.range_eq_univ _, }
+
 /-- Reinterpret a `linear_isometry_equiv` as an `homeomorph`. -/
 def to_homeomorph : E ≃ₜ F := e.to_isometric.to_homeomorph
 

src/measure_theory/arithmetic.lean

@@ -279,6 +279,16 @@ begin
   simp_rw [set.mem_set_of_eq, pi.sub_apply, sub_eq_zero],
 end
 
+lemma ae_eq_trim_of_measurable {α E} {m m0 : measurable_space α} {μ : measure α}
+  [measurable_space E] [add_group E] [measurable_singleton_class E] [has_measurable_sub₂ E]
+  (hm : m ≤ m0) {f g : α → E} (hf : @measurable _ _ m _ f) (hg : @measurable _ _ m _ g)
+  (hfg : f =ᵐ[μ] g) :
+  f =ᶠ[@measure.ae α m (μ.trim hm)] g :=
+begin
+  rwa [filter.eventually_eq, ae_iff, trim_measurable_set_eq hm _],
+  exact (@measurable_set.compl α _ m (@measurable_set_eq_fun α m E _ _ _ _ _ _ hf hg)),
+end
+
 end div
 
 /-- We say that a type `has_measurable_neg` if `x ↦ -x` is a measurable function. -/

src/measure_theory/conditional_expectation.lean

@@ -0,0 +1,265 @@
+/-
+Copyright (c) 2021 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+
+import measure_theory.lp_space
+
+/-! # Conditional expectation
+
+The conditional expectation will be defined for functions in `L²` by an orthogonal projection into
+a complete subspace of `L²`. It will then be extended to `L¹`.
+
+For now, this file contains only the definition of the subspace of `Lᵖ` containing functions which
+are measurable with respect to a sub-σ-algebra, as well as a proof that it is complete.
+
+-/
+
+noncomputable theory
+open topological_space measure_theory.Lp filter
+open_locale nnreal ennreal topological_space big_operators measure_theory
+
+namespace measure_theory
+
+/-- A function `f` verifies `ae_measurable' m f μ` if it is `μ`-a.e. equal to an `m`-measurable
+function. This is similar to `ae_measurable`, but the `measurable_space` structures used for the
+measurability statement and for the measure are different. -/
+def ae_measurable' {α β} [measurable_space β] (m : measurable_space α) {m0 : measurable_space α}
+  (f : α → β) (μ : measure α) : Prop :=
+∃ g : α → β, @measurable α β m _ g ∧ f =ᵐ[μ] g
+
+namespace ae_measurable'
+
+variables {α β 𝕜 : Type*} {m m0 : measurable_space α} {μ : measure α}
+  [measurable_space β] [measurable_space 𝕜] {f g : α → β}
+
+lemma congr (hf : ae_measurable' m f μ) (hfg : f =ᵐ[μ] g) : ae_measurable' m g μ :=
+by { obtain ⟨f', hf'_meas, hff'⟩ := hf, exact ⟨f', hf'_meas, hfg.symm.trans hff'⟩, }
+
+lemma add [has_add β] [has_measurable_add₂ β] (hf : ae_measurable' m f μ)
+  (hg : ae_measurable' m g μ) :
+  ae_measurable' m (f+g) μ :=
+begin
+  rcases hf with ⟨f', h_f'_meas, hff'⟩,
+  rcases hg with ⟨g', h_g'_meas, hgg'⟩,
+  exact ⟨f' + g', @measurable.add α m _ _ _ _ f' g' h_f'_meas h_g'_meas, hff'.add hgg'⟩,
+end
+
+lemma const_smul [has_scalar 𝕜 β] [has_measurable_smul 𝕜 β] (c : 𝕜) (hf : ae_measurable' m f μ) :
+  ae_measurable' m (c • f) μ :=
+begin
+  rcases hf with ⟨f', h_f'_meas, hff'⟩,
+  refine ⟨c • f', @measurable.const_smul α m _ _ _ _ _ _ f' h_f'_meas c, _⟩,
+  exact eventually_eq.fun_comp hff' (λ x, c • x),
+end
+
+end ae_measurable'
+
+lemma ae_measurable'_of_ae_measurable'_trim {α β} {m m0 m0' : measurable_space α}
+  [measurable_space β] (hm0 : m0 ≤ m0') {μ : measure α} {f : α → β}
+  (hf : ae_measurable' m f (μ.trim hm0)) :
+  ae_measurable' m f μ :=
+by { obtain ⟨g, hg_meas, hfg⟩ := hf, exact ⟨g, hg_meas, ae_eq_of_ae_eq_trim hfg⟩, }
+
+variables {α β γ E E' F F' G G' H 𝕜 : Type*} {p : ℝ≥0∞}
+  [is_R_or_C 𝕜] [measurable_space 𝕜] -- 𝕜 for ℝ or ℂ, together with a measurable_space
+  [measurable_space β] -- β for a generic measurable space
+  -- E and E' will be used for inner product spaces, when they are needed.
+  -- F for a Lp submodule
+  [normed_group F] [normed_space 𝕜 F] [measurable_space F] [borel_space F]
+  [second_countable_topology F]
+  -- F' for integrals on a Lp submodule
+  [normed_group F'] [normed_space 𝕜 F'] [measurable_space F'] [borel_space F']
+  [second_countable_topology F'] [normed_space ℝ F'] [complete_space F']
+  -- G for a Lp add_subgroup
+  [normed_group G] [measurable_space G] [borel_space G] [second_countable_topology G]
+  -- G' for integrals on a Lp add_subgroup
+  [normed_group G'] [measurable_space G'] [borel_space G'] [second_countable_topology G']
+  [normed_space ℝ G'] [complete_space G']
+  -- H for measurable space and normed group (hypotheses of mem_ℒp)
+  [measurable_space H] [normed_group H]
+
+section Lp_meas
+
+variables (F 𝕜)
+/-- `Lp_meas F 𝕜 m p μ` is the subspace of `Lp F p μ` containing functions `f` verifying
+`ae_measurable' m f μ`, i.e. functions which are `μ`-a.e. equal to an `m`-measurable function. -/
+def Lp_meas [opens_measurable_space 𝕜] (m : measurable_space α) [measurable_space α] (p : ℝ≥0∞)
+  (μ : measure α) :
+  submodule 𝕜 (Lp F p μ) :=
+{ carrier   := {f : (Lp F p μ) | ae_measurable' m f μ} ,
+  zero_mem' := ⟨(0 : α → F), @measurable_zero _ α _ m _, Lp.coe_fn_zero _ _ _⟩,
+  add_mem'  := λ f g hf hg, (hf.add hg).congr (Lp.coe_fn_add f g).symm,
+  smul_mem' := λ c f hf, (hf.const_smul c).congr (Lp.coe_fn_smul c f).symm, }
+variables {F 𝕜}
+
+variables [opens_measurable_space 𝕜]
+
+lemma mem_Lp_meas_iff_ae_measurable' {m m0 : measurable_space α} {μ : measure α} {f : Lp F p μ} :
+  f ∈ Lp_meas F 𝕜 m p μ ↔ ae_measurable' m f μ :=
+by simp_rw [← set_like.mem_coe, ← submodule.mem_carrier, Lp_meas, set.mem_set_of_eq]
+
+lemma Lp_meas.ae_measurable' {m m0 : measurable_space α} {μ : measure α} (f : Lp_meas F 𝕜 m p μ) :
+  ae_measurable' m f μ :=
+mem_Lp_meas_iff_ae_measurable'.mp f.mem
+
+lemma mem_Lp_meas_self {m0 : measurable_space α} (μ : measure α) (f : Lp F p μ) :
+  f ∈ Lp_meas F 𝕜 m0 p μ :=
+mem_Lp_meas_iff_ae_measurable'.mpr (Lp.ae_measurable f)
+
+lemma Lp_meas_coe {m m0 : measurable_space α} {μ : measure α} {f : Lp_meas F 𝕜 m p μ} :
+  ⇑f = (f : Lp F p μ) :=
+coe_fn_coe_base f
+
+section complete_subspace
+
+/-! ## The subspace `Lp_meas` is complete.
+
+We define a `linear_isometry_equiv` between `Lp_meas` and the `Lp` space corresponding to the
+measure `μ.trim hm`. As a consequence, the completeness of `Lp` implies completeness of
+`Lp_meas`. -/
+
+variables {ι : Type*} {m m0 : measurable_space α} {μ : measure α}
+
+/-- If `f` belongs to `Lp_meas F 𝕜 m p μ`, then the measurable function it is almost everywhere
+equal to (given by `ae_measurable.mk`) belongs to `ℒp` for the measure `μ.trim hm`. -/
+lemma mem_ℒp_trim_of_mem_Lp_meas (hm : m ≤ m0) (f : Lp F p μ) (hf_meas : f ∈ Lp_meas F 𝕜 m p μ) :
+  @mem_ℒp α F m _ _ (mem_Lp_meas_iff_ae_measurable'.mp hf_meas).some p (μ.trim hm) :=
+begin
+  have hf : ae_measurable' m f μ, from (mem_Lp_meas_iff_ae_measurable'.mp hf_meas),
+  let g := hf.some,
+  obtain ⟨hg, hfg⟩ := hf.some_spec,
+  change @mem_ℒp α F m _ _ g p (μ.trim hm),
+  refine ⟨@measurable.ae_measurable _ _ m _ g (μ.trim hm) hg, _⟩,
+  have h_snorm_fg : @snorm α _ m _ g p (μ.trim hm) = snorm f p μ,
+    by { rw snorm_trim hm hg, exact snorm_congr_ae hfg.symm, },
+  rw h_snorm_fg,
+  exact Lp.snorm_lt_top f,
+end
+
+/-- If `f` belongs to `Lp` for the measure `μ.trim hm`, then it belongs to the subspace
+`Lp_meas F 𝕜 m p μ`. -/
+lemma mem_Lp_meas_to_Lp_of_trim (hm : m ≤ m0) (f : @Lp α F m _ _ _ _ p (μ.trim hm)) :
+  (mem_ℒp_of_mem_ℒp_trim hm (@Lp.mem_ℒp _ _ m _ _ _ _ _ _ f)).to_Lp f ∈ Lp_meas F 𝕜 m p μ :=
+begin
+  let hf_mem_ℒp := mem_ℒp_of_mem_ℒp_trim hm (@Lp.mem_ℒp _ _ m _ _ _ _ _ _ f),
+  rw mem_Lp_meas_iff_ae_measurable',
+  refine ae_measurable'.congr _ (mem_ℒp.coe_fn_to_Lp hf_mem_ℒp).symm,
+  refine ae_measurable'_of_ae_measurable'_trim hm _,
+  exact (@Lp.ae_measurable _ _ m _ _ _ _ _ _ f),
+end
+
+variables (F 𝕜 p μ)
+/-- Map from `Lp_meas` to `Lp F p (μ.trim hm)`. -/
+def Lp_meas_to_Lp_trim (hm : m ≤ m0) (f : Lp_meas F 𝕜 m p μ) : @Lp α F m _ _ _ _ p (μ.trim hm) :=
+@mem_ℒp.to_Lp _ _ m p (μ.trim hm) _ _ _ _ (mem_Lp_meas_iff_ae_measurable'.mp f.mem).some
+  (mem_ℒp_trim_of_mem_Lp_meas hm f f.mem)
+
+/-- Map from `Lp F p (μ.trim hm)` to `Lp_meas`, inverse of `Lp_meas_to_Lp_trim`. -/
+def Lp_trim_to_Lp_meas (hm : m ≤ m0) (f : @Lp α F m _ _ _ _ p (μ.trim hm)) :
+  Lp_meas F 𝕜 m p μ :=
+⟨(mem_ℒp_of_mem_ℒp_trim hm (@Lp.mem_ℒp _ _ m _ _ _ _ _ _ f)).to_Lp f,
+  mem_Lp_meas_to_Lp_of_trim hm f⟩
+
+variables {F 𝕜 p μ}
+
+lemma Lp_meas_to_Lp_trim_ae_eq (hm : m ≤ m0) (f : Lp_meas F 𝕜 m p μ) :
+  Lp_meas_to_Lp_trim F 𝕜 p μ hm f =ᵐ[μ] f :=
+(ae_eq_of_ae_eq_trim
+    (@mem_ℒp.coe_fn_to_Lp _ _ m _ _ _ _ _ _ _ (mem_ℒp_trim_of_mem_Lp_meas hm ↑f f.mem))).trans
+  (mem_Lp_meas_iff_ae_measurable'.mp f.mem).some_spec.2.symm
+
+lemma Lp_trim_to_Lp_meas_ae_eq (hm : m ≤ m0) (f : @Lp α F m _ _ _ _ p (μ.trim hm)) :
+  Lp_trim_to_Lp_meas F 𝕜 p μ hm f =ᵐ[μ] f :=
+mem_ℒp.coe_fn_to_Lp _
+
+/-- `Lp_trim_to_Lp_meas` is a right inverse of `Lp_meas_to_Lp_trim`. -/
+lemma Lp_meas_to_Lp_trim_right_inv (hm : m ≤ m0) :
+  function.right_inverse (Lp_trim_to_Lp_meas F 𝕜 p μ hm) (Lp_meas_to_Lp_trim F 𝕜 p μ hm) :=
+begin
+  intro f,
+  ext1,
+  refine ae_eq_trim_of_measurable hm _ _ _,
+  { exact @Lp.measurable _ _ m _ _ _ _ _ _ _, },
+  { exact @Lp.measurable _ _ m _ _ _ _ _ _ _, },
+  { exact (Lp_meas_to_Lp_trim_ae_eq hm _).trans (Lp_trim_to_Lp_meas_ae_eq hm _), },
+end
+
+/-- `Lp_trim_to_Lp_meas` is a left inverse of `Lp_meas_to_Lp_trim`. -/
+lemma Lp_meas_to_Lp_trim_left_inv (hm : m ≤ m0) :
+  function.left_inverse (Lp_trim_to_Lp_meas F 𝕜 p μ hm) (Lp_meas_to_Lp_trim F 𝕜 p μ hm) :=
+begin
+  intro f,
+  ext1,
+  ext1,
+  rw ← Lp_meas_coe,
+  exact (Lp_trim_to_Lp_meas_ae_eq hm _).trans (Lp_meas_to_Lp_trim_ae_eq hm _),
+end
+
+lemma Lp_meas_to_Lp_trim_add (hm : m ≤ m0) (f g : Lp_meas F 𝕜 m p μ) :
+  Lp_meas_to_Lp_trim F 𝕜 p μ hm (f + g)
+    = Lp_meas_to_Lp_trim F 𝕜 p μ hm f + Lp_meas_to_Lp_trim F 𝕜 p μ hm g :=
+begin
+  ext1,
+  refine eventually_eq.trans _ (@Lp.coe_fn_add _ _ m _ _ _ _ _ _ _ _).symm,
+  refine ae_eq_trim_of_measurable hm _ _ _,
+  { exact @Lp.measurable _ _ m _ _ _ _ _ _ _, },
+  { exact @measurable.add _ m _ _ _ _ _ _ (@Lp.measurable _ _ m _ _ _ _ _ _ _)
+      (@Lp.measurable _ _ m _ _ _ _ _ _ _), },
+  refine (Lp_meas_to_Lp_trim_ae_eq hm _).trans _,
+  refine eventually_eq.trans _
+    (eventually_eq.add (Lp_meas_to_Lp_trim_ae_eq hm f).symm (Lp_meas_to_Lp_trim_ae_eq hm g).symm),
+  refine (Lp.coe_fn_add _ _).trans _,
+  simp_rw Lp_meas_coe,
+  refine eventually_of_forall (λ x, _),
+  refl,
+end
+
+lemma Lp_meas_to_Lp_trim_smul (hm : m ≤ m0) (c : 𝕜) (f : Lp_meas F 𝕜 m p μ) :
+  Lp_meas_to_Lp_trim F 𝕜 p μ hm (c • f) = c • Lp_meas_to_Lp_trim F 𝕜 p μ hm f :=
+begin
+  ext1,
+  refine eventually_eq.trans _ (@Lp.coe_fn_smul _ _ m _ _ _ _ _ _ _ _ _ _ _ _ _).symm,
+  refine ae_eq_trim_of_measurable hm _ _ _,
+  { exact @Lp.measurable _ _ m _ _ _ _ _ _ _, },
+  { exact @measurable.const_smul _ m _ _ _ _ _ _ _ (@Lp.measurable _ _ m _ _ _ _ _ _ _) c, },
+  refine (Lp_meas_to_Lp_trim_ae_eq hm _).trans _,
+  refine (Lp.coe_fn_smul c _).trans _,
+  refine (Lp_meas_to_Lp_trim_ae_eq hm f).mono (λ x hx, _),
+  rw [pi.smul_apply, pi.smul_apply, hx, Lp_meas_coe],
+  refl,
+end
+
+/-- `Lp_meas_to_Lp_trim` preserves the norm. -/
+lemma Lp_meas_to_Lp_trim_norm_map [hp : fact (1 ≤ p)] (hm : m ≤ m0) (f : Lp_meas F 𝕜 m p μ) :
+  ∥Lp_meas_to_Lp_trim F 𝕜 p μ hm f∥ = ∥f∥ :=
+begin
+  rw [norm_def, snorm_trim hm (@Lp.measurable _ _ m _ _ _ _ _ _ _)],
+  swap, { apply_instance, },
+  rw [snorm_congr_ae (Lp_meas_to_Lp_trim_ae_eq hm _), Lp_meas_coe, ← norm_def],
+  congr,
+end
+
+variables (F 𝕜 p μ)
+/-- A linear isometry equivalence between `Lp_meas` and `Lp F p (μ.trim hm)`. -/
+def Lp_meas_to_Lp_trim_lie [hp : fact (1 ≤ p)] (hm : m ≤ m0) :
+  Lp_meas F 𝕜 m p μ ≃ₗᵢ[𝕜] @Lp α F m _ _ _ _ p (μ.trim hm) :=
+{ to_fun    := Lp_meas_to_Lp_trim F 𝕜 p μ hm,
+  map_add'  := Lp_meas_to_Lp_trim_add hm,
+  map_smul' := Lp_meas_to_Lp_trim_smul hm,
+  inv_fun   := Lp_trim_to_Lp_meas F 𝕜 p μ hm,
+  left_inv  := Lp_meas_to_Lp_trim_left_inv hm,
+  right_inv := Lp_meas_to_Lp_trim_right_inv hm,
+  norm_map' := Lp_meas_to_Lp_trim_norm_map hm, }
+variables {F 𝕜 p μ}
+
+instance [hm : fact (m ≤ m0)] [complete_space F] [hp : fact (1 ≤ p)] :
+  complete_space (Lp_meas F 𝕜 m p μ) :=
+by { rw (Lp_meas_to_Lp_trim_lie F 𝕜 p μ hm.elim).to_isometric.complete_space_iff, apply_instance, }
+
+end complete_subspace
+
+end Lp_meas
+
+end measure_theory

src/measure_theory/lp_space.lean

@@ -545,46 +545,43 @@ end
 
 section trim
 
-lemma snorm'_trim {α : Type*} {m m0 : measurable_space α} {μ : measure α} (hm : m ≤ m0) {f : α → E}
-  (hf : @measurable _ _ m _ f) :
-  @snorm' α E m _ f q (μ.trim hm) = snorm' f q μ :=
+variables {β : Type*} {m m0 : measurable_space β} {ν : measure β}
+
+lemma snorm'_trim (hm : m ≤ m0) {f : β → E} (hf : @measurable _ _ m _ f) :
+  @snorm' β E m _ f q (ν.trim hm) = snorm' f q ν :=
 begin
   simp_rw snorm',
   congr' 1,
   refine lintegral_trim hm _,
-  refine @measurable.pow_const α m _ _ _ _ _ _ _ (@measurable.coe_nnreal_ennreal α m _ _) _,
-  exact @measurable.nnnorm E α _ _ _ m _ hf,
+  refine @measurable.pow_const _ m _ _ _ _ _ _ _ (@measurable.coe_nnreal_ennreal _ m _ _) _,
+  exact @measurable.nnnorm E _ _ _ _ m _ hf,
 end
 
-lemma limsup_trim {α : Type*} {m m0 : measurable_space α} {μ : measure α} (hm : m ≤ m0)
-  {f : α → ℝ≥0∞} (hf : @measurable _ _ m _ f) :
-  (@measure.ae α m (μ.trim hm)).limsup f = μ.ae.limsup f :=
+lemma limsup_trim (hm : m ≤ m0) {f : β → ℝ≥0∞} (hf : @measurable _ _ m _ f) :
+  (@measure.ae _ m (ν.trim hm)).limsup f = ν.ae.limsup f :=
 begin
   simp_rw limsup_eq,
-  suffices h_set_eq : {a : ℝ≥0∞ | filter.eventually (λ n, f n ≤ a) (@measure.ae α m (μ.trim hm))}
-      = {a : ℝ≥0∞ | ∀ᵐ (n : α) ∂μ, f n ≤ a},
+  suffices h_set_eq : {a : ℝ≥0∞ | filter.eventually (λ n, f n ≤ a) (@measure.ae _ m (ν.trim hm))}
+      = {a : ℝ≥0∞ | ∀ᵐ n ∂ν, f n ≤ a},
     by rw h_set_eq,
   ext1 a,
-  suffices h_meas_eq : μ {x | ¬ f x ≤ a} = μ.trim hm {x | ¬ f x ≤ a},
+  suffices h_meas_eq : ν {x | ¬ f x ≤ a} = ν.trim hm {x | ¬ f x ≤ a},
     by simp_rw [set.mem_set_of_eq, ae_iff, h_meas_eq],
   refine (trim_measurable_set_eq hm _).symm,
-  refine @measurable_set.compl α _ m (@measurable_set_le ℝ≥0∞ α _ _ _ m _ _ _ _ _ hf _),
-  exact @measurable_const _ α _ m _,
+  refine @measurable_set.compl _ _ m (@measurable_set_le ℝ≥0∞ _ _ _ _ m _ _ _ _ _ hf _),
+  exact @measurable_const _ _ _ m _,
 end
 
-lemma ess_sup_trim {α : Type*} {m m0 : measurable_space α} {μ : measure α} (hm : m ≤ m0)
-  {f : α → ℝ≥0∞} (hf : @measurable _ _ m _ f) :
-  @ess_sup α _ m _ f (μ.trim hm) = ess_sup f μ :=
+lemma ess_sup_trim (hm : m ≤ m0) {f : β → ℝ≥0∞} (hf : @measurable _ _ m _ f) :
+  @ess_sup _ _ m _ f (ν.trim hm) = ess_sup f ν :=
 by { simp_rw ess_sup, exact limsup_trim hm hf, }
 
-lemma snorm_ess_sup_trim {α : Type*} {m m0 : measurable_space α} {μ : measure α} (hm : m ≤ m0)
-  {f : α → E} (hf : @measurable _ _ m _ f) :
-  @snorm_ess_sup α E m _ f (μ.trim hm) = snorm_ess_sup f μ :=
-ess_sup_trim hm (@measurable.coe_nnreal_ennreal α m _ (@measurable.nnnorm E α _ _ _ m _ hf))
+lemma snorm_ess_sup_trim (hm : m ≤ m0) {f : β → E} (hf : @measurable _ _ m _ f) :
+  @snorm_ess_sup _ E m _ f (ν.trim hm) = snorm_ess_sup f ν :=
+ess_sup_trim hm (@measurable.coe_nnreal_ennreal _ m _ (@measurable.nnnorm E _ _ _ _ m _ hf))
 
-lemma snorm_trim {α : Type*} {m m0 : measurable_space α} {μ : measure α} (hm : m ≤ m0) {f : α → E}
-  (hf : @measurable _ _ m _ f) :
-  @snorm α E m _ f p (μ.trim hm) = snorm f p μ :=
+lemma snorm_trim (hm : m ≤ m0) {f : β → E} (hf : @measurable _ _ m _ f) :
+  @snorm _ E m _ f p (ν.trim hm) = snorm f p ν :=
 begin
   by_cases h0 : p = 0,
   { simp [h0], },
@@ -593,6 +590,21 @@ begin
   simpa only [snorm_eq_snorm' h0 h_top] using snorm'_trim hm hf,
 end
 
+lemma snorm_trim_ae (hm : m ≤ m0) {f : β → E} (hf : @ae_measurable _ _ m _ f (ν.trim hm)) :
+  @snorm _ E m _ f p (ν.trim hm) = snorm f p ν :=
+begin
+  let g := @ae_measurable.mk _ _ m _ _ _ hf,
+  have hg_meas : @measurable _ _ m _ g, from @ae_measurable.measurable_mk _ _ m _ _ _ hf,
+  have hfg := @ae_measurable.ae_eq_mk _ _ m _ _ _ hf,
+  rw @snorm_congr_ae _ _ m _ _ _ _ _ hfg,
+  rw snorm_congr_ae (ae_eq_of_ae_eq_trim hfg),
+  exact snorm_trim hm hg_meas,
+end
+
+lemma mem_ℒp_of_mem_ℒp_trim (hm : m ≤ m0) {f : β → E} (hf : @mem_ℒp _ E m _ _ f p (ν.trim hm)) :
+  mem_ℒp f p ν :=
+⟨ae_measurable_of_ae_measurable_trim hm hf.1, (le_of_eq (snorm_trim_ae hm hf.1).symm).trans_lt hf.2⟩
+
 end trim
 
 end opens_measurable_space

src/topology/metric_space/isometry.lean

@@ -290,6 +290,13 @@ lemma mul_apply (e₁ e₂ : α ≃ᵢ α) (x : α) : (e₁ * e₂) x = e₁ (e
 
 @[simp] lemma apply_inv_self (e : α ≃ᵢ α) (x: α) : e (e⁻¹ x) = x := e.apply_symm_apply x
 
+protected lemma complete_space (e : α ≃ᵢ β) (hF : complete_space β) : complete_space α :=
+complete_space_of_is_complete_univ $ is_complete_of_complete_image e.isometry.uniform_inducing $
+  by rwa [set.image_univ, isometric.range_eq_univ, ← complete_space_iff_is_complete_univ]
+
+lemma complete_space_iff (e : α ≃ᵢ β) : complete_space α ↔ complete_space β :=
+⟨λ h, e.symm.complete_space h, λ h, e.complete_space h⟩
+
 end pseudo_emetric_space
 
 section pseudo_metric_space