# Strongly measurable and finitely strongly measurable functions #

A function `f` is said to be almost everywhere strongly measurable if `f` is almost everywhere equal to a strongly measurable function, i.e. the sequential limit of simple functions. It is said to be almost everywhere finitely strongly measurable with respect to a measure `μ` if the supports of those simple functions have finite measure.

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

## Main definitions #

- `AEStronglyMeasurable f μ`: `f` is almost everywhere equal to a `StronglyMeasurable` function.

- `AEFinStronglyMeasurable f μ`: `f` is almost everywhere equal to a `FinStronglyMeasurable` function.

- `AEFinStronglyMeasurable.sigmaFiniteSet`: a measurable set `t` such that `f =ᵐ[μ.restrict tᶜ] 0` and `μ.restrict t` is sigma-finite.

## Main statements #

- `AEFinStronglyMeasurable.exists_set_sigmaFinite`: there exists a measurable set `t` such that `f =ᵐ[μ.restrict tᶜ] 0` and `μ.restrict t` is sigma-finite.

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

## References #

- [Hytönen, Tuomas, Jan Van Neerven, Mark Veraar, and Lutz Weis. Analysis in Banach spaces. Springer, 2016.][Hytonen_VanNeerven_Veraar_Wies_2016]

source
def MeasureTheory.AEStronglyMeasurable {α : Type u_1} {β : Type u_2} [TopologicalSpace β] [m : MeasurableSpace α] {m₀ : MeasurableSpace α} (f : α → β) (μ : Measure α := by volume_tac) :
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.

One can specify the sigma-algebra according to which simple functions are taken using the `AEStronglyMeasurable[m]` notation in the `MeasureTheory` scope.

Equations

- MeasureTheory.AEStronglyMeasurable f μ = ∃ (g : α → β), MeasureTheory.StronglyMeasurable g ∧ f =ᵐ[μ] g

Instances For

source
def MeasureTheory.«termAEStronglyMeasurable[_]» :
Lean.ParserDescr

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def MeasureTheory.AEFinStronglyMeasurable {α : Type u_1} {β : Type u_2} [TopologicalSpace β] [Zero β] {x✝ : MeasurableSpace α} (f : α → β) (μ : Measure α := by volume_tac) :
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

- MeasureTheory.AEFinStronglyMeasurable f μ = ∃ (g : α → β), MeasureTheory.FinStronglyMeasurable g μ ∧ f =ᵐ[μ] g

Instances For

