Documentation

Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable

Functions a.e. measurable with respect to a sub-σ-algebra #

A function f verifies AEStronglyMeasurable' m f μ if it is μ-a.e. equal to an m-strongly measurable function. This is similar to AEStronglyMeasurable, but the MeasurableSpace structures used for the measurability statement and for the measure are different.

We define lpMeas F 𝕜 m p μ, the subspace of Lp F p μ containing functions f verifying AEStronglyMeasurable' m f μ, i.e. functions which are μ-a.e. equal to an m-strongly measurable function.

Main statements #

We define an IsometryEquiv between lpMeasSubgroup and the Lp space corresponding to the measure μ.trim hm. As a consequence, the completeness of Lp implies completeness of lpMeas.

Lp.induction_stronglyMeasurable (see also Memℒp.induction_stronglyMeasurable): To prove something for an Lp function a.e. strongly measurable with respect to a sub-σ-algebra m in a normed space, it suffices to show that

def MeasureTheory.AEStronglyMeasurable' {α : Type u_1} {β : Type u_2} [TopologicalSpace β] (m : MeasurableSpace α) :
{x : MeasurableSpace α} → (αβ)MeasureTheory.Measure αProp

A function f verifies AEStronglyMeasurable' m f μ if it is μ-a.e. equal to an m-strongly measurable function. This is similar to AEStronglyMeasurable, but the MeasurableSpace structures used for the measurability statement and for the measure are different.

