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 μ:fis almost everywhere equal to aStronglyMeasurablefunction.AEFinStronglyMeasurable f μ:fis almost everywhere equal to aFinStronglyMeasurablefunction.AEFinStronglyMeasurable.sigmaFiniteSet: a measurable settsuch thatf =ᵐ[μ.restrict tᶜ] 0andμ.restrict tis sigma-finite.
Main statements #
AEFinStronglyMeasurable.exists_set_sigmaFinite: there exists a measurable settsuch thatf =ᵐ[μ.restrict tᶜ] 0andμ.restrict tis 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]
def
MeasureTheory.AEStronglyMeasurable
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
[m : MeasurableSpace α]
{m₀ : MeasurableSpace α}
(f : α → β)
(μ : Measure α := by volume_tac)
:
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
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
def
MeasureTheory.AEFinStronglyMeasurable
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
[Zero β]
{x✝ : MeasurableSpace α}
(f : α → β)
(μ : Measure α := by volume_tac)
:
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
theorem
MeasureTheory.FinStronglyMeasurable.aefinStronglyMeasurable
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{f : α → β}
[Zero β]
[TopologicalSpace β]
(hf : FinStronglyMeasurable f μ)
:
theorem
MeasureTheory.aefinStronglyMeasurable_zero
{α : Type u_5}
{β : Type u_6}
{x✝ : MeasurableSpace α}
(μ : Measure α)
[Zero β]
[TopologicalSpace β]
:
Almost everywhere strongly measurable functions #
theorem
MeasureTheory.StronglyMeasurable.aestronglyMeasurable
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{f : α → β}
(hf : StronglyMeasurable f)
:
theorem
MeasureTheory.aestronglyMeasurable_const
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{b : β}
:
AEStronglyMeasurable (fun (x : α) => b) μ
theorem
MeasureTheory.aestronglyMeasurable_one
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
{m m₀ : MeasurableSpace α}
{μ : Measure α}
[One β]
:
theorem
MeasureTheory.aestronglyMeasurable_zero
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
{m m₀ : MeasurableSpace α}
{μ : Measure α}
[Zero β]
:
@[simp]
theorem
MeasureTheory.AEStronglyMeasurable.of_subsingleton_dom
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{f : α → β}
[Subsingleton α]
:
@[simp]
theorem
MeasureTheory.AEStronglyMeasurable.of_subsingleton_cod
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{f : α → β}
[Subsingleton β]
:
@[deprecated MeasureTheory.AEStronglyMeasurable.of_subsingleton_cod (since := "2025-04-09")]
theorem
MeasureTheory.Subsingleton.aestronglyMeasurable
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
{m₀ : MeasurableSpace α}
{μ : Measure α}
[Subsingleton β]
(f : α → β)
:
@[deprecated MeasureTheory.AEStronglyMeasurable.of_subsingleton_dom (since := "2025-04-09")]
theorem
MeasureTheory.Subsingleton.aestronglyMeasurable'
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
{m₀ : MeasurableSpace α}
{μ : Measure α}
[Subsingleton α]
(f : α → β)
:
@[simp]
theorem
MeasureTheory.aestronglyMeasurable_zero_measure
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
{m m₀ : MeasurableSpace α}
(f : α → β)
:
theorem
MeasureTheory.SimpleFunc.aestronglyMeasurable
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
{m₀ : MeasurableSpace α}
{μ : Measure α}
(f : SimpleFunc α β)
:
AEStronglyMeasurable (⇑f) μ
theorem
MeasureTheory.AEStronglyMeasurable.of_discrete
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
{m₀ : MeasurableSpace α}
{μ : Measure α}
{f : α → β}
[Countable α]
[MeasurableSingletonClass α]
:
@[deprecated MeasureTheory.AEStronglyMeasurable.of_discrete (since := "2025-04-09")]
theorem
MeasureTheory.AEStronglyMeasurable.of_finite
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
{m₀ : MeasurableSpace α}
{μ : Measure α}
{f : α → β}
[DiscreteMeasurableSpace α]
[Finite α]
:
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
Instances For
theorem
MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{f : α → β}
(hf : AEStronglyMeasurable f μ)
:
theorem
MeasureTheory.AEStronglyMeasurable.measurable_mk
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{f : α → β}
[TopologicalSpace.PseudoMetrizableSpace β]
[MeasurableSpace β]
[BorelSpace β]
(hf : AEStronglyMeasurable f μ)
:
theorem
MeasureTheory.AEStronglyMeasurable.ae_eq_mk
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{f : α → β}
(hf : AEStronglyMeasurable f μ)
:
theorem
MeasureTheory.AEStronglyMeasurable.aemeasurable
{α : Type u_1}
{m₀ : MeasurableSpace α}
{μ : Measure α}
{β : Type u_5}
[MeasurableSpace β]
[TopologicalSpace β]
[TopologicalSpace.PseudoMetrizableSpace β]
[BorelSpace β]
{f : α → β}
(hf : AEStronglyMeasurable f μ)
:
AEMeasurable f μ
theorem
MeasureTheory.AEStronglyMeasurable.congr
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{f g : α → β}
(hf : AEStronglyMeasurable f μ)
(h : f =ᶠ[ae μ] g)
:
theorem
aestronglyMeasurable_congr
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
{m m₀ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f g : α → β}
(h : f =ᵐ[μ] g)
:
theorem
MeasureTheory.AEStronglyMeasurable.mono_measure
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{f : α → β}
{ν : Measure α}
(hf : AEStronglyMeasurable f μ)
(h : ν ≤ μ)
:
theorem
MeasureTheory.AEStronglyMeasurable.mono_ac
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
{m m₀ : MeasurableSpace α}
{μ ν : Measure α}
{f : α → β}
(h : ν.AbsolutelyContinuous μ)
(hμ : AEStronglyMeasurable f μ)
:
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)
theorem
MeasureTheory.AEStronglyMeasurable.mono
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{f : α → β}
{m' : MeasurableSpace α}
(hm : m ≤ m')
(hf : AEStronglyMeasurable f μ)
:
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₀))
:
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)
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))
:
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.
theorem
Continuous.aestronglyMeasurable
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
{m₀ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → β}
[TopologicalSpace α]
[OpensMeasurableSpace α]
[TopologicalSpace.PseudoMetrizableSpace β]
[SecondCountableTopologyEither α β]
(hf : Continuous f)
:
A continuous function from α to β is ae strongly measurable when one of the two spaces is
second countable.
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) μ
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) μ
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)) μ
@[deprecated MeasureTheory.AEStronglyMeasurable.prodMk (since := "2025-03-05")]
theorem
MeasureTheory.AEStronglyMeasurable.prod_mk
{α : 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)) μ
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.
theorem
Measurable.aestronglyMeasurable
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
{m m₀ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → β}
[MeasurableSpace β]
[TopologicalSpace.PseudoMetrizableSpace β]
[SecondCountableTopology β]
[OpensMeasurableSpace β]
(hf : Measurable f)
:
In a space with second countable topology, measurable implies ae strongly measurable.
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)
:
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.
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) μ
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) μ
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) μ
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) μ
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) μ
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) μ
theorem
MeasureTheory.AEStronglyMeasurable.inv
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{f : α → β}
[Inv β]
[ContinuousInv β]
(hf : AEStronglyMeasurable f μ)
:
theorem
MeasureTheory.AEStronglyMeasurable.neg
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{f : α → β}
[Neg β]
[ContinuousNeg β]
(hf : AEStronglyMeasurable f μ)
:
AEStronglyMeasurable (-f) μ
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) μ
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) μ
theorem
MeasureTheory.AEStronglyMeasurable.mul_iff_right
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{f g : α → β}
[CommGroup β]
[IsTopologicalGroup β]
(hf : AEStronglyMeasurable f μ)
:
theorem
MeasureTheory.AEStronglyMeasurable.add_iff_right
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{f g : α → β}
[AddCommGroup β]
[IsTopologicalAddGroup β]
(hf : AEStronglyMeasurable f μ)
:
theorem
MeasureTheory.AEStronglyMeasurable.mul_iff_left
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{f g : α → β}
[CommGroup β]
[IsTopologicalGroup β]
(hf : AEStronglyMeasurable f μ)
:
theorem
MeasureTheory.AEStronglyMeasurable.add_iff_left
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{f g : α → β}
[AddCommGroup β]
[IsTopologicalAddGroup β]
(hf : AEStronglyMeasurable f μ)
:
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) μ
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) μ
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) μ
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) μ
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) μ
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) μ
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) μ
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) μ
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) μ
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) μ
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) μ
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 ∑ #
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 μ)
:
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 μ)
:
@[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 μ)
:
Alias of List.aestronglyMeasurable_sum.
@[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 μ)
:
Alias of List.aestronglyMeasurable_prod.
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) μ
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) μ
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 μ)
:
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 μ)
:
@[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 μ)
:
Alias of Multiset.aestronglyMeasurable_sum.
@[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 μ)
:
Alias of Multiset.aestronglyMeasurable_prod.
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) μ
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) μ
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) μ
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) μ
@[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.
@[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.
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) μ
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) μ
theorem
AEMeasurable.aestronglyMeasurable
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
{m₀ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → β}
[MeasurableSpace β]
[TopologicalSpace.PseudoMetrizableSpace β]
[OpensMeasurableSpace β]
[SecondCountableTopology β]
(hf : AEMeasurable f μ)
:
In a space with second countable topology, measurable implies strongly measurable.
theorem
aestronglyMeasurable_id
{α : Type u_5}
[TopologicalSpace α]
[TopologicalSpace.PseudoMetrizableSpace α]
{x✝ : MeasurableSpace α}
[OpensMeasurableSpace α]
[SecondCountableTopology α]
{μ : MeasureTheory.Measure α}
:
theorem
aestronglyMeasurable_iff_aemeasurable
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
{m₀ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → β}
[MeasurableSpace β]
[TopologicalSpace.PseudoMetrizableSpace β]
[BorelSpace β]
[SecondCountableTopology β]
:
In a space with second countable topology, strongly measurable and measurable are equivalent.
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)) μ
theorem
MeasureTheory.AEStronglyMeasurable.norm
{α : Type u_1}
{m₀ : MeasurableSpace α}
{μ : Measure α}
{β : Type u_5}
[SeminormedAddCommGroup β]
{f : α → β}
(hf : AEStronglyMeasurable f μ)
:
AEStronglyMeasurable (fun (x : α) => ‖f x‖) μ
theorem
MeasureTheory.AEStronglyMeasurable.nnnorm
{α : Type u_1}
{m₀ : MeasurableSpace α}
{μ : Measure α}
{β : Type u_5}
[SeminormedAddCommGroup β]
{f : α → β}
(hf : AEStronglyMeasurable f μ)
:
AEStronglyMeasurable (fun (x : α) => ‖f x‖₊) μ
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.
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.
theorem
MeasureTheory.AEStronglyMeasurable.real_toNNReal
{α : Type u_1}
{m₀ : MeasurableSpace α}
{μ : Measure α}
{f : α → ℝ}
(hf : AEStronglyMeasurable f μ)
:
AEStronglyMeasurable (fun (x : α) => (f x).toNNReal) μ
theorem
aestronglyMeasurable_indicator_iff
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
{m₀ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → β}
[Zero β]
{s : Set α}
(hs : MeasurableSet s)
:
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) μ
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 μ)
:
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 μ)
:
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 μ)
:
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 μ)
:
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 μ)
:
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))
:
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) μ
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) μ
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) μ
theorem
MeasureTheory.AEStronglyMeasurable.isSeparable_ae_range
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
{m₀ : MeasurableSpace α}
{μ : Measure α}
{f : α → β}
(hf : AEStronglyMeasurable f μ)
:
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.
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
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 : α → β}
:
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 μ
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)))
:
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}
[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.
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)
:
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.
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) μ
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))
:
@[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)
@[simp]
theorem
aestronglyMeasurable_add_measure_iff
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
{m₀ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → β}
[TopologicalSpace.PseudoMetrizableSpace β]
{ν : MeasureTheory.Measure α}
:
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 (μ + ν)
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))
@[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))
@[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)
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))
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 • μ)
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 μ
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 μ
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 #
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
Instances For
theorem
MeasureTheory.AEFinStronglyMeasurable.finStronglyMeasurable_mk
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace β]
{f : α → β}
[Zero β]
(hf : AEFinStronglyMeasurable f μ)
:
theorem
MeasureTheory.AEFinStronglyMeasurable.ae_eq_mk
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace β]
{f : α → β}
[Zero β]
(hf : AEFinStronglyMeasurable f μ)
:
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 μ
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) μ
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) μ
theorem
MeasureTheory.AEFinStronglyMeasurable.neg
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace β]
{f : α → β}
[SubtractionMonoid β]
[ContinuousNeg β]
(hf : AEFinStronglyMeasurable f μ)
:
AEFinStronglyMeasurable (-f) μ
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) μ
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) μ
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) μ
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) μ
theorem
MeasureTheory.AEFinStronglyMeasurable.exists_set_sigmaFinite
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace β]
{f : α → β}
[Zero β]
[T2Space β]
(hf : AEFinStronglyMeasurable f μ)
:
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
theorem
MeasureTheory.AEFinStronglyMeasurable.measurableSet
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace β]
{f : α → β}
[Zero β]
[T2Space β]
(hf : AEFinStronglyMeasurable f μ)
:
theorem
MeasureTheory.AEFinStronglyMeasurable.ae_eq_zero_compl
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace β]
{f : α → β}
[Zero β]
[T2Space β]
(hf : AEFinStronglyMeasurable f μ)
:
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)
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 μ]
:
In a space with second countable topology and a sigma-finite measure,
AEFinStronglyMeasurable and AEMeasurable are equivalent.
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 μ)
:
In a space with second countable topology and a sigma-finite measure,
an AEMeasurable function is AEFinStronglyMeasurable.