source
theorem MeasureTheory.FinStronglyMeasurable.aefinStronglyMeasurable {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {μ : Measure α} {f : α → β} [Zero β] [TopologicalSpace β] (hf : FinStronglyMeasurable f μ) :
AEFinStronglyMeasurable f μ
source
theorem MeasureTheory.aefinStronglyMeasurable_zero {α : Type u_5} {β : Type u_6} {x✝ : MeasurableSpace α} (μ : Measure α) [Zero β] [TopologicalSpace β] :
AEFinStronglyMeasurable 0 μ

## Almost everywhere strongly measurable functions #

source
theorem MeasureTheory.StronglyMeasurable.aestronglyMeasurable {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : Measure α} {f : α → β} (hf : StronglyMeasurable f) :
AEStronglyMeasurable f μ
source
theorem MeasureTheory.aestronglyMeasurable_const {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : Measure α} {b : β} :
AEStronglyMeasurable (fun (x : α) => b) μ
source
theorem MeasureTheory.aestronglyMeasurable_one {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : Measure α} [One β] :
AEStronglyMeasurable 1 μ
source
theorem MeasureTheory.aestronglyMeasurable_zero {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : Measure α} [Zero β] :
AEStronglyMeasurable 0 μ
source
@[simp]
theorem MeasureTheory.AEStronglyMeasurable.of_subsingleton_dom {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : Measure α} {f : α → β} [Subsingleton α] :
AEStronglyMeasurable f μ
source
@[simp]
theorem MeasureTheory.AEStronglyMeasurable.of_subsingleton_cod {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : Measure α} {f : α → β} [Subsingleton β] :
AEStronglyMeasurable f μ
source
@[simp]
theorem MeasureTheory.aestronglyMeasurable_zero_measure {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} (f : α → β) :
AEStronglyMeasurable f 0
source
theorem MeasureTheory.SimpleFunc.aestronglyMeasurable {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : Measure α} (f : SimpleFunc α β) :
AEStronglyMeasurable (⇑f) μ
source
theorem MeasureTheory.AEStronglyMeasurable.of_discrete {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : Measure α} {f : α → β} [Countable α] [MeasurableSingletonClass α] :
AEStronglyMeasurable f μ
source
noncomputable def MeasureTheory.AEStronglyMeasurable.mk {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : Measure α} (f : α → β) (hf : AEStronglyMeasurable f μ) :
α → β

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

Equations

- MeasureTheory.AEStronglyMeasurable.mk f hf = Exists.choose hf

Instances For

source
theorem MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : Measure α} {f : α → β} (hf : AEStronglyMeasurable f μ) :
StronglyMeasurable (AEStronglyMeasurable.mk f hf)
source
theorem MeasureTheory.AEStronglyMeasurable.measurable_mk {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : Measure α} {f : α → β} [TopologicalSpace.PseudoMetrizableSpace β] [MeasurableSpace β] [BorelSpace β] (hf : AEStronglyMeasurable f μ) :
Measurable (AEStronglyMeasurable.mk f hf)
source
theorem MeasureTheory.AEStronglyMeasurable.ae_eq_mk {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : Measure α} {f : α → β} (hf : AEStronglyMeasurable f μ) :
f =ᶠ[ae μ] AEStronglyMeasurable.mk f hf
source
theorem MeasureTheory.AEStronglyMeasurable.aemeasurable {α : Type u_1} {m₀ : MeasurableSpace α} {μ : Measure α} {β : Type u_5} [MeasurableSpace β] [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [BorelSpace β] {f : α → β} (hf : AEStronglyMeasurable f μ) :
AEMeasurable f μ
source
theorem MeasureTheory.AEStronglyMeasurable.congr {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : Measure α} {f g : α → β} (hf : AEStronglyMeasurable f μ) (h : f =ᶠ[ae μ] g) :
AEStronglyMeasurable g μ
source
theorem aestronglyMeasurable_congr {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → β} (h : f =ᵐ[μ] g) :
MeasureTheory.AEStronglyMeasurable f μ ↔ MeasureTheory.AEStronglyMeasurable g μ
source
theorem MeasureTheory.AEStronglyMeasurable.mono_measure {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : Measure α} {f : α → β} {ν : Measure α} (hf : AEStronglyMeasurable f μ) (h : ν ≤ μ) :
AEStronglyMeasurable f ν
source
theorem MeasureTheory.AEStronglyMeasurable.mono_ac {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ ν : Measure α} {f : α → β} (h : ν.AbsolutelyContinuous μ) (hμ : AEStronglyMeasurable f μ) :
AEStronglyMeasurable f ν
source
theorem MeasureTheory.AEStronglyMeasurable.mono_set {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : Measure α} {f : α → β} {s t : Set α} (h : s ⊆ t) (ht : AEStronglyMeasurable f (μ.restrict t)) :
AEStronglyMeasurable f (μ.restrict s)
source
theorem MeasureTheory.AEStronglyMeasurable.mono {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : Measure α} {f : α → β} {m' : MeasurableSpace α} (hm : m ≤ m') (hf : AEStronglyMeasurable f μ) :
AEStronglyMeasurable f μ
source
theorem MeasureTheory.AEStronglyMeasurable.of_trim {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : Measure α} {f : α → β} {m₀' : MeasurableSpace α} (hm₀ : m₀' ≤ m₀) (hf : AEStronglyMeasurable f (μ.trim hm₀)) :
AEStronglyMeasurable f μ
source
theorem MeasureTheory.AEStronglyMeasurable.restrict {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : Measure α} {f : α → β} (hfm : AEStronglyMeasurable f μ) {s : Set α} :
AEStronglyMeasurable f (μ.restrict s)
source
theorem MeasureTheory.AEStronglyMeasurable.ae_mem_imp_eq_mk {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : Measure α} {f : α → β} {s : Set α} (h : AEStronglyMeasurable f (μ.restrict s)) :
∀ᵐ (x : α) ∂μ, x ∈ s → f x = AEStronglyMeasurable.mk f h x
source
theorem Continuous.comp_aestronglyMeasurable {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace β] [TopologicalSpace γ] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {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.

source
theorem Continuous.aestronglyMeasurable {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β} [TopologicalSpace α] [OpensMeasurableSpace α] [TopologicalSpace.PseudoMetrizableSpace β] [SecondCountableTopologyEither α β] (hf : Continuous f) :
MeasureTheory.AEStronglyMeasurable f μ

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

source
theorem MeasureTheory.AEStronglyMeasurable.fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace β] [TopologicalSpace γ] {m m₀ : MeasurableSpace α} {μ : Measure α} {f : α → β × γ} (hf : AEStronglyMeasurable f μ) :
AEStronglyMeasurable (fun (x : α) => (f x).1) μ
source
theorem MeasureTheory.AEStronglyMeasurable.snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace β] [TopologicalSpace γ] {m m₀ : MeasurableSpace α} {μ : Measure α} {f : α → β × γ} (hf : AEStronglyMeasurable f μ) :
AEStronglyMeasurable (fun (x : α) => (f x).2) μ
source
theorem MeasureTheory.AEStronglyMeasurable.prodMk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace β] [TopologicalSpace γ] {m m₀ : MeasurableSpace α} {μ : Measure α} {f : α → β} {g : α → γ} (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) :
AEStronglyMeasurable (fun (x : α) => (f x, g x)) μ
source
theorem Continuous.comp_aestronglyMeasurable₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace β] [TopologicalSpace γ] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β' : 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.