Equations
Instances For
    theorem MeasureTheory.AEStronglyMeasurable'.congr {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : αβ} {g : αβ} (hf : MeasureTheory.AEStronglyMeasurable' m f μ) (hfg : f =ᵐ[μ] g) :
    theorem MeasureTheory.AEStronglyMeasurable'.const_smul {α : Type u_1} {β : Type u_2} {𝕜 : Type u_3} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : αβ} [SMul 𝕜 β] [ContinuousConstSMul 𝕜 β] (c : 𝕜) (hf : MeasureTheory.AEStronglyMeasurable' m f μ) :
    theorem MeasureTheory.AEStronglyMeasurable'.const_inner {α : Type u_1} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_4} {β : Type u_5} [RCLike 𝕜] [NormedAddCommGroup β] [InnerProductSpace 𝕜 β] {f : αβ} (hfm : MeasureTheory.AEStronglyMeasurable' m f μ) (c : β) :
    MeasureTheory.AEStronglyMeasurable' m (fun (x : α) => c, f x⟫_𝕜) μ
    noncomputable def MeasureTheory.AEStronglyMeasurable'.mk {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] (f : αβ) (hfm : MeasureTheory.AEStronglyMeasurable' m f μ) :
    αβ

    An m-strongly measurable function almost everywhere equal to f.

    Equations
    Instances For
      theorem MeasureTheory.AEStronglyMeasurable'.continuous_comp {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {γ : Type u_4} [TopologicalSpace γ] {f : αβ} {g : βγ} (hg : Continuous g) (hf : MeasureTheory.AEStronglyMeasurable' m f μ) :
      theorem MeasureTheory.AEStronglyMeasurable'.aeStronglyMeasurable'_of_measurableSpace_le_on {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {m₂ : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace E] [Zero E] (hm : m m0) {s : Set α} {f : αE} (hs_m : MeasurableSet s) (hs : ∀ (t : Set α), MeasurableSet (s t)MeasurableSet (s t)) (hf : MeasureTheory.AEStronglyMeasurable' m f μ) (hf_zero : f =ᵐ[μ.restrict s] 0) :

      If the restriction to a set s of a σ-algebra m is included in the restriction to s of another σ-algebra m₂ (hypothesis hs), the set s is m measurable and a function f almost everywhere supported on s is m-ae-strongly-measurable, then f is also m₂-ae-strongly-measurable.

      The subset lpMeas of Lp functions a.e. measurable with respect to a sub-sigma-algebra #

      lpMeasSubgroup F m p μ is the subspace of Lp F p μ containing functions f verifying AEStronglyMeasurable' m f μ, i.e. functions which are μ-a.e. equal to an m-strongly measurable function.

      Equations
      Instances For
        def MeasureTheory.lpMeas {α : Type u_1} (F : Type u_3) (𝕜 : Type u_5) [RCLike 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (m : MeasurableSpace α) [MeasurableSpace α] (p : ENNReal) (μ : MeasureTheory.Measure α) :
        Submodule 𝕜 (MeasureTheory.Lp F p μ)

        lpMeas F 𝕜 m p μ is the subspace of Lp F p μ containing functions f verifying AEStronglyMeasurable' m f μ, i.e. functions which are μ-a.e. equal to an m-strongly measurable function.

        Equations
        Instances For
          theorem MeasureTheory.mem_lpMeas_iff_aeStronglyMeasurable' {α : Type u_1} {F : Type u_3} {𝕜 : Type u_5} {p : ENNReal} [RCLike 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : (MeasureTheory.Lp F p μ)} :
          theorem MeasureTheory.lpMeas.aeStronglyMeasurable' {α : Type u_1} {F : Type u_3} {𝕜 : Type u_5} {p : ENNReal} [RCLike 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {m : MeasurableSpace α} :
          ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : (MeasureTheory.lpMeas F 𝕜 m p μ)), MeasureTheory.AEStronglyMeasurable' m (f) μ
          theorem MeasureTheory.mem_lpMeas_self {α : Type u_1} {F : Type u_3} {𝕜 : Type u_5} {p : ENNReal} [RCLike 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : (MeasureTheory.Lp F p μ)) :
          f MeasureTheory.lpMeas F 𝕜 m0 p μ
          theorem MeasureTheory.lpMeasSubgroup_coe {α : Type u_1} {F : Type u_3} {p : ENNReal} [NormedAddCommGroup F] {m : MeasurableSpace α} :
          ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : (MeasureTheory.lpMeasSubgroup F m p μ)}, f = f
          theorem MeasureTheory.lpMeas_coe {α : Type u_1} {F : Type u_3} {𝕜 : Type u_5} {p : ENNReal} [RCLike 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {m : MeasurableSpace α} :
          ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : (MeasureTheory.lpMeas F 𝕜 m p μ)}, f = f
          theorem MeasureTheory.mem_lpMeas_indicatorConstLp {α : Type u_1} {F : Type u_3} {𝕜 : Type u_5} {p : ENNReal} [RCLike 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {m : MeasurableSpace α} {m0 : MeasurableSpace α} (hm : m m0) {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) (hμs : μ s ) {c : F} :

          The subspace lpMeas is complete. #

          We define an IsometryEquiv between lpMeasSubgroup and the Lp space corresponding to the measure μ.trim hm. As a consequence, the completeness of Lp implies completeness of lpMeasSubgroup (and lpMeas).

          theorem MeasureTheory.memℒp_trim_of_mem_lpMeasSubgroup {α : Type u_1} {F : Type u_3} {p : ENNReal} [NormedAddCommGroup F] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m m0) (f : (MeasureTheory.Lp F p μ)) (hf_meas : f MeasureTheory.lpMeasSubgroup F m p μ) :

          If f belongs to lpMeasSubgroup F m p μ, then the measurable function it is almost everywhere equal to (given by AEMeasurable.mk) belongs to ℒp for the measure μ.trim hm.

          theorem MeasureTheory.mem_lpMeasSubgroup_toLp_of_trim {α : Type u_1} {F : Type u_3} {p : ENNReal} [NormedAddCommGroup F] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m m0) (f : (MeasureTheory.Lp F p (μ.trim hm))) :

          If f belongs to Lp for the measure μ.trim hm, then it belongs to the subgroup lpMeasSubgroup F m p μ.

          noncomputable def MeasureTheory.lpMeasSubgroupToLpTrim {α : Type u_1} (F : Type u_3) (p : ENNReal) [NormedAddCommGroup F] {m : MeasurableSpace α} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (hm : m m0) (f : (MeasureTheory.lpMeasSubgroup F m p μ)) :
          (MeasureTheory.Lp F p (μ.trim hm))

          Map from lpMeasSubgroup to Lp F p (μ.trim hm).

          Equations
          Instances For
            noncomputable def MeasureTheory.lpMeasToLpTrim {α : Type u_1} (F : Type u_3) (𝕜 : Type u_5) (p : ENNReal) [RCLike 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {m : MeasurableSpace α} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (hm : m m0) (f : (MeasureTheory.lpMeas F 𝕜 m p μ)) :
            (MeasureTheory.Lp F p (μ.trim hm))

            Map from lpMeas to Lp F p (μ.trim hm).

            Equations
            Instances For
              noncomputable def MeasureTheory.lpTrimToLpMeasSubgroup {α : Type u_1} (F : Type u_3) (p : ENNReal) [NormedAddCommGroup F] {m : MeasurableSpace α} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (hm : m m0) (f : (MeasureTheory.Lp F p (μ.trim hm))) :

              Map from Lp F p (μ.trim hm) to lpMeasSubgroup, inverse of lpMeasSubgroupToLpTrim.

              Equations
              Instances For
                noncomputable def MeasureTheory.lpTrimToLpMeas {α : Type u_1} (F : Type u_3) (𝕜 : Type u_5) (p : ENNReal) [RCLike 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {m : MeasurableSpace α} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (hm : m m0) (f : (MeasureTheory.Lp F p (μ.trim hm))) :
                (MeasureTheory.lpMeas F 𝕜 m p μ)

                Map from Lp F p (μ.trim hm) to lpMeas, inverse of Lp_meas_to_Lp_trim.

                Equations
                Instances For
                  theorem MeasureTheory.lpMeasSubgroupToLpTrim_ae_eq {α : Type u_1} {F : Type u_3} {p : ENNReal} [NormedAddCommGroup F] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m m0) (f : (MeasureTheory.lpMeasSubgroup F m p μ)) :
                  (MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm f) =ᵐ[μ] f
                  theorem MeasureTheory.lpTrimToLpMeasSubgroup_ae_eq {α : Type u_1} {F : Type u_3} {p : ENNReal} [NormedAddCommGroup F] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m m0) (f : (MeasureTheory.Lp F p (μ.trim hm))) :
                  (MeasureTheory.lpTrimToLpMeasSubgroup F p μ hm f) =ᵐ[μ] f
                  theorem MeasureTheory.lpMeasToLpTrim_ae_eq {α : Type u_1} {F : Type u_3} {𝕜 : Type u_5} {p : ENNReal} [RCLike 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m m0) (f : (MeasureTheory.lpMeas F 𝕜 m p μ)) :
                  (MeasureTheory.lpMeasToLpTrim F 𝕜 p μ hm f) =ᵐ[μ] f
                  theorem MeasureTheory.lpTrimToLpMeas_ae_eq {α : Type u_1} {F : Type u_3} {𝕜 : Type u_5} {p : ENNReal} [RCLike 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m m0) (f : (MeasureTheory.Lp F p (μ.trim hm))) :
                  (MeasureTheory.lpTrimToLpMeas F 𝕜 p μ hm f) =ᵐ[μ] f
                  theorem MeasureTheory.lpMeasToLpTrim_smul {α : Type u_1} {F : Type u_3} {𝕜 : Type u_5} {p : ENNReal} [RCLike 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m m0) (c : 𝕜) (f : (MeasureTheory.lpMeas F 𝕜 m p μ)) :
                  MeasureTheory.lpMeasToLpTrim F 𝕜 p μ hm (c f) = c MeasureTheory.lpMeasToLpTrim F 𝕜 p μ hm f
                  noncomputable def MeasureTheory.lpMeasSubgroupToLpTrimIso {α : Type u_1} (F : Type u_3) (p : ENNReal) [NormedAddCommGroup F] {m : MeasurableSpace α} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [Fact (1 p)] (hm : m m0) :
                  (MeasureTheory.lpMeasSubgroup F m p μ) ≃ᵢ (MeasureTheory.Lp F p (μ.trim hm))

                  lpMeasSubgroup and Lp F p (μ.trim hm) are isometric.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    noncomputable def MeasureTheory.lpMeasSubgroupToLpMeasIso {α : Type u_1} (F : Type u_3) (𝕜 : Type u_5) (p : ENNReal) [RCLike 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {m : MeasurableSpace α} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [Fact (1 p)] :

                    lpMeasSubgroup and lpMeas are isometric.

                    Equations
                    Instances For
                      noncomputable def MeasureTheory.lpMeasToLpTrimLie {α : Type u_1} (F : Type u_3) (𝕜 : Type u_5) (p : ENNReal) [RCLike 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {m : MeasurableSpace α} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [Fact (1 p)] (hm : m m0) :
                      (MeasureTheory.lpMeas F 𝕜 m p μ) ≃ₗᵢ[𝕜] (MeasureTheory.Lp F p (μ.trim hm))

                      lpMeas and Lp F p (μ.trim hm) are isometric, with a linear equivalence.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        Equations
                        • =
                        theorem MeasureTheory.isComplete_aeStronglyMeasurable' {α : Type u_1} {F : Type u_3} {p : ENNReal} [NormedAddCommGroup F] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [hp : Fact (1 p)] [CompleteSpace F] (hm : m m0) :
                        theorem MeasureTheory.lpMeas.ae_fin_strongly_measurable' {α : Type u_1} {F : Type u_3} {𝕜 : Type u_5} {p : ENNReal} [RCLike 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m m0) (f : (MeasureTheory.lpMeas F 𝕜 m p μ)) (hp_ne_zero : p 0) (hp_ne_top : p ) :
                        ∃ (g : αF), MeasureTheory.FinStronglyMeasurable g (μ.trim hm) f =ᵐ[μ] g

                        We do not get ae_fin_strongly_measurable f (μ.trim hm), since we don't have f =ᵐ[μ.trim hm] Lp_meas_to_Lp_trim F 𝕜 p μ hm f but only the weaker f =ᵐ[μ] Lp_meas_to_Lp_trim F 𝕜 p μ hm f.

                        theorem MeasureTheory.lpMeasToLpTrimLie_symm_indicator {α : Type u_1} {F : Type u_3} {p : ENNReal} [NormedAddCommGroup F] {m : MeasurableSpace α} {m0 : MeasurableSpace α} [one_le_p : Fact (1 p)] [NormedSpace F] {hm : m m0} {s : Set α} {μ : MeasureTheory.Measure α} (hs : MeasurableSet s) (hμs : (μ.trim hm) s ) (c : F) :

                        When applying the inverse of lpMeasToLpTrimLie (which takes a function in the Lp space of the sub-sigma algebra and returns its version in the larger Lp space) to an indicator of the sub-sigma-algebra, we obtain an indicator in the Lp space of the larger sigma-algebra.

                        theorem MeasureTheory.lpMeasToLpTrimLie_symm_toLp {α : Type u_1} {F : Type u_3} {p : ENNReal} [NormedAddCommGroup F] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [one_le_p : Fact (1 p)] [NormedSpace F] (hm : m m0) (f : αF) (hf : MeasureTheory.Memℒp f p (μ.trim hm)) :
                        theorem MeasureTheory.Lp.induction_stronglyMeasurable_aux {α : Type u_1} {F : Type u_3} {p : ENNReal} [NormedAddCommGroup F] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Fact (1 p)] [NormedSpace F] (hm : m m0) (hp_ne_top : p ) (P : (MeasureTheory.Lp F p μ)Prop) (h_ind : ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ), P (MeasureTheory.Lp.simpleFunc.indicatorConst p c)) (h_add : ∀ ⦃f g : αF⦄ (hf : MeasureTheory.Memℒp f p μ) (hg : MeasureTheory.Memℒp g p μ), MeasureTheory.AEStronglyMeasurable' m f μMeasureTheory.AEStronglyMeasurable' m g μDisjoint (Function.support f) (Function.support g)P (MeasureTheory.Memℒp.toLp f hf)P (MeasureTheory.Memℒp.toLp g hg)P (MeasureTheory.Memℒp.toLp f hf + MeasureTheory.Memℒp.toLp g hg)) (h_closed : IsClosed {f : (MeasureTheory.lpMeas F m p μ) | P f}) (f : (MeasureTheory.Lp F p μ)) :

                        Auxiliary lemma for Lp.induction_stronglyMeasurable.

                        theorem MeasureTheory.Lp.induction_stronglyMeasurable {α : Type u_1} {F : Type u_3} {p : ENNReal} [NormedAddCommGroup F] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Fact (1 p)] [NormedSpace F] (hm : m m0) (hp_ne_top : p ) (P : (MeasureTheory.Lp F p μ)Prop) (h_ind : ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ), P (MeasureTheory.Lp.simpleFunc.indicatorConst p c)) (h_add : ∀ ⦃f g : αF⦄ (hf : MeasureTheory.Memℒp f p μ) (hg : MeasureTheory.Memℒp g p μ), MeasureTheory.StronglyMeasurable fMeasureTheory.StronglyMeasurable gDisjoint (Function.support f) (Function.support g)P (MeasureTheory.Memℒp.toLp f hf)P (MeasureTheory.Memℒp.toLp g hg)P (MeasureTheory.Memℒp.toLp f hf + MeasureTheory.Memℒp.toLp g hg)) (h_closed : IsClosed {f : (MeasureTheory.lpMeas F m p μ) | P f}) (f : (MeasureTheory.Lp F p μ)) :

                        To prove something for an Lp function a.e. strongly measurable with respect to a sub-σ-algebra m in a normed space, it suffices to show that

                        • the property holds for (multiples of) characteristic functions which are measurable w.r.t. m;
                        • is closed under addition;
                        • the set of functions in Lp strongly measurable w.r.t. m for which the property holds is closed.
                        theorem MeasureTheory.Memℒp.induction_stronglyMeasurable {α : Type u_1} {F : Type u_3} {p : ENNReal} [NormedAddCommGroup F] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Fact (1 p)] [NormedSpace F] (hm : m m0) (hp_ne_top : p ) (P : (αF)Prop) (h_ind : ∀ (c : F) ⦃s : Set α⦄, MeasurableSet sμ s < P (s.indicator fun (x : α) => c)) (h_add : ∀ ⦃f g : αF⦄, Disjoint (Function.support f) (Function.support g)MeasureTheory.Memℒp f p μMeasureTheory.Memℒp g p μMeasureTheory.StronglyMeasurable fMeasureTheory.StronglyMeasurable gP fP gP (f + g)) (h_closed : IsClosed {f : (MeasureTheory.lpMeas F m p μ) | P f}) (h_ae : ∀ ⦃f g : αF⦄, f =ᵐ[μ] gMeasureTheory.Memℒp f p μP fP g) ⦃f : αF :

                        To prove something for an arbitrary Memℒp function a.e. strongly measurable with respect to a sub-σ-algebra m in a normed space, it suffices to show that

                        • the property holds for (multiples of) characteristic functions which are measurable w.r.t. m;
                        • is closed under addition;
                        • the set of functions in the Lᵖ space strongly measurable w.r.t. m for which the property holds is closed.
                        • the property is closed under the almost-everywhere equal relation.