Documentation

Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Strongly measurable and finitely strongly measurable functions #

A function f is said to be strongly measurable if f is the sequential limit of simple functions. It is said to be finitely strongly measurable with respect to a measure μ if the supports of those simple functions have finite measure. We also provide almost everywhere versions of these notions.

Almost everywhere strongly measurable functions form the largest class of functions that can be integrated using the Bochner integral.

If the target space has a second countable topology, strongly measurable and measurable are equivalent.

If the measure is sigma-finite, strongly measurable and finitely strongly measurable are equivalent.

The main property of finitely strongly measurable functions is FinStronglyMeasurable.exists_set_sigmaFinite: there exists a measurable set t such that the function is supported on t and μ.restrict t is sigma-finite. As a consequence, we can prove some results for those functions as if the measure was sigma-finite.

Main definitions #

Main statements #

We provide a solid API for strongly measurable functions, and for almost everywhere strongly measurable functions, as a basis for the Bochner integral.

References #

def MeasureTheory.StronglyMeasurable {α : Type u_1} {β : Type u_2} [TopologicalSpace β] [MeasurableSpace α] (f : αβ) :

A function is StronglyMeasurable if it is the limit of simple functions.

Equations
Instances For

    The notation for StronglyMeasurable giving the measurable space instance explicitly.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      def MeasureTheory.FinStronglyMeasurable {α : Type u_1} {β : Type u_2} [TopologicalSpace β] [Zero β] :
      {x : MeasurableSpace α} → (αβ)autoParam (MeasureTheory.Measure α) _auto✝Prop

      A function is FinStronglyMeasurable with respect to a measure if it is the limit of simple functions with support with finite measure.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        def MeasureTheory.AEStronglyMeasurable {α : Type u_1} {β : Type u_2} [TopologicalSpace β] :
        {x : MeasurableSpace α} → (αβ)autoParam (MeasureTheory.Measure α) _auto✝Prop

        A function is AEStronglyMeasurable with respect to a measure μ if it is almost everywhere equal to the limit of a sequence of simple functions.

        Equations
        Instances For
          def MeasureTheory.AEFinStronglyMeasurable {α : Type u_1} {β : Type u_2} [TopologicalSpace β] [Zero β] :
          {x : MeasurableSpace α} → (αβ)autoParam (MeasureTheory.Measure α) _auto✝Prop

          A function is AEFinStronglyMeasurable with respect to a measure if it is almost everywhere equal to the limit of a sequence of simple functions with support with finite measure.

          Equations
          Instances For

            Strongly measurable functions #

            @[deprecated MeasureTheory.StronglyMeasurable.of_finite]
            theorem MeasureTheory.stronglyMeasurable_of_fintype {α : Type u_1} {β : Type u_2} [Finite α] :
            ∀ {x : MeasurableSpace α} [inst : MeasurableSingletonClass α] [inst : TopologicalSpace β] {f : αβ}, MeasureTheory.StronglyMeasurable f

            Alias of MeasureTheory.StronglyMeasurable.of_finite.

            @[deprecated MeasureTheory.StronglyMeasurable.of_finite]
            theorem MeasureTheory.stronglyMeasurable_of_isEmpty {α : Type u_1} {β : Type u_2} [IsEmpty α] :
            ∀ {x : MeasurableSpace α} [inst : TopologicalSpace β] (f : αβ), MeasureTheory.StronglyMeasurable f
            theorem MeasureTheory.stronglyMeasurable_const {α : Type u_5} {β : Type u_6} :
            ∀ {x : MeasurableSpace α} [inst : TopologicalSpace β] {b : β}, MeasureTheory.StronglyMeasurable fun (x : α) => b
            theorem MeasureTheory.stronglyMeasurable_zero {α : Type u_5} {β : Type u_6} :
            ∀ {x : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : Zero β], MeasureTheory.StronglyMeasurable 0
            theorem MeasureTheory.stronglyMeasurable_one {α : Type u_5} {β : Type u_6} :
            ∀ {x : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : One β], MeasureTheory.StronglyMeasurable 1
            theorem MeasureTheory.stronglyMeasurable_const' {α : Type u_5} {β : Type u_6} {m : MeasurableSpace α} [TopologicalSpace β] {f : αβ} (hf : ∀ (x y : α), f x = f y) :

            A version of stronglyMeasurable_const that assumes f x = f y for all x, y. This version works for functions between empty types.

            noncomputable def MeasureTheory.StronglyMeasurable.approx {α : Type u_1} {β : Type u_2} {f : αβ} [TopologicalSpace β] :

            A sequence of simple functions such that ∀ x, Tendsto (fun n => hf.approx n x) atTop (𝓝 (f x)). That property is given by stronglyMeasurable.tendsto_approx.

            Equations
            Instances For
              theorem MeasureTheory.StronglyMeasurable.tendsto_approx {α : Type u_1} {β : Type u_2} {f : αβ} [TopologicalSpace β] :
              ∀ {x : MeasurableSpace α} (hf : MeasureTheory.StronglyMeasurable f) (x_1 : α), Filter.Tendsto (fun (n : ) => (hf.approx n) x_1) Filter.atTop (nhds (f x_1))
              noncomputable def MeasureTheory.StronglyMeasurable.approxBounded {α : Type u_1} {β : Type u_2} {f : αβ} [TopologicalSpace β] :
              {x : MeasurableSpace α} → [inst : Norm β] → [inst : SMul β] → MeasureTheory.StronglyMeasurable fMeasureTheory.SimpleFunc α β

              Similar to stronglyMeasurable.approx, but enforces that the norm of every function in the sequence is less than c everywhere. If ‖f x‖ ≤ c this sequence of simple functions verifies Tendsto (fun n => hf.approxBounded n x) atTop (𝓝 (f x)).

              Equations
              Instances For
                theorem MeasureTheory.StronglyMeasurable.tendsto_approxBounded_of_norm_le {α : Type u_1} {β : Type u_5} {f : αβ} [NormedAddCommGroup β] [NormedSpace β] {m : MeasurableSpace α} (hf : MeasureTheory.StronglyMeasurable f) {c : } {x : α} (hfx : f x c) :
                Filter.Tendsto (fun (n : ) => (hf.approxBounded c n) x) Filter.atTop (nhds (f x))
                theorem MeasureTheory.StronglyMeasurable.tendsto_approxBounded_ae {α : Type u_1} {β : Type u_5} {f : αβ} [NormedAddCommGroup β] [NormedSpace β] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hf : MeasureTheory.StronglyMeasurable f) {c : } (hf_bound : ∀ᵐ (x : α) ∂μ, f x c) :
                ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ) => (hf.approxBounded c n) x) Filter.atTop (nhds (f x))
                theorem MeasureTheory.StronglyMeasurable.norm_approxBounded_le {α : Type u_1} {β : Type u_5} {f : αβ} [SeminormedAddCommGroup β] [NormedSpace β] {m : MeasurableSpace α} {c : } (hf : MeasureTheory.StronglyMeasurable f) (hc : 0 c) (n : ) (x : α) :
                (hf.approxBounded c n) x c
                theorem stronglyMeasurable_bot_iff {α : Type u_1} {β : Type u_2} {f : αβ} [TopologicalSpace β] [Nonempty β] [T2Space β] :
                MeasureTheory.StronglyMeasurable f ∃ (c : β), f = fun (x : α) => c
                theorem MeasureTheory.StronglyMeasurable.finStronglyMeasurable_of_set_sigmaFinite {α : Type u_1} {β : Type u_2} {f : αβ} [TopologicalSpace β] [Zero β] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hf_meas : MeasureTheory.StronglyMeasurable f) {t : Set α} (ht : MeasurableSet t) (hft_zero : xt, f x = 0) (htμ : MeasureTheory.SigmaFinite (μ.restrict t)) :

                If the measure is sigma-finite, all strongly measurable functions are FinStronglyMeasurable.

                theorem MeasureTheory.StronglyMeasurable.measurable {α : Type u_1} {β : Type u_2} {f : αβ} :

                A strongly measurable function is measurable.

                theorem MeasureTheory.StronglyMeasurable.aemeasurable {α : Type u_1} {β : Type u_2} {f : αβ} :

                A strongly measurable function is almost everywhere measurable.

                theorem Continuous.comp_stronglyMeasurable {α : Type u_1} {β : Type u_2} {γ : Type u_3} :
                ∀ {x : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : TopologicalSpace γ] {g : βγ} {f : αβ}, Continuous gMeasureTheory.StronglyMeasurable fMeasureTheory.StronglyMeasurable fun (x : α) => g (f x)
                theorem MeasureTheory.StronglyMeasurable.prod_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} [TopologicalSpace β] [TopologicalSpace γ] {f : αβ} {g : αγ} (hf : MeasureTheory.StronglyMeasurable f) (hg : MeasureTheory.StronglyMeasurable g) :
                MeasureTheory.StronglyMeasurable fun (x : α) => (f x, g x)
                theorem MeasureTheory.StronglyMeasurable.comp_measurable {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace β] :
                ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace γ} {f : αβ} {g : γα}, MeasureTheory.StronglyMeasurable fMeasurable gMeasureTheory.StronglyMeasurable (f g)
                theorem MeasureTheory.StronglyMeasurable.of_uncurry_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace β] :
                ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace γ} {f : αγβ}, MeasureTheory.StronglyMeasurable (Function.uncurry f)∀ {x : α}, MeasureTheory.StronglyMeasurable (f x)
                theorem MeasureTheory.StronglyMeasurable.of_uncurry_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace β] :
                ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace γ} {f : αγβ}, MeasureTheory.StronglyMeasurable (Function.uncurry f)∀ {y : γ}, MeasureTheory.StronglyMeasurable fun (x : α) => f x y
                theorem MeasureTheory.StronglyMeasurable.add_const {α : Type u_1} {β : Type u_2} {f : αβ} {mα : MeasurableSpace α} [TopologicalSpace β] [Add β] [ContinuousAdd β] (hf : MeasureTheory.StronglyMeasurable f) (c : β) :
                MeasureTheory.StronglyMeasurable fun (x : α) => f x + c
                theorem MeasureTheory.StronglyMeasurable.mul_const {α : Type u_1} {β : Type u_2} {f : αβ} {mα : MeasurableSpace α} [TopologicalSpace β] [Mul β] [ContinuousMul β] (hf : MeasureTheory.StronglyMeasurable f) (c : β) :
                MeasureTheory.StronglyMeasurable fun (x : α) => f x * c
                theorem MeasureTheory.StronglyMeasurable.const_add {α : Type u_1} {β : Type u_2} {f : αβ} {mα : MeasurableSpace α} [TopologicalSpace β] [Add β] [ContinuousAdd β] (hf : MeasureTheory.StronglyMeasurable f) (c : β) :
                MeasureTheory.StronglyMeasurable fun (x : α) => c + f x
                theorem MeasureTheory.StronglyMeasurable.const_mul {α : Type u_1} {β : Type u_2} {f : αβ} {mα : MeasurableSpace α} [TopologicalSpace β] [Mul β] [ContinuousMul β] (hf : MeasureTheory.StronglyMeasurable f) (c : β) :
                MeasureTheory.StronglyMeasurable fun (x : α) => c * f x
                theorem MeasureTheory.StronglyMeasurable.vadd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [TopologicalSpace β] {𝕜 : Type u_5} [TopologicalSpace 𝕜] [VAdd 𝕜 β] [ContinuousVAdd 𝕜 β] {f : α𝕜} {g : αβ} (hf : MeasureTheory.StronglyMeasurable f) (hg : MeasureTheory.StronglyMeasurable g) :
                MeasureTheory.StronglyMeasurable fun (x : α) => f x +ᵥ g x
                theorem MeasureTheory.StronglyMeasurable.smul {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [TopologicalSpace β] {𝕜 : Type u_5} [TopologicalSpace 𝕜] [SMul 𝕜 β] [ContinuousSMul 𝕜 β] {f : α𝕜} {g : αβ} (hf : MeasureTheory.StronglyMeasurable f) (hg : MeasureTheory.StronglyMeasurable g) :
                MeasureTheory.StronglyMeasurable fun (x : α) => f x g x
                theorem MeasureTheory.StronglyMeasurable.const_vadd {α : Type u_1} {β : Type u_2} {f : αβ} {mα : MeasurableSpace α} [TopologicalSpace β] {𝕜 : Type u_5} [VAdd 𝕜 β] [ContinuousConstVAdd 𝕜 β] (hf : MeasureTheory.StronglyMeasurable f) (c : 𝕜) :
                theorem MeasureTheory.StronglyMeasurable.const_smul {α : Type u_1} {β : Type u_2} {f : αβ} {mα : MeasurableSpace α} [TopologicalSpace β] {𝕜 : Type u_5} [SMul 𝕜 β] [ContinuousConstSMul 𝕜 β] (hf : MeasureTheory.StronglyMeasurable f) (c : 𝕜) :
                theorem MeasureTheory.StronglyMeasurable.const_vadd' {α : Type u_1} {β : Type u_2} {f : αβ} {mα : MeasurableSpace α} [TopologicalSpace β] {𝕜 : Type u_5} [VAdd 𝕜 β] [ContinuousConstVAdd 𝕜 β] (hf : MeasureTheory.StronglyMeasurable f) (c : 𝕜) :
                theorem MeasureTheory.StronglyMeasurable.const_smul' {α : Type u_1} {β : Type u_2} {f : αβ} {mα : MeasurableSpace α} [TopologicalSpace β] {𝕜 : Type u_5} [SMul 𝕜 β] [ContinuousConstSMul 𝕜 β] (hf : MeasureTheory.StronglyMeasurable f) (c : 𝕜) :
                theorem MeasureTheory.StronglyMeasurable.vadd_const {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [TopologicalSpace β] {𝕜 : Type u_5} [TopologicalSpace 𝕜] [VAdd 𝕜 β] [ContinuousVAdd 𝕜 β] {f : α𝕜} (hf : MeasureTheory.StronglyMeasurable f) (c : β) :
                theorem MeasureTheory.StronglyMeasurable.smul_const {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [TopologicalSpace β] {𝕜 : Type u_5} [TopologicalSpace 𝕜] [SMul 𝕜 β] [ContinuousSMul 𝕜 β] {f : α𝕜} (hf : MeasureTheory.StronglyMeasurable f) (c : β) :
                theorem Measurable.add_stronglyMeasurable {α : Type u_5} {E : Type u_6} :
                ∀ {x : MeasurableSpace α} [inst : AddGroup E] [inst_1 : TopologicalSpace E] [inst_2 : MeasurableSpace E] [inst_3 : BorelSpace E] [inst_4 : ContinuousAdd E] [inst_5 : TopologicalSpace.PseudoMetrizableSpace E] {g f : αE}, Measurable gMeasureTheory.StronglyMeasurable fMeasurable (g + f)

                In a normed vector space, the addition of a measurable function and a strongly measurable function is measurable. Note that this is not true without further second-countability assumptions for the addition of two measurable functions.

                theorem Measurable.sub_stronglyMeasurable {α : Type u_5} {E : Type u_6} :
                ∀ {x : MeasurableSpace α} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [inst_2 : MeasurableSpace E] [inst_3 : BorelSpace E] [inst_4 : ContinuousAdd E] [inst_5 : ContinuousNeg E] [inst_6 : TopologicalSpace.PseudoMetrizableSpace E] {g f : αE}, Measurable gMeasureTheory.StronglyMeasurable fMeasurable (g - f)

                In a normed vector space, the subtraction of a measurable function and a strongly measurable function is measurable. Note that this is not true without further second-countability assumptions for the subtraction of two measurable functions.

                theorem Measurable.stronglyMeasurable_add {α : Type u_5} {E : Type u_6} :
                ∀ {x : MeasurableSpace α} [inst : AddGroup E] [inst_1 : TopologicalSpace E] [inst_2 : MeasurableSpace E] [inst_3 : BorelSpace E] [inst_4 : ContinuousAdd E] [inst_5 : TopologicalSpace.PseudoMetrizableSpace E] {g f : αE}, Measurable gMeasureTheory.StronglyMeasurable fMeasurable (f + g)

                In a normed vector space, the addition of a strongly measurable function and a measurable function is measurable. Note that this is not true without further second-countability assumptions for the addition of two measurable functions.

                theorem stronglyMeasurable_const_smul_iff {α : Type u_1} {β : Type u_2} {f : αβ} {G : Type u_6} [TopologicalSpace β] [Group G] [MulAction G β] [ContinuousConstSMul G β] {m : MeasurableSpace α} (c : G) :
                theorem IsUnit.stronglyMeasurable_const_smul_iff {α : Type u_1} {β : Type u_2} {f : αβ} {M : Type u_5} [TopologicalSpace β] [Monoid M] [MulAction M β] [ContinuousConstSMul M β] :
                ∀ {x : MeasurableSpace α} {c : M}, IsUnit c((MeasureTheory.StronglyMeasurable fun (x : α) => c f x) MeasureTheory.StronglyMeasurable f)
                theorem stronglyMeasurable_const_smul_iff₀ {α : Type u_1} {β : Type u_2} {f : αβ} {G₀ : Type u_7} [TopologicalSpace β] [GroupWithZero G₀] [MulAction G₀ β] [ContinuousConstSMul G₀ β] :
                ∀ {x : MeasurableSpace α} {c : G₀}, c 0((MeasureTheory.StronglyMeasurable fun (x : α) => c f x) MeasureTheory.StronglyMeasurable f)

                Big operators: and #

                theorem List.stronglyMeasurable_sum {α : Type u_1} {M : Type u_5} [AddMonoid M] [TopologicalSpace M] [ContinuousAdd M] {m : MeasurableSpace α} (l : List (αM)) (hl : fl, MeasureTheory.StronglyMeasurable f) :
                MeasureTheory.StronglyMeasurable fun (x : α) => (List.map (fun (f : αM) => f x) l).sum
                theorem List.stronglyMeasurable_prod {α : Type u_1} {M : Type u_5} [Monoid M] [TopologicalSpace M] [ContinuousMul M] {m : MeasurableSpace α} (l : List (αM)) (hl : fl, MeasureTheory.StronglyMeasurable f) :
                MeasureTheory.StronglyMeasurable fun (x : α) => (List.map (fun (f : αM) => f x) l).prod
                theorem Multiset.stronglyMeasurable_sum {α : Type u_1} {M : Type u_5} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] {m : MeasurableSpace α} (s : Multiset (αM)) (hs : fs, MeasureTheory.StronglyMeasurable f) :
                MeasureTheory.StronglyMeasurable fun (x : α) => (Multiset.map (fun (f : αM) => f x) s).sum
                theorem Multiset.stronglyMeasurable_prod {α : Type u_1} {M : Type u_5} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] {m : MeasurableSpace α} (s : Multiset (αM)) (hs : fs, MeasureTheory.StronglyMeasurable f) :
                MeasureTheory.StronglyMeasurable fun (x : α) => (Multiset.map (fun (f : αM) => f x) s).prod
                theorem Finset.stronglyMeasurable_sum' {α : Type u_1} {M : Type u_5} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] {m : MeasurableSpace α} {ι : Type u_6} {f : ιαM} (s : Finset ι) (hf : is, MeasureTheory.StronglyMeasurable (f i)) :
                theorem Finset.stronglyMeasurable_prod' {α : Type u_1} {M : Type u_5} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] {m : MeasurableSpace α} {ι : Type u_6} {f : ιαM} (s : Finset ι) (hf : is, MeasureTheory.StronglyMeasurable (f i)) :
                theorem Finset.stronglyMeasurable_sum {α : Type u_1} {M : Type u_5} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] {m : MeasurableSpace α} {ι : Type u_6} {f : ιαM} (s : Finset ι) (hf : is, MeasureTheory.StronglyMeasurable (f i)) :
                MeasureTheory.StronglyMeasurable fun (a : α) => is, f i a
                theorem Finset.stronglyMeasurable_prod {α : Type u_1} {M : Type u_5} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] {m : MeasurableSpace α} {ι : Type u_6} {f : ιαM} (s : Finset ι) (hf : is, MeasureTheory.StronglyMeasurable (f i)) :
                MeasureTheory.StronglyMeasurable fun (a : α) => is, f i a

                The range of a strongly measurable function is separable.

                In a space with second countable topology, measurable implies strongly measurable.

                In a space with second countable topology, strongly measurable and measurable are equivalent.

                A function is strongly measurable if and only if it is measurable and has separable range.

                A continuous function is strongly measurable when either the source space or the target space is second-countable.

                A continuous function whose support is contained in a compact set is strongly measurable.

                A continuous function with compact support is strongly measurable.

                A continuous function with compact support on a product space is strongly measurable for the product sigma-algebra. The subtlety is that we do not assume that the spaces are separable, so the product of the Borel sigma algebras might not contain all open sets, but still it contains enough of them to approximate compactly supported continuous functions.

                If g is a topological embedding, then f is strongly measurable iff g ∘ f is.

                theorem stronglyMeasurable_of_tendsto {α : Type u_1} {β : Type u_2} {ι : Type u_5} {m : MeasurableSpace α} [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] (u : Filter ι) [u.NeBot] [u.IsCountablyGenerated] {f : ιαβ} {g : αβ} (hf : ∀ (i : ι), MeasureTheory.StronglyMeasurable (f i)) (lim : Filter.Tendsto f u (nhds g)) :

                A sequential limit of strongly measurable functions is strongly measurable.

                theorem MeasureTheory.StronglyMeasurable.piecewise {α : Type u_1} {β : Type u_2} {f : αβ} {g : αβ} {m : MeasurableSpace α} [TopologicalSpace β] {s : Set α} :
                theorem MeasureTheory.StronglyMeasurable.ite {α : Type u_1} {β : Type u_2} {f : αβ} {g : αβ} :
                ∀ {x : MeasurableSpace α} [inst : TopologicalSpace β] {p : αProp} {x_1 : DecidablePred p}, MeasurableSet {a : α | p a}MeasureTheory.StronglyMeasurable fMeasureTheory.StronglyMeasurable gMeasureTheory.StronglyMeasurable fun (x : α) => if p x then f x else g x

                this is slightly different from StronglyMeasurable.piecewise. It can be used to show StronglyMeasurable (ite (x=0) 0 1) by exact StronglyMeasurable.ite (measurableSet_singleton 0) stronglyMeasurable_const stronglyMeasurable_const, but replacing StronglyMeasurable.ite by StronglyMeasurable.piecewise in that example proof does not work.

                theorem MeasurableEmbedding.stronglyMeasurable_extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβ} {g : αγ} {g' : γβ} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} [TopologicalSpace β] (hg : MeasurableEmbedding g) (hf : MeasureTheory.StronglyMeasurable f) (hg' : MeasureTheory.StronglyMeasurable g') :
                theorem MeasurableEmbedding.exists_stronglyMeasurable_extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβ} {g : αγ} :
                ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace γ} [inst : TopologicalSpace β], MeasurableEmbedding gMeasureTheory.StronglyMeasurable f(γNonempty β)∃ (f' : γβ), MeasureTheory.StronglyMeasurable f' f' g = f
                theorem stronglyMeasurable_of_stronglyMeasurable_union_cover {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [TopologicalSpace β] {f : αβ} (s : Set α) (t : Set α) (hs : MeasurableSet s) (ht : MeasurableSet t) (h : Set.univ s t) (hc : MeasureTheory.StronglyMeasurable fun (a : s) => f a) (hd : MeasureTheory.StronglyMeasurable fun (a : t) => f a) :
                theorem MeasureTheory.StronglyMeasurable.indicator {α : Type u_1} {β : Type u_2} {f : αβ} :
                ∀ {x : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : Zero β], MeasureTheory.StronglyMeasurable f∀ {s : Set α}, MeasurableSet sMeasureTheory.StronglyMeasurable (s.indicator f)
                theorem MeasureTheory.StronglyMeasurable.dist {α : Type u_1} :
                ∀ {x : MeasurableSpace α} {β : Type u_5} [inst : PseudoMetricSpace β] {f g : αβ}, MeasureTheory.StronglyMeasurable fMeasureTheory.StronglyMeasurable gMeasureTheory.StronglyMeasurable fun (x : α) => dist (f x) (g x)
                theorem MeasureTheory.StronglyMeasurable.ennnorm {α : Type u_1} :
                ∀ {x : MeasurableSpace α} {β : Type u_5} [inst : SeminormedAddCommGroup β] {f : αβ}, MeasureTheory.StronglyMeasurable fMeasurable fun (a : α) => f a‖₊
                theorem MeasureTheory.StronglyMeasurable.stronglyMeasurable_in_set {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [TopologicalSpace β] [Zero β] {s : Set α} {f : αβ} (hs : MeasurableSet s) (hf : MeasureTheory.StronglyMeasurable f) (hf_zero : xs, f x = 0) :
                ∃ (fs : MeasureTheory.SimpleFunc α β), (∀ (x : α), Filter.Tendsto (fun (n : ) => (fs n) x) Filter.atTop (nhds (f x))) xs, ∀ (n : ), (fs n) x = 0
                theorem MeasureTheory.StronglyMeasurable.stronglyMeasurable_of_measurableSpace_le_on {α : Type u_5} {E : Type u_6} {m : MeasurableSpace α} {m₂ : MeasurableSpace α} [TopologicalSpace E] [Zero E] {s : Set α} {f : αE} (hs_m : MeasurableSet s) (hs : ∀ (t : Set α), MeasurableSet (s t)MeasurableSet (s t)) (hf : MeasureTheory.StronglyMeasurable f) (hf_zero : xs, f x = 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 supported on s is m-strongly-measurable, then f is also m₂-strongly-measurable.

                theorem MeasureTheory.StronglyMeasurable.exists_spanning_measurableSet_norm_le {α : Type u_1} {β : Type u_2} {f : αβ} [SeminormedAddCommGroup β] {m : MeasurableSpace α} {m0 : MeasurableSpace α} (hm : m m0) (hf : MeasureTheory.StronglyMeasurable f) (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite (μ.trim hm)] :
                ∃ (s : Set α), (∀ (n : ), MeasurableSet (s n) μ (s n) < xs n, f x n) ⋃ (i : ), s i = Set.univ

                If a function f is strongly measurable w.r.t. a sub-σ-algebra m and the measure is σ-finite on m, then there exists spanning measurable sets with finite measure on which f has bounded norm. In particular, f is integrable on each of those sets.

                Finitely strongly measurable functions #

                noncomputable def MeasureTheory.FinStronglyMeasurable.approx {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αβ} [Zero β] [TopologicalSpace β] (hf : MeasureTheory.FinStronglyMeasurable f μ) :

                A sequence of simple functions such that ∀ x, Tendsto (fun n ↦ hf.approx n x) atTop (𝓝 (f x)) and ∀ n, μ (support (hf.approx n)) < ∞. These properties are given by FinStronglyMeasurable.tendsto_approx and FinStronglyMeasurable.fin_support_approx.

                Equations
                Instances For
                  theorem MeasureTheory.FinStronglyMeasurable.fin_support_approx {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αβ} [Zero β] [TopologicalSpace β] (hf : MeasureTheory.FinStronglyMeasurable f μ) (n : ) :
                  μ (Function.support (hf.approx n)) <
                  theorem MeasureTheory.FinStronglyMeasurable.tendsto_approx {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αβ} [Zero β] [TopologicalSpace β] (hf : MeasureTheory.FinStronglyMeasurable f μ) (x : α) :
                  Filter.Tendsto (fun (n : ) => (hf.approx n) x) Filter.atTop (nhds (f x))

                  A finitely strongly measurable function is strongly measurable.

                  theorem MeasureTheory.FinStronglyMeasurable.exists_set_sigmaFinite {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αβ} [Zero β] [TopologicalSpace β] [T2Space β] (hf : MeasureTheory.FinStronglyMeasurable f μ) :
                  ∃ (t : Set α), MeasurableSet t (∀ xt, f x = 0) MeasureTheory.SigmaFinite (μ.restrict t)

                  A finitely strongly measurable function is measurable.

                  theorem MeasureTheory.FinStronglyMeasurable.const_smul {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αβ} [TopologicalSpace β] {𝕜 : Type u_5} [TopologicalSpace 𝕜] [AddMonoid β] [Monoid 𝕜] [DistribMulAction 𝕜 β] [ContinuousSMul 𝕜 β] (hf : MeasureTheory.FinStronglyMeasurable f μ) (c : 𝕜) :

                  Almost everywhere strongly measurable functions #

                  theorem MeasureTheory.aestronglyMeasurable_const {α : Type u_5} {β : Type u_6} :
                  ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β] {b : β}, MeasureTheory.AEStronglyMeasurable (fun (x : α) => b) μ
                  @[simp]
                  theorem MeasureTheory.Subsingleton.aestronglyMeasurable {α : Type u_1} {β : Type u_2} :
                  ∀ {x : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : Subsingleton β] {μ : MeasureTheory.Measure α} (f : αβ), MeasureTheory.AEStronglyMeasurable f μ
                  @[simp]
                  theorem MeasureTheory.Subsingleton.aestronglyMeasurable' {α : Type u_1} {β : Type u_2} :
                  ∀ {x : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : Subsingleton α] {μ : MeasureTheory.Measure α} (f : αβ), MeasureTheory.AEStronglyMeasurable f μ
                  noncomputable def MeasureTheory.AEStronglyMeasurable.mk {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] (f : αβ) (hf : MeasureTheory.AEStronglyMeasurable f μ) :
                  αβ

                  A StronglyMeasurable function such that f =ᵐ[μ] hf.mk f. See lemmas stronglyMeasurable_mk and ae_eq_mk.

                  Equations
                  Instances For
                    theorem MeasureTheory.AEStronglyMeasurable.congr {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : αβ} {g : αβ} (hf : MeasureTheory.AEStronglyMeasurable f μ) (h : f =ᵐ[μ] g) :
                    theorem aestronglyMeasurable_congr {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : αβ} {g : αβ} (h : f =ᵐ[μ] g) :
                    theorem MeasureTheory.AEStronglyMeasurable.mono_ac {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [TopologicalSpace β] {f : αβ} (h : ν.AbsolutelyContinuous μ) (hμ : MeasureTheory.AEStronglyMeasurable f μ) :
                    @[deprecated MeasureTheory.AEStronglyMeasurable.mono_ac]
                    theorem MeasureTheory.AEStronglyMeasurable.mono' {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [TopologicalSpace β] {f : αβ} (h : ν.AbsolutelyContinuous μ) (hμ : MeasureTheory.AEStronglyMeasurable f μ) :

                    Alias of MeasureTheory.AEStronglyMeasurable.mono_ac.

                    theorem MeasureTheory.AEStronglyMeasurable.mono_set {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : αβ} {s : Set α} {t : Set α} (h : s t) (ht : MeasureTheory.AEStronglyMeasurable f (μ.restrict t)) :
                    theorem MeasureTheory.AEStronglyMeasurable.ae_mem_imp_eq_mk {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : αβ} {s : Set α} (h : MeasureTheory.AEStronglyMeasurable f (μ.restrict s)) :
                    ∀ᵐ (x : α) ∂μ, x sf x = MeasureTheory.AEStronglyMeasurable.mk f h x
                    theorem Continuous.comp_aestronglyMeasurable {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] [TopologicalSpace γ] {g : βγ} {f : αβ} (hg : Continuous g) (hf : MeasureTheory.AEStronglyMeasurable f μ) :
                    MeasureTheory.AEStronglyMeasurable (fun (x : α) => g (f x)) μ

                    The composition of a continuous function and an ae strongly measurable function is ae strongly measurable.

                    A continuous function from α to β is ae strongly measurable when one of the two spaces is second countable.

                    theorem MeasureTheory.AEStronglyMeasurable.prod_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] [TopologicalSpace γ] {f : αβ} {g : αγ} (hf : MeasureTheory.AEStronglyMeasurable f μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) :
                    MeasureTheory.AEStronglyMeasurable (fun (x : α) => (f x, g x)) μ
                    theorem Continuous.comp_aestronglyMeasurable₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] [TopologicalSpace γ] {β' : Type u_5} [TopologicalSpace β'] {g : ββ'γ} {f : αβ} {f' : αβ'} (hg : Continuous (Function.uncurry g)) (hf : MeasureTheory.AEStronglyMeasurable f μ) (h'f : MeasureTheory.AEStronglyMeasurable f' μ) :
                    MeasureTheory.AEStronglyMeasurable (fun (x : α) => g (f x) (f' x)) μ

                    The composition of a continuous function of two variables and two ae strongly measurable functions is ae strongly measurable.

                    In a space with second countable topology, measurable implies ae strongly measurable.

                    theorem MeasureTheory.AEStronglyMeasurable.add_const {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : αβ} [Add β] [ContinuousAdd β] (hf : MeasureTheory.AEStronglyMeasurable f μ) (c : β) :
                    MeasureTheory.AEStronglyMeasurable (fun (x : α) => f x + c) μ
                    theorem MeasureTheory.AEStronglyMeasurable.mul_const {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : αβ} [Mul β] [ContinuousMul β] (hf : MeasureTheory.AEStronglyMeasurable f μ) (c : β) :
                    MeasureTheory.AEStronglyMeasurable (fun (x : α) => f x * c) μ
                    theorem MeasureTheory.AEStronglyMeasurable.const_add {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : αβ} [Add β] [ContinuousAdd β] (hf : MeasureTheory.AEStronglyMeasurable f μ) (c : β) :
                    MeasureTheory.AEStronglyMeasurable (fun (x : α) => c + f x) μ
                    theorem MeasureTheory.AEStronglyMeasurable.const_mul {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : αβ} [Mul β] [ContinuousMul β] (hf : MeasureTheory.AEStronglyMeasurable f μ) (c : β) :
                    MeasureTheory.AEStronglyMeasurable (fun (x : α) => c * f x) μ
                    theorem MeasureTheory.AEStronglyMeasurable.vadd {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {𝕜 : Type u_5} [TopologicalSpace 𝕜] [VAdd 𝕜 β] [ContinuousVAdd 𝕜 β] {f : α𝕜} {g : αβ} (hf : MeasureTheory.AEStronglyMeasurable f μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) :
                    MeasureTheory.AEStronglyMeasurable (fun (x : α) => f x +ᵥ g x) μ
                    theorem MeasureTheory.AEStronglyMeasurable.smul {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {𝕜 : Type u_5} [TopologicalSpace 𝕜] [SMul 𝕜 β] [ContinuousSMul 𝕜 β] {f : α𝕜} {g : αβ} (hf : MeasureTheory.AEStronglyMeasurable f μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) :
                    MeasureTheory.AEStronglyMeasurable (fun (x : α) => f x g x) μ
                    theorem MeasureTheory.AEStronglyMeasurable.const_vadd {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : αβ} {𝕜 : Type u_5} [VAdd 𝕜 β] [ContinuousConstVAdd 𝕜 β] (hf : MeasureTheory.AEStronglyMeasurable f μ) (c : 𝕜) :
                    theorem MeasureTheory.AEStronglyMeasurable.const_smul {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : αβ} {𝕜 : Type u_5} [SMul 𝕜 β] [ContinuousConstSMul 𝕜 β] (hf : MeasureTheory.AEStronglyMeasurable f μ) (c : 𝕜) :
                    theorem MeasureTheory.AEStronglyMeasurable.const_vadd' {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : αβ} {𝕜 : Type u_5} [VAdd 𝕜 β] [ContinuousConstVAdd 𝕜 β] (hf : MeasureTheory.AEStronglyMeasurable f μ) (c : 𝕜) :
                    MeasureTheory.AEStronglyMeasurable (fun (x : α) => c +ᵥ f x) μ
                    theorem MeasureTheory.AEStronglyMeasurable.const_smul' {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : αβ} {𝕜 : Type u_5} [SMul 𝕜 β] [ContinuousConstSMul 𝕜 β] (hf : MeasureTheory.AEStronglyMeasurable f μ) (c : 𝕜) :
                    MeasureTheory.AEStronglyMeasurable (fun (x : α) => c f x) μ
                    theorem MeasureTheory.AEStronglyMeasurable.vadd_const {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {𝕜 : Type u_5} [TopologicalSpace 𝕜] [VAdd 𝕜 β] [ContinuousVAdd 𝕜 β] {f : α𝕜} (hf : MeasureTheory.AEStronglyMeasurable f μ) (c : β) :
                    MeasureTheory.AEStronglyMeasurable (fun (x : α) => f x +ᵥ c) μ
                    theorem MeasureTheory.AEStronglyMeasurable.smul_const {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {𝕜 : Type u_5} [TopologicalSpace 𝕜] [SMul 𝕜 β] [ContinuousSMul 𝕜 β] {f : α𝕜} (hf : MeasureTheory.AEStronglyMeasurable f μ) (c : β) :
                    MeasureTheory.AEStronglyMeasurable (fun (x : α) => f x c) μ

                    Big operators: and #

                    theorem List.aestronglyMeasurable_sum {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {M : Type u_5} [AddMonoid M] [TopologicalSpace M] [ContinuousAdd M] (l : List (αM)) (hl : fl, MeasureTheory.AEStronglyMeasurable f μ) :
                    MeasureTheory.AEStronglyMeasurable (fun (x : α) => (List.map (fun (f : αM) => f x) l).sum) μ
                    theorem List.aestronglyMeasurable_prod {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {M : Type u_5} [Monoid M] [TopologicalSpace M] [ContinuousMul M] (l : List (αM)) (hl : fl, MeasureTheory.AEStronglyMeasurable f μ) :
                    MeasureTheory.AEStronglyMeasurable (fun (x : α) => (List.map (fun (f : αM) => f x) l).prod) μ
                    theorem Multiset.aestronglyMeasurable_sum {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {M : Type u_5} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] (s : Multiset (αM)) (hs : fs, MeasureTheory.AEStronglyMeasurable f μ) :
                    MeasureTheory.AEStronglyMeasurable (fun (x : α) => (Multiset.map (fun (f : αM) => f x) s).sum) μ
                    theorem Multiset.aestronglyMeasurable_prod {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {M : Type u_5} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] (s : Multiset (αM)) (hs : fs, MeasureTheory.AEStronglyMeasurable f μ) :
                    MeasureTheory.AEStronglyMeasurable (fun (x : α) => (Multiset.map (fun (f : αM) => f x) s).prod) μ
                    theorem Finset.aestronglyMeasurable_sum' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {M : Type u_5} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] {ι : Type u_6} {f : ιαM} (s : Finset ι) (hf : is, MeasureTheory.AEStronglyMeasurable (f i) μ) :
                    theorem Finset.aestronglyMeasurable_prod' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {M : Type u_5} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] {ι : Type u_6} {f : ιαM} (s : Finset ι) (hf : is, MeasureTheory.AEStronglyMeasurable (f i) μ) :
                    theorem Finset.aestronglyMeasurable_sum {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {M : Type u_5} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] {ι : Type u_6} {f : ιαM} (s : Finset ι) (hf : is, MeasureTheory.AEStronglyMeasurable (f i) μ) :
                    MeasureTheory.AEStronglyMeasurable (fun (a : α) => is, f i a) μ
                    theorem Finset.aestronglyMeasurable_prod {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {M : Type u_5} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] {ι : Type u_6} {f : ιαM} (s : Finset ι) (hf : is, MeasureTheory.AEStronglyMeasurable (f i) μ) :
                    MeasureTheory.AEStronglyMeasurable (fun (a : α) => is, f i a) μ

                    In a space with second countable topology, measurable implies strongly measurable.

                    In a space with second countable topology, strongly measurable and measurable are equivalent.

                    theorem MeasureTheory.AEStronglyMeasurable.dist {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_5} [PseudoMetricSpace β] {f : αβ} {g : αβ} (hf : MeasureTheory.AEStronglyMeasurable f μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) :
                    MeasureTheory.AEStronglyMeasurable (fun (x : α) => dist (f x) (g x)) μ
                    theorem MeasureTheory.AEStronglyMeasurable.ennnorm {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_5} [SeminormedAddCommGroup β] {f : αβ} (hf : MeasureTheory.AEStronglyMeasurable f μ) :
                    AEMeasurable (fun (a : α) => f a‖₊) μ
                    theorem MeasureTheory.AEStronglyMeasurable.edist {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_5} [SeminormedAddCommGroup β] {f : αβ} {g : αβ} (hf : MeasureTheory.AEStronglyMeasurable f μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) :
                    AEMeasurable (fun (a : α) => edist (f a) (g a)) μ
                    theorem aestronglyMeasurable_indicator_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : αβ} [Zero β] {s : Set α} (hs : MeasurableSet s) :
                    theorem MeasureTheory.AEStronglyMeasurable.indicator {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : αβ} [Zero β] (hfm : MeasureTheory.AEStronglyMeasurable f μ) {s : Set α} (hs : MeasurableSet s) :
                    theorem MeasureTheory.AEStronglyMeasurable.isSeparable_ae_range {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : αβ} (hf : MeasureTheory.AEStronglyMeasurable f μ) :
                    ∃ (t : Set β), TopologicalSpace.IsSeparable t ∀ᵐ (x : α) ∂μ, f x t

                    A function is almost everywhere strongly measurable if and only if it is almost everywhere measurable, and up to a zero measure set its range is contained in a separable set.

                    theorem aestronglyMeasurable_of_tendsto_ae {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {ι : Type u_5} [TopologicalSpace.PseudoMetrizableSpace β] (u : Filter ι) [u.NeBot] [u.IsCountablyGenerated] {f : ιαβ} {g : αβ} (hf : ∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ) (lim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ι) => f n x) u (nhds (g x))) :

                    An almost everywhere sequential limit of almost everywhere strongly measurable functions is almost everywhere strongly measurable.

                    theorem exists_stronglyMeasurable_limit_of_tendsto_ae {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] {f : αβ} (hf : ∀ (n : ), MeasureTheory.AEStronglyMeasurable (f n) μ) (h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Filter.Tendsto (fun (n : ) => f n x) Filter.atTop (nhds l)) :
                    ∃ (f_lim : αβ), MeasureTheory.StronglyMeasurable f_lim ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ) => f n x) Filter.atTop (nhds (f_lim x))

                    If a sequence of almost everywhere strongly measurable functions converges almost everywhere, one can select a strongly measurable function as the almost everywhere limit.

                    theorem MeasureTheory.AEStronglyMeasurable.piecewise {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : αβ} {g : αβ} {s : Set α} [DecidablePred fun (x : α) => x s] (hs : MeasurableSet s) (hf : MeasureTheory.AEStronglyMeasurable f (μ.restrict s)) (hg : MeasureTheory.AEStronglyMeasurable g (μ.restrict s)) :
                    theorem MeasureTheory.AEStronglyMeasurable.iUnion {α : Type u_1} {β : Type u_2} {ι : Type u_4} [Countable ι] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : αβ} [TopologicalSpace.PseudoMetrizableSpace β] {s : ιSet α} (h : ∀ (i : ι), MeasureTheory.AEStronglyMeasurable f (μ.restrict (s i))) :
                    MeasureTheory.AEStronglyMeasurable f (μ.restrict (⋃ (i : ι), s i))
                    @[simp]
                    theorem aestronglyMeasurable_iUnion_iff {α : Type u_1} {β : Type u_2} {ι : Type u_4} [Countable ι] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : αβ} [TopologicalSpace.PseudoMetrizableSpace β] {s : ιSet α} :
                    MeasureTheory.AEStronglyMeasurable f (μ.restrict (⋃ (i : ι), s i)) ∀ (i : ι), MeasureTheory.AEStronglyMeasurable f (μ.restrict (s i))
                    @[simp]
                    theorem aestronglyMeasurable_union_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : αβ} [TopologicalSpace.PseudoMetrizableSpace β] {s : Set α} {t : Set α} :
                    theorem aestronglyMeasurable_const_smul_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : αβ} {G : Type u_6} [Group G] [MulAction G β] [ContinuousConstSMul G β] (c : G) :
                    theorem IsUnit.aestronglyMeasurable_const_smul_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : αβ} {M : Type u_5} [Monoid M] [MulAction M β] [ContinuousConstSMul M β] {c : M} (hc : IsUnit c) :
                    theorem aestronglyMeasurable_const_smul_iff₀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : αβ} {G₀ : Type u_7} [GroupWithZero G₀] [MulAction G₀ β] [ContinuousConstSMul G₀ β] {c : G₀} (hc : c 0) :

                    Almost everywhere finitely strongly measurable functions #

                    noncomputable def MeasureTheory.AEFinStronglyMeasurable.mk {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] [Zero β] (f : αβ) (hf : MeasureTheory.AEFinStronglyMeasurable f μ) :
                    αβ

                    A fin_strongly_measurable function such that f =ᵐ[μ] hf.mk f. See lemmas fin_strongly_measurable_mk and ae_eq_mk.

                    Equations
                    Instances For
                      theorem MeasureTheory.AEFinStronglyMeasurable.exists_set_sigmaFinite {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : αβ} [Zero β] [T2Space β] (hf : MeasureTheory.AEFinStronglyMeasurable f μ) :
                      ∃ (t : Set α), MeasurableSet t f =ᵐ[μ.restrict t] 0 MeasureTheory.SigmaFinite (μ.restrict t)

                      A measurable set t such that f =ᵐ[μ.restrict tᶜ] 0 and sigma_finite (μ.restrict t).

                      Equations
                      • hf.sigmaFiniteSet = .choose
                      Instances For
                        theorem MeasureTheory.AEFinStronglyMeasurable.measurableSet {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : αβ} [Zero β] [T2Space β] (hf : MeasureTheory.AEFinStronglyMeasurable f μ) :
                        MeasurableSet hf.sigmaFiniteSet
                        theorem MeasureTheory.AEFinStronglyMeasurable.ae_eq_zero_compl {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : αβ} [Zero β] [T2Space β] (hf : MeasureTheory.AEFinStronglyMeasurable f μ) :
                        f =ᵐ[μ.restrict hf.sigmaFiniteSet] 0
                        instance MeasureTheory.AEFinStronglyMeasurable.sigmaFinite_restrict {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : αβ} [Zero β] [T2Space β] (hf : MeasureTheory.AEFinStronglyMeasurable f μ) :
                        MeasureTheory.SigmaFinite (μ.restrict hf.sigmaFiniteSet)
                        Equations
                        • =

                        In a space with second countable topology and a sigma-finite measure, FinStronglyMeasurable and Measurable are equivalent.

                        In a space with second countable topology and a sigma-finite measure, a measurable function is FinStronglyMeasurable.

                        In a space with second countable topology and a sigma-finite measure, AEFinStronglyMeasurable and AEMeasurable are equivalent.

                        In a space with second countable topology and a sigma-finite measure, an AEMeasurable function is AEFinStronglyMeasurable.

                        theorem MeasureTheory.measurable_uncurry_of_continuous_of_measurable {α : Type u_5} {β : Type u_6} {ι : Type u_7} [TopologicalSpace ι] [TopologicalSpace.MetrizableSpace ι] [MeasurableSpace ι] [SecondCountableTopology ι] [OpensMeasurableSpace ι] {mβ : MeasurableSpace β} [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [BorelSpace β] {m : MeasurableSpace α} {u : ιαβ} (hu_cont : ∀ (x : α), Continuous fun (i : ι) => u i x) (h : ∀ (i : ι), Measurable (u i)) :