source
theorem Measurable.aestronglyMeasurable {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β} [MeasurableSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [SecondCountableTopology β] [OpensMeasurableSpace β] (hf : Measurable f) :
MeasureTheory.AEStronglyMeasurable f μ

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

source
theorem MeasureTheory.AEStronglyMeasurable.of_measurableSpace_le_on {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m : MeasurableSpace α} {f : α → β} {m' m₀ : MeasurableSpace α} {μ : Measure α} [Zero β] (hm : m ≤ m₀) {s : Set α} (hs_m : MeasurableSet s) (hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)) (hf : AEStronglyMeasurable f μ) (hf_zero : f =ᶠ[ae (μ.restrict s ᶜ)] 0) :
AEStronglyMeasurable f μ

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.

source
theorem MeasureTheory.AEStronglyMeasurable.mul {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : Measure α} {f g : α → β} [Mul β] [ContinuousMul β] (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) :
AEStronglyMeasurable (f * g) μ
source
theorem MeasureTheory.AEStronglyMeasurable.add {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : Measure α} {f g : α → β} [Add β] [ContinuousAdd β] (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) :
AEStronglyMeasurable (f + g) μ
source
theorem MeasureTheory.AEStronglyMeasurable.mul_const {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : Measure α} {f : α → β} [Mul β] [ContinuousMul β] (hf : AEStronglyMeasurable f μ) (c : β) :
AEStronglyMeasurable (fun (x : α) => f x * c) μ
source
theorem MeasureTheory.AEStronglyMeasurable.add_const {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : Measure α} {f : α → β} [Add β] [ContinuousAdd β] (hf : AEStronglyMeasurable f μ) (c : β) :
AEStronglyMeasurable (fun (x : α) => f x + c) μ
source
theorem MeasureTheory.AEStronglyMeasurable.const_mul {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : Measure α} {f : α → β} [Mul β] [ContinuousMul β] (hf : AEStronglyMeasurable f μ) (c : β) :
AEStronglyMeasurable (fun (x : α) => c * f x) μ
source
theorem MeasureTheory.AEStronglyMeasurable.const_add {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : Measure α} {f : α → β} [Add β] [ContinuousAdd β] (hf : AEStronglyMeasurable f μ) (c : β) :
AEStronglyMeasurable (fun (x : α) => c + f x) μ
source
theorem MeasureTheory.AEStronglyMeasurable.inv {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : Measure α} {f : α → β} [Inv β] [ContinuousInv β] (hf : AEStronglyMeasurable f μ) :
AEStronglyMeasurable f⁻¹ μ
source
theorem MeasureTheory.AEStronglyMeasurable.neg {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : Measure α} {f : α → β} [Neg β] [ContinuousNeg β] (hf : AEStronglyMeasurable f μ) :
AEStronglyMeasurable (-f) μ
source
theorem MeasureTheory.AEStronglyMeasurable.div {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : Measure α} {f g : α → β} [Group β] [IsTopologicalGroup β] (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) :
AEStronglyMeasurable (f / g) μ
source
theorem MeasureTheory.AEStronglyMeasurable.sub {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : Measure α} {f g : α → β} [AddGroup β] [IsTopologicalAddGroup β] (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) :
AEStronglyMeasurable (f - g) μ
source
theorem MeasureTheory.AEStronglyMeasurable.mul_iff_right {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : Measure α} {f g : α → β} [CommGroup β] [IsTopologicalGroup β] (hf : AEStronglyMeasurable f μ) :
AEStronglyMeasurable (f * g) μ ↔ AEStronglyMeasurable g μ
source
theorem MeasureTheory.AEStronglyMeasurable.add_iff_right {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : Measure α} {f g : α → β} [AddCommGroup β] [IsTopologicalAddGroup β] (hf : AEStronglyMeasurable f μ) :
AEStronglyMeasurable (f + g) μ ↔ AEStronglyMeasurable g μ
source
theorem MeasureTheory.AEStronglyMeasurable.mul_iff_left {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : Measure α} {f g : α → β} [CommGroup β] [IsTopologicalGroup β] (hf : AEStronglyMeasurable f μ) :
AEStronglyMeasurable (g * f) μ ↔ AEStronglyMeasurable g μ
source
theorem MeasureTheory.AEStronglyMeasurable.add_iff_left {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : Measure α} {f g : α → β} [AddCommGroup β] [IsTopologicalAddGroup β] (hf : AEStronglyMeasurable f μ) :
AEStronglyMeasurable (g + f) μ ↔ AEStronglyMeasurable g μ
source
theorem MeasureTheory.AEStronglyMeasurable.smul {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : Measure α} {𝕜 : Type u_5} [TopologicalSpace 𝕜] [SMul 𝕜 β] [ContinuousSMul 𝕜 β] {f : α → 𝕜} {g : α → β} (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) :
AEStronglyMeasurable (fun (x : α) => f x • g x) μ
source
theorem MeasureTheory.AEStronglyMeasurable.vadd {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : Measure α} {𝕜 : Type u_5} [TopologicalSpace 𝕜] [VAdd 𝕜 β] [ContinuousVAdd 𝕜 β] {f : α → 𝕜} {g : α → β} (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) :
AEStronglyMeasurable (fun (x : α) => f x +ᵥ g x) μ
source
theorem MeasureTheory.AEStronglyMeasurable.pow {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : Measure α} {f : α → β} [Monoid β] [ContinuousMul β] (hf : AEStronglyMeasurable f μ) (n : ℕ) :
AEStronglyMeasurable (f ^ n) μ
source
theorem MeasureTheory.AEStronglyMeasurable.const_nsmul {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : Measure α} {f : α → β} [AddMonoid β] [ContinuousAdd β] (hf : AEStronglyMeasurable f μ) (n : ℕ) :
AEStronglyMeasurable (n • f) μ
source
theorem MeasureTheory.AEStronglyMeasurable.const_smul {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : Measure α} {f : α → β} {𝕜 : Type u_5} [SMul 𝕜 β] [ContinuousConstSMul 𝕜 β] (hf : AEStronglyMeasurable f μ) (c : 𝕜) :
AEStronglyMeasurable (c • f) μ
source
theorem MeasureTheory.AEStronglyMeasurable.const_vadd {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : Measure α} {f : α → β} {𝕜 : Type u_5} [VAdd 𝕜 β] [ContinuousConstVAdd 𝕜 β] (hf : AEStronglyMeasurable f μ) (c : 𝕜) :
AEStronglyMeasurable (c +ᵥ f) μ
source
theorem MeasureTheory.AEStronglyMeasurable.const_smul' {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : Measure α} {f : α → β} {𝕜 : Type u_5} [SMul 𝕜 β] [ContinuousConstSMul 𝕜 β] (hf : AEStronglyMeasurable f μ) (c : 𝕜) :
AEStronglyMeasurable (fun (x : α) => c • f x) μ
source
theorem MeasureTheory.AEStronglyMeasurable.const_vadd' {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : Measure α} {f : α → β} {𝕜 : Type u_5} [VAdd 𝕜 β] [ContinuousConstVAdd 𝕜 β] (hf : AEStronglyMeasurable f μ) (c : 𝕜) :
AEStronglyMeasurable (fun (x : α) => c +ᵥ f x) μ
source
theorem MeasureTheory.AEStronglyMeasurable.smul_const {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : Measure α} {𝕜 : Type u_5} [TopologicalSpace 𝕜] [SMul 𝕜 β] [ContinuousSMul 𝕜 β] {f : α → 𝕜} (hf : AEStronglyMeasurable f μ) (c : β) :
AEStronglyMeasurable (fun (x : α) => f x • c) μ
source
theorem MeasureTheory.AEStronglyMeasurable.vadd_const {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : Measure α} {𝕜 : Type u_5} [TopologicalSpace 𝕜] [VAdd 𝕜 β] [ContinuousVAdd 𝕜 β] {f : α → 𝕜} (hf : AEStronglyMeasurable f μ) (c : β) :
AEStronglyMeasurable (fun (x : α) => f x +ᵥ c) μ
source
theorem MeasureTheory.AEStronglyMeasurable.star {α : Type u_1} {m₀ : MeasurableSpace α} {μ : Measure α} {R : Type u_5} [TopologicalSpace R] [Star R] [ContinuousStar R] {f : α → R} (hf : AEStronglyMeasurable f μ) :
AEStronglyMeasurable (star f) μ
source
theorem MeasureTheory.AEStronglyMeasurable.sup {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : Measure α} {f g : α → β} [SemilatticeSup β] [ContinuousSup β] (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) :
AEStronglyMeasurable (f ⊔ g) μ
source
theorem MeasureTheory.AEStronglyMeasurable.inf {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : Measure α} {f g : α → β} [SemilatticeInf β] [ContinuousInf β] (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) :
AEStronglyMeasurable (f ⊓ g) μ

### Big operators: `∏` and `∑` #

source
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 : ∀ f ∈ l, MeasureTheory.AEStronglyMeasurable f μ) :
MeasureTheory.AEStronglyMeasurable l.prod μ
source
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 : ∀ f ∈ l, MeasureTheory.AEStronglyMeasurable f μ) :
MeasureTheory.AEStronglyMeasurable l.sum μ
source
@[deprecated List.aestronglyMeasurable_sum (since := "2025-05-30")]
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 : ∀ f ∈ l, MeasureTheory.AEStronglyMeasurable f μ) :
MeasureTheory.AEStronglyMeasurable l.sum μ

Alias of `List.aestronglyMeasurable_sum`.

source
@[deprecated List.aestronglyMeasurable_prod (since := "2025-05-30")]
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 : ∀ f ∈ l, MeasureTheory.AEStronglyMeasurable f μ) :
MeasureTheory.AEStronglyMeasurable l.prod μ

Alias of `List.aestronglyMeasurable_prod`.

source
theorem List.aestronglyMeasurable_fun_prod {α : Type u_1} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {M : Type u_5} [Monoid M] [TopologicalSpace M] [ContinuousMul M] (l : List (α → M)) (hl : ∀ f ∈ l, MeasureTheory.AEStronglyMeasurable f μ) :
MeasureTheory.AEStronglyMeasurable (fun (x : α) => (map (fun (f : α → M) => f x) l).prod) μ
source
theorem List.aestronglyMeasurable_fun_sum {α : Type u_1} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {M : Type u_5} [AddMonoid M] [TopologicalSpace M] [ContinuousAdd M] (l : List (α → M)) (hl : ∀ f ∈ l, MeasureTheory.AEStronglyMeasurable f μ) :
MeasureTheory.AEStronglyMeasurable (fun (x : α) => (map (fun (f : α → M) => f x) l).sum) μ
source
theorem Multiset.aestronglyMeasurable_prod {α : Type u_1} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {M : Type u_5} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] (l : Multiset (α → M)) (hl : ∀ f ∈ l, MeasureTheory.AEStronglyMeasurable f μ) :
MeasureTheory.AEStronglyMeasurable l.prod μ
source
theorem Multiset.aestronglyMeasurable_sum {α : Type u_1} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {M : Type u_5} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] (l : Multiset (α → M)) (hl : ∀ f ∈ l, MeasureTheory.AEStronglyMeasurable f μ) :
MeasureTheory.AEStronglyMeasurable l.sum μ
source
@[deprecated Multiset.aestronglyMeasurable_sum (since := "2025-05-30")]
theorem Multiset.aestronglyMeasurable_sum' {α : Type u_1} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {M : Type u_5} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] (l : Multiset (α → M)) (hl : ∀ f ∈ l, MeasureTheory.AEStronglyMeasurable f μ) :
MeasureTheory.AEStronglyMeasurable l.sum μ

Alias of `Multiset.aestronglyMeasurable_sum`.

source
@[deprecated Multiset.aestronglyMeasurable_prod (since := "2025-05-30")]
theorem Multiset.aestronglyMeasurable_prod' {α : Type u_1} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {M : Type u_5} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] (l : Multiset (α → M)) (hl : ∀ f ∈ l, MeasureTheory.AEStronglyMeasurable f μ) :
MeasureTheory.AEStronglyMeasurable l.prod μ

Alias of `Multiset.aestronglyMeasurable_prod`.

source
theorem Multiset.aestronglyMeasurable_fun_prod {α : Type u_1} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {M : Type u_5} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] (s : Multiset (α → M)) (hs : ∀ f ∈ s, MeasureTheory.AEStronglyMeasurable f μ) :
MeasureTheory.AEStronglyMeasurable (fun (x : α) => (map (fun (f : α → M) => f x) s).prod) μ
source
theorem Multiset.aestronglyMeasurable_fun_sum {α : Type u_1} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {M : Type u_5} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] (s : Multiset (α → M)) (hs : ∀ f ∈ s, MeasureTheory.AEStronglyMeasurable f μ) :
MeasureTheory.AEStronglyMeasurable (fun (x : α) => (map (fun (f : α → M) => f x) s).sum) μ
source
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 : ∀ i ∈ s, MeasureTheory.AEStronglyMeasurable (f i) μ) :
MeasureTheory.AEStronglyMeasurable (∏ i ∈ s, f i) μ
source
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 : ∀ i ∈ s, MeasureTheory.AEStronglyMeasurable (f i) μ) :
MeasureTheory.AEStronglyMeasurable (∑ i ∈ s, f i) μ
source
@[deprecated Finset.aestronglyMeasurable_sum (since := "2025-05-30")]
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 : ∀ i ∈ s, MeasureTheory.AEStronglyMeasurable (f i) μ) :
MeasureTheory.AEStronglyMeasurable (∑ i ∈ s, f i) μ

Alias of `Finset.aestronglyMeasurable_sum`.

source
@[deprecated Finset.aestronglyMeasurable_prod (since := "2025-05-30")]
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 : ∀ i ∈ s, MeasureTheory.AEStronglyMeasurable (f i) μ) :
MeasureTheory.AEStronglyMeasurable (∏ i ∈ s, f i) μ

Alias of `Finset.aestronglyMeasurable_prod`.

source
theorem Finset.aestronglyMeasurable_fun_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 : ∀ i ∈ s, MeasureTheory.AEStronglyMeasurable (f i) μ) :
MeasureTheory.AEStronglyMeasurable (fun (a : α) => ∏ i ∈ s, f i a) μ
source
theorem Finset.aestronglyMeasurable_fun_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 : ∀ i ∈ s, MeasureTheory.AEStronglyMeasurable (f i) μ) :
MeasureTheory.AEStronglyMeasurable (fun (a : α) => ∑ i ∈ s, f i a) μ
source
theorem AEMeasurable.aestronglyMeasurable {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β} [MeasurableSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [OpensMeasurableSpace β] [SecondCountableTopology β] (hf : AEMeasurable f μ) :
MeasureTheory.AEStronglyMeasurable f μ

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

source
theorem aestronglyMeasurable_id {α : Type u_5} [TopologicalSpace α] [TopologicalSpace.PseudoMetrizableSpace α] {x✝ : MeasurableSpace α} [OpensMeasurableSpace α] [SecondCountableTopology α] {μ : MeasureTheory.Measure α} :
MeasureTheory.AEStronglyMeasurable id μ
source
theorem aestronglyMeasurable_iff_aemeasurable {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β} [MeasurableSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [BorelSpace β] [SecondCountableTopology β] :
MeasureTheory.AEStronglyMeasurable f μ ↔ AEMeasurable f μ

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

source
theorem MeasureTheory.AEStronglyMeasurable.dist {α : Type u_1} {m₀ : MeasurableSpace α} {μ : Measure α} {β : Type u_5} [PseudoMetricSpace β] {f g : α → β} (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) :
AEStronglyMeasurable (fun (x : α) => dist (f x) (g x)) μ
source
theorem MeasureTheory.AEStronglyMeasurable.norm {α : Type u_1} {m₀ : MeasurableSpace α} {μ : Measure α} {β : Type u_5} [SeminormedAddCommGroup β] {f : α → β} (hf : AEStronglyMeasurable f μ) :
AEStronglyMeasurable (fun (x : α) => ‖f x‖) μ
source
theorem MeasureTheory.AEStronglyMeasurable.nnnorm {α : Type u_1} {m₀ : MeasurableSpace α} {μ : Measure α} {β : Type u_5} [SeminormedAddCommGroup β] {f : α → β} (hf : AEStronglyMeasurable f μ) :
AEStronglyMeasurable (fun (x : α) => ‖f x‖₊) μ
source
theorem MeasureTheory.AEStronglyMeasurable.enorm {α : Type u_1} {m₀ : MeasurableSpace α} {μ : Measure α} {β : Type u_5} [TopologicalSpace β] [ContinuousENorm β] {f : α → β} (hf : AEStronglyMeasurable f μ) :
AEMeasurable (fun (x : α) => ‖f x‖ₑ) μ

The `enorm` of a strongly a.e. measurable function is a.e. measurable.

Note that unlike `AEStronglyMeasurable.norm` and `AEStronglyMeasurable.nnnorm`, this lemma proves a.e. measurability, not a.e. strong measurability. This is an intentional decision: for functions taking values in `ℝ≥0∞`, a.e. measurability is much more useful than a.e. strong measurability.

source
theorem MeasureTheory.AEStronglyMeasurable.edist {α : Type u_1} {m₀ : MeasurableSpace α} {μ : Measure α} {β : Type u_5} [PseudoMetricSpace β] {f g : α → β} (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) :
AEMeasurable (fun (a : α) => edist (f a) (g a)) μ

Given a.e. strongly measurable functions `f` and `g`, `edist f g` is measurable.

Note that this lemma proves a.e. measurability, not a.e. strong measurability. This is an intentional decision: for functions taking values in ℝ≥0∞, a.e. measurability is much more useful than a.e. strong measurability.

source
theorem MeasureTheory.AEStronglyMeasurable.real_toNNReal {α : Type u_1} {m₀ : MeasurableSpace α} {μ : Measure α} {f : α → ℝ} (hf : AEStronglyMeasurable f μ) :
AEStronglyMeasurable (fun (x : α) => (f x).toNNReal) μ
source
theorem aestronglyMeasurable_indicator_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β} [Zero β] {s : Set α} (hs : MeasurableSet s) :
MeasureTheory.AEStronglyMeasurable (s.indicator f) μ ↔ MeasureTheory.AEStronglyMeasurable f (μ.restrict s)
source
theorem aestronglyMeasurable_indicator_iff₀ {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β} [Zero β] {s : Set α} (hs : MeasureTheory.NullMeasurableSet s μ) :
MeasureTheory.AEStronglyMeasurable (s.indicator f) μ ↔ MeasureTheory.AEStronglyMeasurable f (μ.restrict s)
source
theorem MeasureTheory.AEStronglyMeasurable.indicator {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : Measure α} {f : α → β} [Zero β] (hfm : AEStronglyMeasurable f μ) {s : Set α} (hs : MeasurableSet s) :
AEStronglyMeasurable (s.indicator f) μ
source
theorem MeasureTheory.AEStronglyMeasurable.indicator₀ {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : Measure α} {f : α → β} [Zero β] (hfm : AEStronglyMeasurable f μ) {s : Set α} (hs : NullMeasurableSet s μ) :
AEStronglyMeasurable (s.indicator f) μ
source
theorem MeasureTheory.AEStronglyMeasurable.nullMeasurableSet_eq_fun {α : Type u_1} {m₀ : MeasurableSpace α} {μ : Measure α} {E : Type u_5} [TopologicalSpace E] [TopologicalSpace.MetrizableSpace E] {f g : α → E} (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) :
NullMeasurableSet {x : α | f x = g x} μ
source
theorem MeasureTheory.AEStronglyMeasurable.nullMeasurableSet_mulSupport {α : Type u_1} {m₀ : MeasurableSpace α} {μ : Measure α} {E : Type u_5} [TopologicalSpace E] [TopologicalSpace.MetrizableSpace E] [One E] {f : α → E} (hf : AEStronglyMeasurable f μ) :
NullMeasurableSet (Function.mulSupport f) μ
source
theorem MeasureTheory.AEStronglyMeasurable.nullMeasurableSet_support {α : Type u_1} {m₀ : MeasurableSpace α} {μ : Measure α} {E : Type u_5} [TopologicalSpace E] [TopologicalSpace.MetrizableSpace E] [Zero E] {f : α → E} (hf : AEStronglyMeasurable f μ) :
NullMeasurableSet (Function.support f) μ
source
theorem MeasureTheory.AEStronglyMeasurable.nullMeasurableSet_lt {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : Measure α} [Preorder β] [OrderClosedTopology β] [TopologicalSpace.PseudoMetrizableSpace β] {f g : α → β} (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) :
NullMeasurableSet {a : α | f a < g a} μ
source
theorem MeasureTheory.AEStronglyMeasurable.nullMeasurableSet_le {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : Measure α} [Preorder β] [OrderClosedTopology β] [TopologicalSpace.PseudoMetrizableSpace β] {f g : α → β} (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) :
NullMeasurableSet {a : α | f a ≤ g a} μ
source
theorem aestronglyMeasurable_of_aestronglyMeasurable_trim {β : Type u_2} [TopologicalSpace β] {α : Type u_5} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) {f : α → β} (hf : MeasureTheory.AEStronglyMeasurable f (μ.trim hm)) :
MeasureTheory.AEStronglyMeasurable f μ
source
theorem MeasureTheory.AEStronglyMeasurable.comp_aemeasurable {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {g : α → β} {γ : Type u_5} {x✝ : MeasurableSpace γ} {x✝¹ : MeasurableSpace α} {f : γ → α} {μ : Measure γ} (hg : AEStronglyMeasurable g (Measure.map f μ)) (hf : AEMeasurable f μ) :
AEStronglyMeasurable (g ∘ f) μ
source
theorem MeasureTheory.AEStronglyMeasurable.comp_measurable {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {g : α → β} {γ : Type u_5} {x✝ : MeasurableSpace γ} {x✝¹ : MeasurableSpace α} {f : γ → α} {μ : Measure γ} (hg : AEStronglyMeasurable g (Measure.map f μ)) (hf : Measurable f) :
AEStronglyMeasurable (g ∘ f) μ
source
theorem MeasureTheory.AEStronglyMeasurable.comp_quasiMeasurePreserving {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {g : α → β} {γ : Type u_5} {x✝ : MeasurableSpace γ} {x✝¹ : MeasurableSpace α} {f : γ → α} {μ : Measure γ} {ν : Measure α} (hg : AEStronglyMeasurable g ν) (hf : Measure.QuasiMeasurePreserving f μ ν) :
AEStronglyMeasurable (g ∘ f) μ
source
theorem MeasureTheory.AEStronglyMeasurable.isSeparable_ae_range {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : Measure α} {f : α → β} (hf : AEStronglyMeasurable f μ) :
∃ (t : Set β), TopologicalSpace.IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t
source
theorem aestronglyMeasurable_iff_aemeasurable_separable {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β} [TopologicalSpace.PseudoMetrizableSpace β] [MeasurableSpace β] [BorelSpace β] :
MeasureTheory.AEStronglyMeasurable f μ ↔ AEMeasurable 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.

source
theorem aestronglyMeasurable_iff_nullMeasurable_separable {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β} [TopologicalSpace.PseudoMetrizableSpace β] [MeasurableSpace β] [BorelSpace β] :
MeasureTheory.AEStronglyMeasurable f μ ↔ MeasureTheory.NullMeasurable f μ ∧ ∃ (t : Set β), TopologicalSpace.IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t
source
theorem MeasurableEmbedding.aestronglyMeasurable_map_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {γ : Type u_5} {mγ : MeasurableSpace γ} {mα : MeasurableSpace α} {f : γ → α} {μ : MeasureTheory.Measure γ} (hf : MeasurableEmbedding f) {g : α → β} :
MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ) ↔ MeasureTheory.AEStronglyMeasurable (g ∘ f) μ
source
theorem Topology.IsEmbedding.aestronglyMeasurable_comp_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace β] [TopologicalSpace γ] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace.PseudoMetrizableSpace β] [TopologicalSpace.PseudoMetrizableSpace γ] {g : β → γ} {f : α → β} (hg : IsEmbedding g) :
MeasureTheory.AEStronglyMeasurable (fun (x : α) => g (f x)) μ ↔ MeasureTheory.AEStronglyMeasurable f μ
source
theorem aestronglyMeasurable_of_tendsto_ae {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : 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))) :
MeasureTheory.AEStronglyMeasurable g μ

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

source
theorem exists_stronglyMeasurable_limit_of_tendsto_ae {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} [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.

source
theorem MeasureTheory.AEStronglyMeasurable.exists_stronglyMeasurable_range_subset {α : Type u_5} {β : Type u_6} [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [mb : MeasurableSpace β] [BorelSpace β] [m : MeasurableSpace α] {μ : Measure α} {f : α → β} (hf : AEStronglyMeasurable f μ) {s : Set β} (hs : MeasurableSet s) (h_nonempty : s.Nonempty) (h_mem : ∀ᵐ (x : α) ∂μ, f x ∈ s) :
∃ (g : α → β), StronglyMeasurable g ∧ (∀ (x : α), g x ∈ s) ∧ f =ᶠ[ae μ] g

If `f` is almost everywhere strongly measurable and its range is almost everywhere contained in a nonempty measurable set `s`, then there is a strongly measurable representative `g` of `f` whose range is contained in `s`.

source
theorem MeasureTheory.AEStronglyMeasurable.piecewise {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : Measure α} {f g : α → β} {s : Set α} [DecidablePred fun (x : α) => x ∈ s] (hs : MeasurableSet s) (hf : AEStronglyMeasurable f (μ.restrict s)) (hg : AEStronglyMeasurable g (μ.restrict s ᶜ)) :
AEStronglyMeasurable (s.piecewise f g) μ
source
theorem MeasureTheory.AEStronglyMeasurable.sum_measure {α : Type u_1} {β : Type u_2} {ι : Type u_4} [Countable ι] [TopologicalSpace β] {f : α → β} [TopologicalSpace.PseudoMetrizableSpace β] {m : MeasurableSpace α} {μ : ι → Measure α} (h : ∀ (i : ι), AEStronglyMeasurable f (μ i)) :
AEStronglyMeasurable f (Measure.sum μ)
source
@[simp]
theorem aestronglyMeasurable_sum_measure_iff {α : Type u_1} {β : Type u_2} {ι : Type u_4} [Countable ι] [TopologicalSpace β] {f : α → β} [TopologicalSpace.PseudoMetrizableSpace β] {_m : MeasurableSpace α} {μ : ι → MeasureTheory.Measure α} :
MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.sum μ) ↔ ∀ (i : ι), MeasureTheory.AEStronglyMeasurable f (μ i)
source
@[simp]
theorem aestronglyMeasurable_add_measure_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β} [TopologicalSpace.PseudoMetrizableSpace β] {ν : MeasureTheory.Measure α} :
MeasureTheory.AEStronglyMeasurable f (μ + ν) ↔ MeasureTheory.AEStronglyMeasurable f μ ∧ MeasureTheory.AEStronglyMeasurable f ν
source
theorem MeasureTheory.AEStronglyMeasurable.add_measure {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : Measure α} [TopologicalSpace.PseudoMetrizableSpace β] {ν : Measure α} {f : α → β} (hμ : AEStronglyMeasurable f μ) (hν : AEStronglyMeasurable f ν) :
AEStronglyMeasurable f (μ + ν)
source
theorem MeasureTheory.AEStronglyMeasurable.iUnion {α : Type u_1} {β : Type u_2} {ι : Type u_4} [Countable ι] [TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : Measure α} {f : α → β} [TopologicalSpace.PseudoMetrizableSpace β] {s : ι → Set α} (h : ∀ (i : ι), AEStronglyMeasurable f (μ.restrict (s i))) :
AEStronglyMeasurable f (μ.restrict (⋃ (i : ι), s i))
source
@[simp]
theorem aestronglyMeasurable_iUnion_iff {α : Type u_1} {β : Type u_2} {ι : Type u_4} [Countable ι] [TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β} [TopologicalSpace.PseudoMetrizableSpace β] {s : ι → Set α} :
MeasureTheory.AEStronglyMeasurable f (μ.restrict (⋃ (i : ι), s i)) ↔ ∀ (i : ι), MeasureTheory.AEStronglyMeasurable f (μ.restrict (s i))
source
@[simp]
theorem aestronglyMeasurable_union_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β} [TopologicalSpace.PseudoMetrizableSpace β] {s t : Set α} :
MeasureTheory.AEStronglyMeasurable f (μ.restrict (s ∪ t)) ↔ MeasureTheory.AEStronglyMeasurable f (μ.restrict s) ∧ MeasureTheory.AEStronglyMeasurable f (μ.restrict t)
source
theorem MeasureTheory.AEStronglyMeasurable.aestronglyMeasurable_uIoc_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : Measure α} [LinearOrder α] [TopologicalSpace.PseudoMetrizableSpace β] {f : α → β} {a b : α} :
AEStronglyMeasurable f (μ.restrict (Set.uIoc a b)) ↔ AEStronglyMeasurable f (μ.restrict (Set.Ioc a b)) ∧ AEStronglyMeasurable f (μ.restrict (Set.Ioc b a))
source
theorem MeasureTheory.AEStronglyMeasurable.smul_measure {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : Measure α} {f : α → β} {R : Type u_5} [SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] (h : AEStronglyMeasurable f μ) (c : R) :
AEStronglyMeasurable f (c • μ)
source
theorem aestronglyMeasurable_const_smul_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β} {G : Type u_6} [Group G] [MulAction G β] [ContinuousConstSMul G β] (c : G) :
MeasureTheory.AEStronglyMeasurable (fun (x : α) => c • f x) μ ↔ MeasureTheory.AEStronglyMeasurable f μ
source
theorem IsUnit.aestronglyMeasurable_const_smul_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β} {M : Type u_5} [Monoid M] [MulAction M β] [ContinuousConstSMul M β] {c : M} (hc : IsUnit c) :
MeasureTheory.AEStronglyMeasurable (fun (x : α) => c • f x) μ ↔ MeasureTheory.AEStronglyMeasurable f μ
source
theorem aestronglyMeasurable_const_smul_iff₀ {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β} {G₀ : Type u_7} [GroupWithZero G₀] [MulAction G₀ β] [ContinuousConstSMul G₀ β] {c : G₀} (hc : c ≠ 0) :
MeasureTheory.AEStronglyMeasurable (fun (x : α) => c • f x) μ ↔ MeasureTheory.AEStronglyMeasurable f μ

## Almost everywhere finitely strongly measurable functions #

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

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

Equations

- MeasureTheory.AEFinStronglyMeasurable.mk f hf = Exists.choose hf

Instances For

source
theorem MeasureTheory.AEFinStronglyMeasurable.finStronglyMeasurable_mk {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace β] {f : α → β} [Zero β] (hf : AEFinStronglyMeasurable f μ) :
FinStronglyMeasurable (AEFinStronglyMeasurable.mk f hf) μ
source
theorem MeasureTheory.AEFinStronglyMeasurable.ae_eq_mk {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace β] {f : α → β} [Zero β] (hf : AEFinStronglyMeasurable f μ) :
f =ᶠ[ae μ] AEFinStronglyMeasurable.mk f hf
source
theorem MeasureTheory.AEFinStronglyMeasurable.aemeasurable {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_5} [Zero β] [MeasurableSpace β] [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [BorelSpace β] {f : α → β} (hf : AEFinStronglyMeasurable f μ) :
AEMeasurable f μ
source
theorem MeasureTheory.AEFinStronglyMeasurable.mul {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace β] {f g : α → β} [MulZeroClass β] [ContinuousMul β] (hf : AEFinStronglyMeasurable f μ) (hg : AEFinStronglyMeasurable g μ) :
AEFinStronglyMeasurable (f * g) μ
source
theorem MeasureTheory.AEFinStronglyMeasurable.add {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace β] {f g : α → β} [AddZeroClass β] [ContinuousAdd β] (hf : AEFinStronglyMeasurable f μ) (hg : AEFinStronglyMeasurable g μ) :
AEFinStronglyMeasurable (f + g) μ
source
theorem MeasureTheory.AEFinStronglyMeasurable.neg {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace β] {f : α → β} [SubtractionMonoid β] [ContinuousNeg β] (hf : AEFinStronglyMeasurable f μ) :
AEFinStronglyMeasurable (-f) μ
source
theorem MeasureTheory.AEFinStronglyMeasurable.sub {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace β] {f g : α → β} [SubtractionMonoid β] [ContinuousSub β] (hf : AEFinStronglyMeasurable f μ) (hg : AEFinStronglyMeasurable g μ) :
AEFinStronglyMeasurable (f - g) μ
source
theorem MeasureTheory.AEFinStronglyMeasurable.const_smul {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace β] {f : α → β} {𝕜 : Type u_5} [TopologicalSpace 𝕜] [Zero β] [SMulZeroClass 𝕜 β] [ContinuousSMul 𝕜 β] (hf : AEFinStronglyMeasurable f μ) (c : 𝕜) :
AEFinStronglyMeasurable (c • f) μ
source
theorem MeasureTheory.AEFinStronglyMeasurable.sup {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace β] {f g : α → β} [Zero β] [SemilatticeSup β] [ContinuousSup β] (hf : AEFinStronglyMeasurable f μ) (hg : AEFinStronglyMeasurable g μ) :
AEFinStronglyMeasurable (f ⊔ g) μ
source
theorem MeasureTheory.AEFinStronglyMeasurable.inf {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace β] {f g : α → β} [Zero β] [SemilatticeInf β] [ContinuousInf β] (hf : AEFinStronglyMeasurable f μ) (hg : AEFinStronglyMeasurable g μ) :
AEFinStronglyMeasurable (f ⊓ g) μ
source
theorem MeasureTheory.AEFinStronglyMeasurable.exists_set_sigmaFinite {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace β] {f : α → β} [Zero β] [T2Space β] (hf : AEFinStronglyMeasurable f μ) :
∃ (t : Set α), MeasurableSet t ∧ f =ᶠ[ae (μ.restrict t ᶜ)] 0 ∧ SigmaFinite (μ.restrict t)
source
def MeasureTheory.AEFinStronglyMeasurable.sigmaFiniteSet {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace β] {f : α → β} [Zero β] [T2Space β] (hf : AEFinStronglyMeasurable f μ) :
Set α

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

Equations

- hf.sigmaFiniteSet = ⋯.choose

Instances For

source
theorem MeasureTheory.AEFinStronglyMeasurable.measurableSet {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace β] {f : α → β} [Zero β] [T2Space β] (hf : AEFinStronglyMeasurable f μ) :
MeasurableSet hf.sigmaFiniteSet
source
theorem MeasureTheory.AEFinStronglyMeasurable.ae_eq_zero_compl {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace β] {f : α → β} [Zero β] [T2Space β] (hf : AEFinStronglyMeasurable f μ) :
f =ᶠ[ae (μ.restrict hf.sigmaFiniteSet ᶜ)] 0
source
instance MeasureTheory.AEFinStronglyMeasurable.sigmaFinite_restrict {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace β] {f : α → β} [Zero β] [T2Space β] (hf : AEFinStronglyMeasurable f μ) :
SigmaFinite (μ.restrict hf.sigmaFiniteSet)
source
theorem MeasureTheory.aefinStronglyMeasurable_iff_aemeasurable {α : Type u_1} {G : Type u_5} [SeminormedAddCommGroup G] [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G] {f : α → G} {_m0 : MeasurableSpace α} (μ : Measure α) [SigmaFinite μ] :
AEFinStronglyMeasurable f μ ↔ AEMeasurable f μ

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

source
theorem MeasureTheory.aefinStronglyMeasurable_of_aemeasurable {α : Type u_1} {G : Type u_5} [SeminormedAddCommGroup G] [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G] {f : α → G} {_m0 : MeasurableSpace α} (μ : Measure α) [SigmaFinite μ] (hf : AEMeasurable f μ) :
AEFinStronglyMeasurable f μ

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