Strongly measurable and finitely strongly measurable functions

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

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

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

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

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

Main definitions

• StronglyMeasurable f: f : α → β is the limit of a sequence fs : ℕ → SimpleFunc α β.

• FinStronglyMeasurable f μ: f : α → β is the limit of a sequence fs : ℕ → SimpleFunc α β such that for all n ∈ ℕ, the measure of the support of fs n is finite.

• 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 strongly measurable functions, and 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.

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

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

Equations

• MeasureTheory.StronglyMeasurable f = ∃ (fs : ℕ → MeasureTheory.SimpleFunc α β), ∀ (x : α), Filter.Tendsto (fun (n : ℕ) => ↑(fs n) x) Filter.atTop (nhds (f x))

def MeasureTheory.«termStronglyMeasurable[_]» : Lean.ParserDescr

The notation for StronglyMeasurable giving the measurable space instance explicitly.

Equations

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

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

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

Equations

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

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

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

Equations

• MeasureTheory.AEStronglyMeasurable f μ = ∃ (g : α → β), MeasureTheory.StronglyMeasurable g ∧ f =ᶠ[MeasureTheory.Measure.ae μ] g

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

Strongly measurable functions

theorem MeasureTheory.StronglyMeasurable.aestronglyMeasurable {α : Type u_5} {β : Type u_6} : ∀ {x : MeasurableSpace α} [inst : TopologicalSpace β] {f : α → β} {μ : MeasureTheory.Measure α}, MeasureTheory.StronglyMeasurable f → MeasureTheory.AEStronglyMeasurable f μ

@[simp]

theorem MeasureTheory.Subsingleton.stronglyMeasurable {α : Type u_5} {β : Type u_6} [MeasurableSpace α] [TopologicalSpace β] [Subsingleton β] (f : α → β) : MeasureTheory.StronglyMeasurable f

theorem MeasureTheory.SimpleFunc.stronglyMeasurable {α : Type u_5} {β : Type u_6} : ∀ {x : MeasurableSpace α} [inst : TopologicalSpace β] (f : MeasureTheory.SimpleFunc α β), MeasureTheory.StronglyMeasurable ↑f

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

@[deprecated MeasureTheory.StronglyMeasurable.of_finite]

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

Alias of MeasureTheory.StronglyMeasurable.of_finite.

@[deprecated MeasureTheory.StronglyMeasurable.of_finite]

theorem MeasureTheory.stronglyMeasurable_of_isEmpty {α : Type u_1} {β : Type u_2} [IsEmpty α] : ∀ {x : MeasurableSpace α} [inst : TopologicalSpace β] (f : α → β), MeasureTheory.StronglyMeasurable f

theorem MeasureTheory.stronglyMeasurable_const {α : Type u_5} {β : Type u_6} : ∀ {x : MeasurableSpace α} [inst : TopologicalSpace β] {b : β}, MeasureTheory.StronglyMeasurable fun (x : α) => b

theorem MeasureTheory.stronglyMeasurable_zero {α : Type u_5} {β : Type u_6} : ∀ {x : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : Zero β], MeasureTheory.StronglyMeasurable 0

theorem MeasureTheory.stronglyMeasurable_one {α : Type u_5} {β : Type u_6} : ∀ {x : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : One β], MeasureTheory.StronglyMeasurable 1

theorem MeasureTheory.stronglyMeasurable_const' {α : Type u_5} {β : Type u_6} {m : MeasurableSpace α} [TopologicalSpace β] {f : α → β} (hf : ∀ (x y : α), f x = f y) : MeasureTheory.StronglyMeasurable f

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

@[simp]

theorem MeasureTheory.Subsingleton.stronglyMeasurable' {α : Type u_5} {β : Type u_6} [MeasurableSpace α] [TopologicalSpace β] [Subsingleton α] (f : α → β) : MeasureTheory.StronglyMeasurable f

noncomputable def MeasureTheory.StronglyMeasurable.approx {α : Type u_1} {β : Type u_2} {f : α → β} [TopologicalSpace β] : {x : MeasurableSpace α} → MeasureTheory.StronglyMeasurable f → ℕ → MeasureTheory.SimpleFunc α β

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

Equations

• MeasureTheory.StronglyMeasurable.approx hf = Exists.choose hf

theorem MeasureTheory.StronglyMeasurable.tendsto_approx {α : Type u_1} {β : Type u_2} {f : α → β} [TopologicalSpace β] : ∀ {x : MeasurableSpace α} (hf : MeasureTheory.StronglyMeasurable f) (x_1 : α), Filter.Tendsto (fun (n : ℕ) => ↑(MeasureTheory.StronglyMeasurable.approx hf n) x_1) Filter.atTop (nhds (f x_1))

noncomputable def MeasureTheory.StronglyMeasurable.approxBounded {α : Type u_1} {β : Type u_2} {f : α → β} [TopologicalSpace β] : {x : MeasurableSpace α} → [inst : Norm β] → [inst : SMul ℝ β] → MeasureTheory.StronglyMeasurable f → ℝ → ℕ → MeasureTheory.SimpleFunc α β

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

Equations

• MeasureTheory.StronglyMeasurable.approxBounded hf c n = MeasureTheory.SimpleFunc.map (fun (x : β) => min 1 (c / ‖x‖) • x) (MeasureTheory.StronglyMeasurable.approx hf n)

theorem MeasureTheory.StronglyMeasurable.tendsto_approxBounded_of_norm_le {α : Type u_1} {β : Type u_5} {f : α → β} [NormedAddCommGroup β] [NormedSpace ℝ β] {m : MeasurableSpace α} (hf : MeasureTheory.StronglyMeasurable f) {c : ℝ} {x : α} (hfx : ‖f x‖ ≤ c) : Filter.Tendsto (fun (n : ℕ) => ↑(MeasureTheory.StronglyMeasurable.approxBounded hf c n) x) Filter.atTop (nhds (f x))

theorem MeasureTheory.StronglyMeasurable.tendsto_approxBounded_ae {α : Type u_1} {β : Type u_5} {f : α → β} [NormedAddCommGroup β] [NormedSpace ℝ β] {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hf : MeasureTheory.StronglyMeasurable f) {c : ℝ} (hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c) : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => ↑(MeasureTheory.StronglyMeasurable.approxBounded hf c n) x) Filter.atTop (nhds (f x))

theorem MeasureTheory.StronglyMeasurable.norm_approxBounded_le {α : Type u_1} {β : Type u_5} {f : α → β} [SeminormedAddCommGroup β] [NormedSpace ℝ β] {m : MeasurableSpace α} {c : ℝ} (hf : MeasureTheory.StronglyMeasurable f) (hc : 0 ≤ c) (n : ℕ) (x : α) : ‖↑(MeasureTheory.StronglyMeasurable.approxBounded hf c n) x‖ ≤ c

theorem stronglyMeasurable_bot_iff {α : Type u_1} {β : Type u_2} {f : α → β} [TopologicalSpace β] [Nonempty β] [T2Space β] : MeasureTheory.StronglyMeasurable f ↔ ∃ (c : β), f = fun (x : α) => c

theorem MeasureTheory.StronglyMeasurable.finStronglyMeasurable_of_set_sigmaFinite {α : Type u_1} {β : Type u_2} {f : α → β} [TopologicalSpace β] [Zero β] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hf_meas : MeasureTheory.StronglyMeasurable f) {t : Set α} (ht : MeasurableSet t) (hft_zero : ∀ x ∈ tᶜ, f x = 0) (htμ : MeasureTheory.SigmaFinite (MeasureTheory.Measure.restrict μ t)) : MeasureTheory.FinStronglyMeasurable f μ

theorem MeasureTheory.StronglyMeasurable.finStronglyMeasurable {α : Type u_1} {β : Type u_2} {f : α → β} [TopologicalSpace β] [Zero β] {m0 : MeasurableSpace α} (hf : MeasureTheory.StronglyMeasurable f) (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] : MeasureTheory.FinStronglyMeasurable f μ

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

theorem MeasureTheory.StronglyMeasurable.measurable {α : Type u_1} {β : Type u_2} {f : α → β} : ∀ {x : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : TopologicalSpace.PseudoMetrizableSpace β] [inst_2 : MeasurableSpace β] [inst_3 : BorelSpace β], MeasureTheory.StronglyMeasurable f → Measurable f

A strongly measurable function is measurable.

theorem MeasureTheory.StronglyMeasurable.aemeasurable {α : Type u_1} {β : Type u_2} {f : α → β} : ∀ {x : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : TopologicalSpace.PseudoMetrizableSpace β] [inst_2 : MeasurableSpace β] [inst_3 : BorelSpace β] {μ : MeasureTheory.Measure α}, MeasureTheory.StronglyMeasurable f → AEMeasurable f

A strongly measurable function is almost everywhere measurable.

theorem Continuous.comp_stronglyMeasurable {α : Type u_1} {β : Type u_2} {γ : Type u_3} : ∀ {x : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : TopologicalSpace γ] {g : β → γ} {f : α → β}, Continuous g → MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable fun (x : α) => g (f x)

theorem MeasureTheory.StronglyMeasurable.measurableSet_support {α : Type u_1} {β : Type u_2} {f : α → β} {m : MeasurableSpace α} [Zero β] [TopologicalSpace β] [TopologicalSpace.MetrizableSpace β] (hf : MeasureTheory.StronglyMeasurable f) : MeasurableSet (Function.support f)

theorem MeasureTheory.StronglyMeasurable.measurableSet_mulSupport {α : Type u_1} {β : Type u_2} {f : α → β} {m : MeasurableSpace α} [One β] [TopologicalSpace β] [TopologicalSpace.MetrizableSpace β] (hf : MeasureTheory.StronglyMeasurable f) : MeasurableSet (Function.mulSupport f)

theorem MeasureTheory.StronglyMeasurable.mono {α : Type u_1} {β : Type u_2} {f : α → β} {m : MeasurableSpace α} {m' : MeasurableSpace α} [TopologicalSpace β] (hf : MeasureTheory.StronglyMeasurable f) (h_mono : m' ≤ m) : MeasureTheory.StronglyMeasurable f

theorem MeasureTheory.StronglyMeasurable.prod_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} [TopologicalSpace β] [TopologicalSpace γ] {f : α → β} {g : α → γ} (hf : MeasureTheory.StronglyMeasurable f) (hg : MeasureTheory.StronglyMeasurable g) : MeasureTheory.StronglyMeasurable fun (x : α) => (f x, g x)

theorem MeasureTheory.StronglyMeasurable.comp_measurable {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace β] : ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace γ} {f : α → β} {g : γ → α}, MeasureTheory.StronglyMeasurable f → Measurable g → MeasureTheory.StronglyMeasurable (f ∘ g)

theorem MeasureTheory.StronglyMeasurable.of_uncurry_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace β] : ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace γ} {f : α → γ → β}, MeasureTheory.StronglyMeasurable (Function.uncurry f) → ∀ {x : α}, MeasureTheory.StronglyMeasurable (f x)

theorem MeasureTheory.StronglyMeasurable.of_uncurry_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace β] : ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace γ} {f : α → γ → β}, MeasureTheory.StronglyMeasurable (Function.uncurry f) → ∀ {y : γ}, MeasureTheory.StronglyMeasurable fun (x : α) => f x y

theorem MeasureTheory.StronglyMeasurable.add {α : Type u_1} {β : Type u_2} {f : α → β} {g : α → β} {mα : MeasurableSpace α} [TopologicalSpace β] [Add β] [ContinuousAdd β] (hf : MeasureTheory.StronglyMeasurable f) (hg : MeasureTheory.StronglyMeasurable g) : MeasureTheory.StronglyMeasurable (f + g)

theorem MeasureTheory.StronglyMeasurable.mul {α : Type u_1} {β : Type u_2} {f : α → β} {g : α → β} {mα : MeasurableSpace α} [TopologicalSpace β] [Mul β] [ContinuousMul β] (hf : MeasureTheory.StronglyMeasurable f) (hg : MeasureTheory.StronglyMeasurable g) : MeasureTheory.StronglyMeasurable (f * g)

theorem MeasureTheory.StronglyMeasurable.add_const {α : Type u_1} {β : Type u_2} {f : α → β} {mα : MeasurableSpace α} [TopologicalSpace β] [Add β] [ContinuousAdd β] (hf : MeasureTheory.StronglyMeasurable f) (c : β) : MeasureTheory.StronglyMeasurable fun (x : α) => f x + c

theorem MeasureTheory.StronglyMeasurable.mul_const {α : Type u_1} {β : Type u_2} {f : α → β} {mα : MeasurableSpace α} [TopologicalSpace β] [Mul β] [ContinuousMul β] (hf : MeasureTheory.StronglyMeasurable f) (c : β) : MeasureTheory.StronglyMeasurable fun (x : α) => f x * c

theorem MeasureTheory.StronglyMeasurable.const_add {α : Type u_1} {β : Type u_2} {f : α → β} {mα : MeasurableSpace α} [TopologicalSpace β] [Add β] [ContinuousAdd β] (hf : MeasureTheory.StronglyMeasurable f) (c : β) : MeasureTheory.StronglyMeasurable fun (x : α) => c + f x

theorem MeasureTheory.StronglyMeasurable.const_mul {α : Type u_1} {β : Type u_2} {f : α → β} {mα : MeasurableSpace α} [TopologicalSpace β] [Mul β] [ContinuousMul β] (hf : MeasureTheory.StronglyMeasurable f) (c : β) : MeasureTheory.StronglyMeasurable fun (x : α) => c * f x

theorem MeasureTheory.StronglyMeasurable.const_nsmul {α : Type u_1} {β : Type u_2} {f : α → β} {mα : MeasurableSpace α} [TopologicalSpace β] [AddMonoid β] [ContinuousAdd β] (hf : MeasureTheory.StronglyMeasurable f) (n : ℕ) : MeasureTheory.StronglyMeasurable (n • f)

theorem MeasureTheory.StronglyMeasurable.pow {α : Type u_1} {β : Type u_2} {f : α → β} {mα : MeasurableSpace α} [TopologicalSpace β] [Monoid β] [ContinuousMul β] (hf : MeasureTheory.StronglyMeasurable f) (n : ℕ) : MeasureTheory.StronglyMeasurable (f ^ n)

theorem MeasureTheory.StronglyMeasurable.neg {α : Type u_1} {β : Type u_2} {f : α → β} {mα : MeasurableSpace α} [TopologicalSpace β] [Neg β] [ContinuousNeg β] (hf : MeasureTheory.StronglyMeasurable f) : MeasureTheory.StronglyMeasurable (-f)

theorem MeasureTheory.StronglyMeasurable.inv {α : Type u_1} {β : Type u_2} {f : α → β} {mα : MeasurableSpace α} [TopologicalSpace β] [Inv β] [ContinuousInv β] (hf : MeasureTheory.StronglyMeasurable f) : MeasureTheory.StronglyMeasurable f⁻¹

theorem MeasureTheory.StronglyMeasurable.sub {α : Type u_1} {β : Type u_2} {f : α → β} {g : α → β} {mα : MeasurableSpace α} [TopologicalSpace β] [Sub β] [ContinuousSub β] (hf : MeasureTheory.StronglyMeasurable f) (hg : MeasureTheory.StronglyMeasurable g) : MeasureTheory.StronglyMeasurable (f - g)

theorem MeasureTheory.StronglyMeasurable.div {α : Type u_1} {β : Type u_2} {f : α → β} {g : α → β} {mα : MeasurableSpace α} [TopologicalSpace β] [Div β] [ContinuousDiv β] (hf : MeasureTheory.StronglyMeasurable f) (hg : MeasureTheory.StronglyMeasurable g) : MeasureTheory.StronglyMeasurable (f / g)

theorem MeasureTheory.StronglyMeasurable.vadd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [TopologicalSpace β] {𝕜 : Type u_5} [TopologicalSpace 𝕜] [VAdd 𝕜 β] [ContinuousVAdd 𝕜 β] {f : α → 𝕜} {g : α → β} (hf : MeasureTheory.StronglyMeasurable f) (hg : MeasureTheory.StronglyMeasurable g) : MeasureTheory.StronglyMeasurable fun (x : α) => f x +ᵥ g x

theorem MeasureTheory.StronglyMeasurable.smul {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [TopologicalSpace β] {𝕜 : Type u_5} [TopologicalSpace 𝕜] [SMul 𝕜 β] [ContinuousSMul 𝕜 β] {f : α → 𝕜} {g : α → β} (hf : MeasureTheory.StronglyMeasurable f) (hg : MeasureTheory.StronglyMeasurable g) : MeasureTheory.StronglyMeasurable fun (x : α) => f x • g x

theorem MeasureTheory.StronglyMeasurable.const_vadd {α : Type u_1} {β : Type u_2} {f : α → β} {mα : MeasurableSpace α} [TopologicalSpace β] {𝕜 : Type u_5} [VAdd 𝕜 β] [ContinuousConstVAdd 𝕜 β] (hf : MeasureTheory.StronglyMeasurable f) (c : 𝕜) : MeasureTheory.StronglyMeasurable (c +ᵥ f)

theorem MeasureTheory.StronglyMeasurable.const_smul {α : Type u_1} {β : Type u_2} {f : α → β} {mα : MeasurableSpace α} [TopologicalSpace β] {𝕜 : Type u_5} [SMul 𝕜 β] [ContinuousConstSMul 𝕜 β] (hf : MeasureTheory.StronglyMeasurable f) (c : 𝕜) : MeasureTheory.StronglyMeasurable (c • f)

theorem MeasureTheory.StronglyMeasurable.const_vadd' {α : Type u_1} {β : Type u_2} {f : α → β} {mα : MeasurableSpace α} [TopologicalSpace β] {𝕜 : Type u_5} [VAdd 𝕜 β] [ContinuousConstVAdd 𝕜 β] (hf : MeasureTheory.StronglyMeasurable f) (c : 𝕜) : MeasureTheory.StronglyMeasurable fun (x : α) => c +ᵥ f x

theorem MeasureTheory.StronglyMeasurable.const_smul' {α : Type u_1} {β : Type u_2} {f : α → β} {mα : MeasurableSpace α} [TopologicalSpace β] {𝕜 : Type u_5} [SMul 𝕜 β] [ContinuousConstSMul 𝕜 β] (hf : MeasureTheory.StronglyMeasurable f) (c : 𝕜) : MeasureTheory.StronglyMeasurable fun (x : α) => c • f x

theorem MeasureTheory.StronglyMeasurable.vadd_const {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [TopologicalSpace β] {𝕜 : Type u_5} [TopologicalSpace 𝕜] [VAdd 𝕜 β] [ContinuousVAdd 𝕜 β] {f : α → 𝕜} (hf : MeasureTheory.StronglyMeasurable f) (c : β) : MeasureTheory.StronglyMeasurable fun (x : α) => f x +ᵥ c

theorem MeasureTheory.StronglyMeasurable.smul_const {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [TopologicalSpace β] {𝕜 : Type u_5} [TopologicalSpace 𝕜] [SMul 𝕜 β] [ContinuousSMul 𝕜 β] {f : α → 𝕜} (hf : MeasureTheory.StronglyMeasurable f) (c : β) : MeasureTheory.StronglyMeasurable fun (x : α) => f x • c

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

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

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

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

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

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

theorem stronglyMeasurable_const_smul_iff {α : Type u_1} {β : Type u_2} {f : α → β} {G : Type u_6} [TopologicalSpace β] [Group G] [MulAction G β] [ContinuousConstSMul G β] {m : MeasurableSpace α} (c : G) : (MeasureTheory.StronglyMeasurable fun (x : α) => c • f x) ↔ MeasureTheory.StronglyMeasurable f

theorem IsUnit.stronglyMeasurable_const_smul_iff {α : Type u_1} {β : Type u_2} {f : α → β} {M : Type u_5} [TopologicalSpace β] [Monoid M] [MulAction M β] [ContinuousConstSMul M β] : ∀ {x : MeasurableSpace α} {c : M}, IsUnit c → ((MeasureTheory.StronglyMeasurable fun (x : α) => c • f x) ↔ MeasureTheory.StronglyMeasurable f)

theorem stronglyMeasurable_const_smul_iff₀ {α : Type u_1} {β : Type u_2} {f : α → β} {G₀ : Type u_7} [TopologicalSpace β] [GroupWithZero G₀] [MulAction G₀ β] [ContinuousConstSMul G₀ β] : ∀ {x : MeasurableSpace α} {c : G₀}, c ≠ 0 → ((MeasureTheory.StronglyMeasurable fun (x : α) => c • f x) ↔ MeasureTheory.StronglyMeasurable f)

theorem MeasureTheory.StronglyMeasurable.sup {α : Type u_1} {β : Type u_2} {f : α → β} {g : α → β} [MeasurableSpace α] [TopologicalSpace β] [Sup β] [ContinuousSup β] (hf : MeasureTheory.StronglyMeasurable f) (hg : MeasureTheory.StronglyMeasurable g) : MeasureTheory.StronglyMeasurable (f ⊔ g)

theorem MeasureTheory.StronglyMeasurable.inf {α : Type u_1} {β : Type u_2} {f : α → β} {g : α → β} [MeasurableSpace α] [TopologicalSpace β] [Inf β] [ContinuousInf β] (hf : MeasureTheory.StronglyMeasurable f) (hg : MeasureTheory.StronglyMeasurable g) : MeasureTheory.StronglyMeasurable (f ⊓ g)

Big operators: ∏ and ∑

theorem List.stronglyMeasurable_sum' {α : Type u_1} {M : Type u_5} [AddMonoid M] [TopologicalSpace M] [ContinuousAdd M] {m : MeasurableSpace α} (l : List (α → M)) (hl : ∀ f ∈ l, MeasureTheory.StronglyMeasurable f) : MeasureTheory.StronglyMeasurable (List.sum l)

theorem List.stronglyMeasurable_prod' {α : Type u_1} {M : Type u_5} [Monoid M] [TopologicalSpace M] [ContinuousMul M] {m : MeasurableSpace α} (l : List (α → M)) (hl : ∀ f ∈ l, MeasureTheory.StronglyMeasurable f) : MeasureTheory.StronglyMeasurable (List.prod l)

theorem List.stronglyMeasurable_sum {α : Type u_1} {M : Type u_5} [AddMonoid M] [TopologicalSpace M] [ContinuousAdd M] {m : MeasurableSpace α} (l : List (α → M)) (hl : ∀ f ∈ l, MeasureTheory.StronglyMeasurable f) : MeasureTheory.StronglyMeasurable fun (x : α) => List.sum (List.map (fun (f : α → M) => f x) l)

theorem List.stronglyMeasurable_prod {α : Type u_1} {M : Type u_5} [Monoid M] [TopologicalSpace M] [ContinuousMul M] {m : MeasurableSpace α} (l : List (α → M)) (hl : ∀ f ∈ l, MeasureTheory.StronglyMeasurable f) : MeasureTheory.StronglyMeasurable fun (x : α) => List.prod (List.map (fun (f : α → M) => f x) l)

theorem Multiset.stronglyMeasurable_sum' {α : Type u_1} {M : Type u_5} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] {m : MeasurableSpace α} (l : Multiset (α → M)) (hl : ∀ f ∈ l, MeasureTheory.StronglyMeasurable f) : MeasureTheory.StronglyMeasurable (Multiset.sum l)

theorem Multiset.stronglyMeasurable_prod' {α : Type u_1} {M : Type u_5} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] {m : MeasurableSpace α} (l : Multiset (α → M)) (hl : ∀ f ∈ l, MeasureTheory.StronglyMeasurable f) : MeasureTheory.StronglyMeasurable (Multiset.prod l)

theorem Multiset.stronglyMeasurable_sum {α : Type u_1} {M : Type u_5} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] {m : MeasurableSpace α} (s : Multiset (α → M)) (hs : ∀ f ∈ s, MeasureTheory.StronglyMeasurable f) : MeasureTheory.StronglyMeasurable fun (x : α) => Multiset.sum (Multiset.map (fun (f : α → M) => f x) s)

theorem Multiset.stronglyMeasurable_prod {α : Type u_1} {M : Type u_5} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] {m : MeasurableSpace α} (s : Multiset (α → M)) (hs : ∀ f ∈ s, MeasureTheory.StronglyMeasurable f) : MeasureTheory.StronglyMeasurable fun (x : α) => Multiset.prod (Multiset.map (fun (f : α → M) => f x) s)

theorem Finset.stronglyMeasurable_sum' {α : Type u_1} {M : Type u_5} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] {m : MeasurableSpace α} {ι : Type u_6} {f : ι → α → M} (s : Finset ι) (hf : ∀ i ∈ s, MeasureTheory.StronglyMeasurable (f i)) : MeasureTheory.StronglyMeasurable (Finset.sum s fun (i : ι) => f i)

theorem Finset.stronglyMeasurable_prod' {α : Type u_1} {M : Type u_5} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] {m : MeasurableSpace α} {ι : Type u_6} {f : ι → α → M} (s : Finset ι) (hf : ∀ i ∈ s, MeasureTheory.StronglyMeasurable (f i)) : MeasureTheory.StronglyMeasurable (Finset.prod s fun (i : ι) => f i)

theorem Finset.stronglyMeasurable_sum {α : Type u_1} {M : Type u_5} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] {m : MeasurableSpace α} {ι : Type u_6} {f : ι → α → M} (s : Finset ι) (hf : ∀ i ∈ s, MeasureTheory.StronglyMeasurable (f i)) : MeasureTheory.StronglyMeasurable fun (a : α) => Finset.sum s fun (i : ι) => f i a

theorem Finset.stronglyMeasurable_prod {α : Type u_1} {M : Type u_5} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] {m : MeasurableSpace α} {ι : Type u_6} {f : ι → α → M} (s : Finset ι) (hf : ∀ i ∈ s, MeasureTheory.StronglyMeasurable (f i)) : MeasureTheory.StronglyMeasurable fun (a : α) => Finset.prod s fun (i : ι) => f i a

theorem MeasureTheory.StronglyMeasurable.isSeparable_range {α : Type u_1} {β : Type u_2} {f : α → β} {m : MeasurableSpace α} [TopologicalSpace β] (hf : MeasureTheory.StronglyMeasurable f) : TopologicalSpace.IsSeparable (Set.range f)

The range of a strongly measurable function is separable.

theorem MeasureTheory.StronglyMeasurable.separableSpace_range_union_singleton {α : Type u_1} {β : Type u_2} {f : α → β} : ∀ {x : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : TopologicalSpace.PseudoMetrizableSpace β], MeasureTheory.StronglyMeasurable f → ∀ {b : β}, TopologicalSpace.SeparableSpace ↑(Set.range f ∪ {b})

theorem Measurable.stronglyMeasurable {α : Type u_1} {β : Type u_2} {f : α → β} {mα : MeasurableSpace α} [MeasurableSpace β] [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [SecondCountableTopology β] [OpensMeasurableSpace β] (hf : Measurable f) : MeasureTheory.StronglyMeasurable f

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

theorem stronglyMeasurable_iff_measurable {α : Type u_1} {β : Type u_2} {f : α → β} {mα : MeasurableSpace α} [MeasurableSpace β] [TopologicalSpace β] [TopologicalSpace.MetrizableSpace β] [BorelSpace β] [SecondCountableTopology β] : MeasureTheory.StronglyMeasurable f ↔ Measurable f

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

theorem stronglyMeasurable_id {α : Type u_1} {mα : MeasurableSpace α} [TopologicalSpace α] [TopologicalSpace.PseudoMetrizableSpace α] [OpensMeasurableSpace α] [SecondCountableTopology α] : MeasureTheory.StronglyMeasurable id

theorem stronglyMeasurable_iff_measurable_separable {α : Type u_1} {β : Type u_2} {f : α → β} {m : MeasurableSpace α} [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [MeasurableSpace β] [BorelSpace β] : MeasureTheory.StronglyMeasurable f ↔ Measurable f ∧ TopologicalSpace.IsSeparable (Set.range f)

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

theorem Continuous.stronglyMeasurable {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [TopologicalSpace α] [OpensMeasurableSpace α] [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [h : SecondCountableTopologyEither α β] {f : α → β} (hf : Continuous f) : MeasureTheory.StronglyMeasurable f

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

theorem Continuous.stronglyMeasurable_of_support_subset_isCompact {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [TopologicalSpace α] [OpensMeasurableSpace α] [MeasurableSpace β] [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [BorelSpace β] [Zero β] {f : α → β} (hf : Continuous f) {k : Set α} (hk : IsCompact k) (h'f : Function.support f ⊆ k) : MeasureTheory.StronglyMeasurable f

theorem Continuous.stronglyMeasurable_of_mulSupport_subset_isCompact {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [TopologicalSpace α] [OpensMeasurableSpace α] [MeasurableSpace β] [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [BorelSpace β] [One β] {f : α → β} (hf : Continuous f) {k : Set α} (hk : IsCompact k) (h'f : Function.mulSupport f ⊆ k) : MeasureTheory.StronglyMeasurable f

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

theorem Continuous.stronglyMeasurable_of_hasCompactSupport {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [TopologicalSpace α] [OpensMeasurableSpace α] [MeasurableSpace β] [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [BorelSpace β] [Zero β] {f : α → β} (hf : Continuous f) (h'f : HasCompactSupport f) : MeasureTheory.StronglyMeasurable f

theorem Continuous.stronglyMeasurable_of_hasCompactMulSupport {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [TopologicalSpace α] [OpensMeasurableSpace α] [MeasurableSpace β] [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [BorelSpace β] [One β] {f : α → β} (hf : Continuous f) (h'f : HasCompactMulSupport f) : MeasureTheory.StronglyMeasurable f

A continuous function with compact support is strongly measurable.

theorem HasCompactSupport.stronglyMeasurable_of_prod {α : Type u_1} {X : Type u_5} {Y : Type u_6} [Zero α] [TopologicalSpace X] [TopologicalSpace Y] [MeasurableSpace X] [MeasurableSpace Y] [OpensMeasurableSpace X] [OpensMeasurableSpace Y] [TopologicalSpace α] [TopologicalSpace.PseudoMetrizableSpace α] {f : X × Y → α} (hf : Continuous f) (h'f : HasCompactSupport f) : MeasureTheory.StronglyMeasurable f

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

theorem Embedding.comp_stronglyMeasurable_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [TopologicalSpace γ] [TopologicalSpace.PseudoMetrizableSpace γ] {g : β → γ} {f : α → β} (hg : Embedding g) : (MeasureTheory.StronglyMeasurable fun (x : α) => g (f x)) ↔ MeasureTheory.StronglyMeasurable f

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

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

A sequential limit of strongly measurable functions is strongly measurable.

theorem MeasureTheory.StronglyMeasurable.piecewise {α : Type u_1} {β : Type u_2} {f : α → β} {g : α → β} {m : MeasurableSpace α} [TopologicalSpace β] {s : Set α} : ∀ {x : DecidablePred fun (x : α) => x ∈ s}, MeasurableSet s → MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable g → MeasureTheory.StronglyMeasurable (Set.piecewise s f g)

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

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

theorem MeasurableEmbedding.stronglyMeasurable_extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : α → γ} {g' : γ → β} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} [TopologicalSpace β] (hg : MeasurableEmbedding g) (hf : MeasureTheory.StronglyMeasurable f) (hg' : MeasureTheory.StronglyMeasurable g') : MeasureTheory.StronglyMeasurable (Function.extend g f g')

theorem MeasurableEmbedding.exists_stronglyMeasurable_extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : α → γ} : ∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace γ} [inst : TopologicalSpace β], MeasurableEmbedding g → MeasureTheory.StronglyMeasurable f → (γ → Nonempty β) → ∃ (f' : γ → β), MeasureTheory.StronglyMeasurable f' ∧ f' ∘ g = f

theorem stronglyMeasurable_of_stronglyMeasurable_union_cover {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [TopologicalSpace β] {f : α → β} (s : Set α) (t : Set α) (hs : MeasurableSet s) (ht : MeasurableSet t) (h : Set.univ ⊆ s ∪ t) (hc : MeasureTheory.StronglyMeasurable fun (a : ↑s) => f ↑a) (hd : MeasureTheory.StronglyMeasurable fun (a : ↑t) => f ↑a) : MeasureTheory.StronglyMeasurable f

theorem stronglyMeasurable_of_restrict_of_restrict_compl {α : Type u_1} {β : Type u_2} : ∀ {x : MeasurableSpace α} [inst : TopologicalSpace β] {f : α → β} {s : Set α}, MeasurableSet s → MeasureTheory.StronglyMeasurable (Set.restrict s f) → MeasureTheory.StronglyMeasurable (Set.restrict sᶜ f) → MeasureTheory.StronglyMeasurable f

theorem MeasureTheory.StronglyMeasurable.indicator {α : Type u_1} {β : Type u_2} {f : α → β} : ∀ {x : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : Zero β], MeasureTheory.StronglyMeasurable f → ∀ {s : Set α}, MeasurableSet s → MeasureTheory.StronglyMeasurable (Set.indicator s f)

theorem MeasureTheory.StronglyMeasurable.dist {α : Type u_1} : ∀ {x : MeasurableSpace α} {β : Type u_5} [inst : PseudoMetricSpace β] {f g : α → β}, MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable g → MeasureTheory.StronglyMeasurable fun (x : α) => dist (f x) (g x)

theorem MeasureTheory.StronglyMeasurable.norm {α : Type u_1} : ∀ {x : MeasurableSpace α} {β : Type u_5} [inst : SeminormedAddCommGroup β] {f : α → β}, MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable fun (x : α) => ‖f x‖

theorem MeasureTheory.StronglyMeasurable.nnnorm {α : Type u_1} : ∀ {x : MeasurableSpace α} {β : Type u_5} [inst : SeminormedAddCommGroup β] {f : α → β}, MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable fun (x : α) => ‖f x‖₊

theorem MeasureTheory.StronglyMeasurable.ennnorm {α : Type u_1} : ∀ {x : MeasurableSpace α} {β : Type u_5} [inst : SeminormedAddCommGroup β] {f : α → β}, MeasureTheory.StronglyMeasurable f → Measurable fun (a : α) => ↑‖f a‖₊

theorem MeasureTheory.StronglyMeasurable.real_toNNReal {α : Type u_1} : ∀ {x : MeasurableSpace α} {f : α → ℝ}, MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable fun (x : α) => Real.toNNReal (f x)

theorem MeasureTheory.StronglyMeasurable.measurableSet_eq_fun {α : Type u_1} {m : MeasurableSpace α} {E : Type u_5} [TopologicalSpace E] [TopologicalSpace.MetrizableSpace E] {f : α → E} {g : α → E} (hf : MeasureTheory.StronglyMeasurable f) (hg : MeasureTheory.StronglyMeasurable g) : MeasurableSet {x : α | f x = g x}

theorem MeasureTheory.StronglyMeasurable.measurableSet_lt {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [TopologicalSpace β] [LinearOrder β] [OrderClosedTopology β] [TopologicalSpace.PseudoMetrizableSpace β] {f : α → β} {g : α → β} (hf : MeasureTheory.StronglyMeasurable f) (hg : MeasureTheory.StronglyMeasurable g) : MeasurableSet {a : α | f a < g a}

theorem MeasureTheory.StronglyMeasurable.measurableSet_le {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [TopologicalSpace β] [Preorder β] [OrderClosedTopology β] [TopologicalSpace.PseudoMetrizableSpace β] {f : α → β} {g : α → β} (hf : MeasureTheory.StronglyMeasurable f) (hg : MeasureTheory.StronglyMeasurable g) : MeasurableSet {a : α | f a ≤ g a}

theorem MeasureTheory.StronglyMeasurable.stronglyMeasurable_in_set {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [TopologicalSpace β] [Zero β] {s : Set α} {f : α → β} (hs : MeasurableSet s) (hf : MeasureTheory.StronglyMeasurable f) (hf_zero : ∀ x ∉ s, f x = 0) : ∃ (fs : ℕ → MeasureTheory.SimpleFunc α β), (∀ (x : α), Filter.Tendsto (fun (n : ℕ) => ↑(fs n) x) Filter.atTop (nhds (f x))) ∧ ∀ x ∉ s, ∀ (n : ℕ), ↑(fs n) x = 0

theorem MeasureTheory.StronglyMeasurable.stronglyMeasurable_of_measurableSpace_le_on {α : Type u_5} {E : Type u_6} {m : MeasurableSpace α} {m₂ : MeasurableSpace α} [TopologicalSpace E] [Zero E] {s : Set α} {f : α → E} (hs_m : MeasurableSet s) (hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)) (hf : MeasureTheory.StronglyMeasurable f) (hf_zero : ∀ x ∉ s, f x = 0) : MeasureTheory.StronglyMeasurable 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 supported on s is m-strongly-measurable, then f is also m₂-strongly-measurable.

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

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

Finitely strongly measurable functions

theorem MeasureTheory.finStronglyMeasurable_zero {α : Type u_5} {β : Type u_6} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Zero β] [TopologicalSpace β] : MeasureTheory.FinStronglyMeasurable 0 μ

theorem MeasureTheory.FinStronglyMeasurable.aefinStronglyMeasurable {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β} [Zero β] [TopologicalSpace β] (hf : MeasureTheory.FinStronglyMeasurable f μ) : MeasureTheory.AEFinStronglyMeasurable f μ

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

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

Equations

• MeasureTheory.FinStronglyMeasurable.approx hf = Exists.choose hf

theorem MeasureTheory.FinStronglyMeasurable.fin_support_approx {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β} [Zero β] [TopologicalSpace β] (hf : MeasureTheory.FinStronglyMeasurable f μ) (n : ℕ) : ↑↑μ (Function.support ↑(MeasureTheory.FinStronglyMeasurable.approx hf n)) < ⊤

theorem MeasureTheory.FinStronglyMeasurable.tendsto_approx {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β} [Zero β] [TopologicalSpace β] (hf : MeasureTheory.FinStronglyMeasurable f μ) (x : α) : Filter.Tendsto (fun (n : ℕ) => ↑(MeasureTheory.FinStronglyMeasurable.approx hf n) x) Filter.atTop (nhds (f x))

theorem MeasureTheory.FinStronglyMeasurable.stronglyMeasurable {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β} [Zero β] [TopologicalSpace β] (hf : MeasureTheory.FinStronglyMeasurable f μ) : MeasureTheory.StronglyMeasurable f

A finitely strongly measurable function is strongly measurable.

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

theorem MeasureTheory.FinStronglyMeasurable.measurable {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β} [Zero β] [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [MeasurableSpace β] [BorelSpace β] (hf : MeasureTheory.FinStronglyMeasurable f μ) : Measurable f

A finitely strongly measurable function is measurable.

theorem MeasureTheory.FinStronglyMeasurable.mul {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β} {g : α → β} [TopologicalSpace β] [MonoidWithZero β] [ContinuousMul β] (hf : MeasureTheory.FinStronglyMeasurable f μ) (hg : MeasureTheory.FinStronglyMeasurable g μ) : MeasureTheory.FinStronglyMeasurable (f * g) μ

theorem MeasureTheory.FinStronglyMeasurable.add {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β} {g : α → β} [TopologicalSpace β] [AddMonoid β] [ContinuousAdd β] (hf : MeasureTheory.FinStronglyMeasurable f μ) (hg : MeasureTheory.FinStronglyMeasurable g μ) : MeasureTheory.FinStronglyMeasurable (f + g) μ

theorem MeasureTheory.FinStronglyMeasurable.neg {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β} [TopologicalSpace β] [AddGroup β] [TopologicalAddGroup β] (hf : MeasureTheory.FinStronglyMeasurable f μ) : MeasureTheory.FinStronglyMeasurable (-f) μ

theorem MeasureTheory.FinStronglyMeasurable.sub {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β} {g : α → β} [TopologicalSpace β] [AddGroup β] [ContinuousSub β] (hf : MeasureTheory.FinStronglyMeasurable f μ) (hg : MeasureTheory.FinStronglyMeasurable g μ) : MeasureTheory.FinStronglyMeasurable (f - g) μ

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

theorem MeasureTheory.FinStronglyMeasurable.sup {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β} {g : α → β} [TopologicalSpace β] [Zero β] [SemilatticeSup β] [ContinuousSup β] (hf : MeasureTheory.FinStronglyMeasurable f μ) (hg : MeasureTheory.FinStronglyMeasurable g μ) : MeasureTheory.FinStronglyMeasurable (f ⊔ g) μ

theorem MeasureTheory.FinStronglyMeasurable.inf {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β} {g : α → β} [TopologicalSpace β] [Zero β] [SemilatticeInf β] [ContinuousInf β] (hf : MeasureTheory.FinStronglyMeasurable f μ) (hg : MeasureTheory.FinStronglyMeasurable g μ) : MeasureTheory.FinStronglyMeasurable (f ⊓ g) μ

theorem MeasureTheory.finStronglyMeasurable_iff_stronglyMeasurable_and_exists_set_sigmaFinite {α : Type u_5} {β : Type u_6} {f : α → β} [TopologicalSpace β] [T2Space β] [Zero β] : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α}, MeasureTheory.FinStronglyMeasurable f μ ↔ MeasureTheory.StronglyMeasurable f ∧ ∃ (t : Set α), MeasurableSet t ∧ (∀ x ∈ tᶜ, f x = 0) ∧ MeasureTheory.SigmaFinite (MeasureTheory.Measure.restrict μ t)

theorem MeasureTheory.aefinStronglyMeasurable_zero {α : Type u_5} {β : Type u_6} : ∀ {x : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : Zero β] [inst_1 : TopologicalSpace β], MeasureTheory.AEFinStronglyMeasurable 0 μ

Almost everywhere strongly measurable functions

theorem MeasureTheory.aestronglyMeasurable_const {α : Type u_5} {β : Type u_6} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β] {b : β}, MeasureTheory.AEStronglyMeasurable (fun (x : α) => b) μ

theorem MeasureTheory.aestronglyMeasurable_zero {α : Type u_5} {β : Type u_6} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β] [inst_1 : Zero β], MeasureTheory.AEStronglyMeasurable 0 μ

theorem MeasureTheory.aestronglyMeasurable_one {α : Type u_5} {β : Type u_6} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β] [inst_1 : One β], MeasureTheory.AEStronglyMeasurable 1 μ

@[simp]

theorem MeasureTheory.Subsingleton.aestronglyMeasurable {α : Type u_1} {β : Type u_2} : ∀ {x : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : Subsingleton β] {μ : MeasureTheory.Measure α} (f : α → β), MeasureTheory.AEStronglyMeasurable f μ

@[simp]

theorem MeasureTheory.Subsingleton.aestronglyMeasurable' {α : Type u_1} {β : Type u_2} : ∀ {x : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : Subsingleton α] {μ : MeasureTheory.Measure α} (f : α → β), MeasureTheory.AEStronglyMeasurable f μ

@[simp]

theorem MeasureTheory.aestronglyMeasurable_zero_measure {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [TopologicalSpace β] (f : α → β) : MeasureTheory.AEStronglyMeasurable f 0

theorem MeasureTheory.SimpleFunc.aestronglyMeasurable {α : Type u_1} {β : Type u_2} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β] (f : MeasureTheory.SimpleFunc α β), MeasureTheory.AEStronglyMeasurable (↑f) μ

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

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

Equations

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

theorem MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} (hf : MeasureTheory.AEStronglyMeasurable f μ) : MeasureTheory.StronglyMeasurable (MeasureTheory.AEStronglyMeasurable.mk f hf)

theorem MeasureTheory.AEStronglyMeasurable.measurable_mk {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} [TopologicalSpace.PseudoMetrizableSpace β] [MeasurableSpace β] [BorelSpace β] (hf : MeasureTheory.AEStronglyMeasurable f μ) : Measurable (MeasureTheory.AEStronglyMeasurable.mk f hf)

theorem MeasureTheory.AEStronglyMeasurable.ae_eq_mk {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} (hf : MeasureTheory.AEStronglyMeasurable f μ) : f =ᶠ[MeasureTheory.Measure.ae μ] MeasureTheory.AEStronglyMeasurable.mk f hf

theorem MeasureTheory.AEStronglyMeasurable.aemeasurable {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_5} [MeasurableSpace β] [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [BorelSpace β] {f : α → β} (hf : MeasureTheory.AEStronglyMeasurable f μ) : AEMeasurable f

theorem MeasureTheory.AEStronglyMeasurable.congr {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} {g : α → β} (hf : MeasureTheory.AEStronglyMeasurable f μ) (h : f =ᶠ[MeasureTheory.Measure.ae μ] g) : MeasureTheory.AEStronglyMeasurable g μ

theorem aestronglyMeasurable_congr {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} {g : α → β} (h : f =ᶠ[MeasureTheory.Measure.ae μ] g) : MeasureTheory.AEStronglyMeasurable f μ ↔ MeasureTheory.AEStronglyMeasurable g μ

theorem MeasureTheory.AEStronglyMeasurable.mono_measure {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} {ν : MeasureTheory.Measure α} (hf : MeasureTheory.AEStronglyMeasurable f μ) (h : ν ≤ μ) : MeasureTheory.AEStronglyMeasurable f ν

theorem MeasureTheory.AEStronglyMeasurable.mono' {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} {ν : MeasureTheory.Measure α} (h : MeasureTheory.AEStronglyMeasurable f μ) (h' : MeasureTheory.Measure.AbsolutelyContinuous ν μ) : MeasureTheory.AEStronglyMeasurable f ν

theorem MeasureTheory.AEStronglyMeasurable.mono_set {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} {s : Set α} {t : Set α} (h : s ⊆ t) (ht : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.restrict μ t)) : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.restrict μ s)

theorem MeasureTheory.AEStronglyMeasurable.restrict {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} (hfm : MeasureTheory.AEStronglyMeasurable f μ) {s : Set α} : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.restrict μ s)

theorem MeasureTheory.AEStronglyMeasurable.ae_mem_imp_eq_mk {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} {s : Set α} (h : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.restrict μ s)) : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = MeasureTheory.AEStronglyMeasurable.mk f h x

theorem Continuous.comp_aestronglyMeasurable {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] [TopologicalSpace γ] {g : β → γ} {f : α → β} (hg : Continuous g) (hf : MeasureTheory.AEStronglyMeasurable f μ) : MeasureTheory.AEStronglyMeasurable (fun (x : α) => g (f x)) μ

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

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

theorem MeasureTheory.AEStronglyMeasurable.prod_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] [TopologicalSpace γ] {f : α → β} {g : α → γ} (hf : MeasureTheory.AEStronglyMeasurable f μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) : MeasureTheory.AEStronglyMeasurable (fun (x : α) => (f x, g x)) μ

theorem Measurable.aestronglyMeasurable {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {f : α → β} : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasurableSpace β] [inst_1 : TopologicalSpace.PseudoMetrizableSpace β] [inst_2 : SecondCountableTopology β] [inst_3 : OpensMeasurableSpace β], Measurable f → MeasureTheory.AEStronglyMeasurable f μ

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

theorem MeasureTheory.AEStronglyMeasurable.add {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} {g : α → β} [Add β] [ContinuousAdd β] (hf : MeasureTheory.AEStronglyMeasurable f μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) : MeasureTheory.AEStronglyMeasurable (f + g) μ

theorem MeasureTheory.AEStronglyMeasurable.mul {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} {g : α → β} [Mul β] [ContinuousMul β] (hf : MeasureTheory.AEStronglyMeasurable f μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) : MeasureTheory.AEStronglyMeasurable (f * g) μ

theorem MeasureTheory.AEStronglyMeasurable.add_const {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} [Add β] [ContinuousAdd β] (hf : MeasureTheory.AEStronglyMeasurable f μ) (c : β) : MeasureTheory.AEStronglyMeasurable (fun (x : α) => f x + c) μ

theorem MeasureTheory.AEStronglyMeasurable.mul_const {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} [Mul β] [ContinuousMul β] (hf : MeasureTheory.AEStronglyMeasurable f μ) (c : β) : MeasureTheory.AEStronglyMeasurable (fun (x : α) => f x * c) μ

theorem MeasureTheory.AEStronglyMeasurable.const_add {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} [Add β] [ContinuousAdd β] (hf : MeasureTheory.AEStronglyMeasurable f μ) (c : β) : MeasureTheory.AEStronglyMeasurable (fun (x : α) => c + f x) μ

theorem MeasureTheory.AEStronglyMeasurable.const_mul {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} [Mul β] [ContinuousMul β] (hf : MeasureTheory.AEStronglyMeasurable f μ) (c : β) : MeasureTheory.AEStronglyMeasurable (fun (x : α) => c * f x) μ

theorem MeasureTheory.AEStronglyMeasurable.neg {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} [Neg β] [ContinuousNeg β] (hf : MeasureTheory.AEStronglyMeasurable f μ) : MeasureTheory.AEStronglyMeasurable (-f) μ

theorem MeasureTheory.AEStronglyMeasurable.inv {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} [Inv β] [ContinuousInv β] (hf : MeasureTheory.AEStronglyMeasurable f μ) : MeasureTheory.AEStronglyMeasurable f⁻¹ μ

theorem MeasureTheory.AEStronglyMeasurable.sub {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} {g : α → β} [AddGroup β] [TopologicalAddGroup β] (hf : MeasureTheory.AEStronglyMeasurable f μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) : MeasureTheory.AEStronglyMeasurable (f - g) μ

theorem MeasureTheory.AEStronglyMeasurable.div {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} {g : α → β} [Group β] [TopologicalGroup β] (hf : MeasureTheory.AEStronglyMeasurable f μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) : MeasureTheory.AEStronglyMeasurable (f / g) μ

theorem MeasureTheory.AEStronglyMeasurable.vadd {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {𝕜 : Type u_5} [TopologicalSpace 𝕜] [VAdd 𝕜 β] [ContinuousVAdd 𝕜 β] {f : α → 𝕜} {g : α → β} (hf : MeasureTheory.AEStronglyMeasurable f μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) : MeasureTheory.AEStronglyMeasurable (fun (x : α) => f x +ᵥ g x) μ

theorem MeasureTheory.AEStronglyMeasurable.smul {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {𝕜 : Type u_5} [TopologicalSpace 𝕜] [SMul 𝕜 β] [ContinuousSMul 𝕜 β] {f : α → 𝕜} {g : α → β} (hf : MeasureTheory.AEStronglyMeasurable f μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) : MeasureTheory.AEStronglyMeasurable (fun (x : α) => f x • g x) μ

theorem MeasureTheory.AEStronglyMeasurable.const_nsmul {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} [AddMonoid β] [ContinuousAdd β] (hf : MeasureTheory.AEStronglyMeasurable f μ) (n : ℕ) : MeasureTheory.AEStronglyMeasurable (n • f) μ

theorem MeasureTheory.AEStronglyMeasurable.pow {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} [Monoid β] [ContinuousMul β] (hf : MeasureTheory.AEStronglyMeasurable f μ) (n : ℕ) : MeasureTheory.AEStronglyMeasurable (f ^ n) μ

theorem MeasureTheory.AEStronglyMeasurable.const_vadd {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} {𝕜 : Type u_5} [VAdd 𝕜 β] [ContinuousConstVAdd 𝕜 β] (hf : MeasureTheory.AEStronglyMeasurable f μ) (c : 𝕜) : MeasureTheory.AEStronglyMeasurable (c +ᵥ f) μ

theorem MeasureTheory.AEStronglyMeasurable.const_smul {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} {𝕜 : Type u_5} [SMul 𝕜 β] [ContinuousConstSMul 𝕜 β] (hf : MeasureTheory.AEStronglyMeasurable f μ) (c : 𝕜) : MeasureTheory.AEStronglyMeasurable (c • f) μ

theorem MeasureTheory.AEStronglyMeasurable.const_vadd' {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} {𝕜 : Type u_5} [VAdd 𝕜 β] [ContinuousConstVAdd 𝕜 β] (hf : MeasureTheory.AEStronglyMeasurable f μ) (c : 𝕜) : MeasureTheory.AEStronglyMeasurable (fun (x : α) => c +ᵥ f x) μ

theorem MeasureTheory.AEStronglyMeasurable.const_smul' {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} {𝕜 : Type u_5} [SMul 𝕜 β] [ContinuousConstSMul 𝕜 β] (hf : MeasureTheory.AEStronglyMeasurable f μ) (c : 𝕜) : MeasureTheory.AEStronglyMeasurable (fun (x : α) => c • f x) μ

theorem MeasureTheory.AEStronglyMeasurable.vadd_const {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {𝕜 : Type u_5} [TopologicalSpace 𝕜] [VAdd 𝕜 β] [ContinuousVAdd 𝕜 β] {f : α → 𝕜} (hf : MeasureTheory.AEStronglyMeasurable f μ) (c : β) : MeasureTheory.AEStronglyMeasurable (fun (x : α) => f x +ᵥ c) μ

theorem MeasureTheory.AEStronglyMeasurable.smul_const {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {𝕜 : Type u_5} [TopologicalSpace 𝕜] [SMul 𝕜 β] [ContinuousSMul 𝕜 β] {f : α → 𝕜} (hf : MeasureTheory.AEStronglyMeasurable f μ) (c : β) : MeasureTheory.AEStronglyMeasurable (fun (x : α) => f x • c) μ

theorem MeasureTheory.AEStronglyMeasurable.sup {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} {g : α → β} [SemilatticeSup β] [ContinuousSup β] (hf : MeasureTheory.AEStronglyMeasurable f μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) : MeasureTheory.AEStronglyMeasurable (f ⊔ g) μ

theorem MeasureTheory.AEStronglyMeasurable.inf {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} {g : α → β} [SemilatticeInf β] [ContinuousInf β] (hf : MeasureTheory.AEStronglyMeasurable f μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) : MeasureTheory.AEStronglyMeasurable (f ⊓ g) μ

Big operators: ∏ and ∑

theorem List.aestronglyMeasurable_sum' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {M : Type u_5} [AddMonoid M] [TopologicalSpace M] [ContinuousAdd M] (l : List (α → M)) (hl : ∀ f ∈ l, MeasureTheory.AEStronglyMeasurable f μ) : MeasureTheory.AEStronglyMeasurable (List.sum l) μ

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 (List.prod l) μ

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 (fun (x : α) => List.sum (List.map (fun (f : α → M) => f x) l)) μ

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 (fun (x : α) => List.prod (List.map (fun (f : α → M) => f x) l)) μ

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 (Multiset.sum l) μ

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 (Multiset.prod l) μ

theorem Multiset.aestronglyMeasurable_sum {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {M : Type u_5} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] (s : Multiset (α → M)) (hs : ∀ f ∈ s, MeasureTheory.AEStronglyMeasurable f μ) : MeasureTheory.AEStronglyMeasurable (fun (x : α) => Multiset.sum (Multiset.map (fun (f : α → M) => f x) s)) μ

theorem Multiset.aestronglyMeasurable_prod {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {M : Type u_5} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] (s : Multiset (α → M)) (hs : ∀ f ∈ s, MeasureTheory.AEStronglyMeasurable f μ) : MeasureTheory.AEStronglyMeasurable (fun (x : α) => Multiset.prod (Multiset.map (fun (f : α → M) => f x) s)) μ

abbrev Finset.aestronglyMeasurable_sum'.match_1 {α : Type u_2} {M : Type u_3} {ι : Type u_1} {f : ι → α → M} (s : Finset ι) (_g : α → M) (motive : (∃ a ∈ s.val, f a = _g) → Prop) : ∀ (x : ∃ a ∈ s.val, f a = _g), (∀ (_i : ι) (hi : _i ∈ s.val) (hg : f _i = _g), motive (_ : ∃ a ∈ s.val, f a = _g)) → motive x

Equations

• (_ : motive x) = (_ : motive x)

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 (Finset.sum s fun (i : ι) => f i) μ

theorem Finset.aestronglyMeasurable_prod' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {M : Type u_5} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] {ι : Type u_6} {f : ι → α → M} (s : Finset ι) (hf : ∀ i ∈ s, MeasureTheory.AEStronglyMeasurable (f i) μ) : MeasureTheory.AEStronglyMeasurable (Finset.prod s fun (i : ι) => 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 (fun (a : α) => Finset.sum s fun (i : ι) => f i a) μ

theorem Finset.aestronglyMeasurable_prod {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {M : Type u_5} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] {ι : Type u_6} {f : ι → α → M} (s : Finset ι) (hf : ∀ i ∈ s, MeasureTheory.AEStronglyMeasurable (f i) μ) : MeasureTheory.AEStronglyMeasurable (fun (a : α) => Finset.prod s fun (i : ι) => f i a) μ

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

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

theorem aestronglyMeasurable_id {α : Type u_5} [TopologicalSpace α] [TopologicalSpace.PseudoMetrizableSpace α] : ∀ {x : MeasurableSpace α} [inst : OpensMeasurableSpace α] [inst : SecondCountableTopology α] {μ : MeasureTheory.Measure α}, MeasureTheory.AEStronglyMeasurable id μ

theorem aestronglyMeasurable_iff_aemeasurable {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} [MeasurableSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [BorelSpace β] [SecondCountableTopology β] : MeasureTheory.AEStronglyMeasurable f μ ↔ AEMeasurable f

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

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

theorem MeasureTheory.AEStronglyMeasurable.norm {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_5} [SeminormedAddCommGroup β] {f : α → β} (hf : MeasureTheory.AEStronglyMeasurable f μ) : MeasureTheory.AEStronglyMeasurable (fun (x : α) => ‖f x‖) μ

theorem MeasureTheory.AEStronglyMeasurable.nnnorm {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_5} [SeminormedAddCommGroup β] {f : α → β} (hf : MeasureTheory.AEStronglyMeasurable f μ) : MeasureTheory.AEStronglyMeasurable (fun (x : α) => ‖f x‖₊) μ

theorem MeasureTheory.AEStronglyMeasurable.ennnorm {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_5} [SeminormedAddCommGroup β] {f : α → β} (hf : MeasureTheory.AEStronglyMeasurable f μ) : AEMeasurable fun (a : α) => ↑‖f a‖₊

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

theorem MeasureTheory.AEStronglyMeasurable.real_toNNReal {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : MeasureTheory.AEStronglyMeasurable f μ) : MeasureTheory.AEStronglyMeasurable (fun (x : α) => Real.toNNReal (f x)) μ

theorem aestronglyMeasurable_indicator_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} [Zero β] {s : Set α} (hs : MeasurableSet s) : MeasureTheory.AEStronglyMeasurable (Set.indicator s f) μ ↔ MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.restrict μ s)

theorem MeasureTheory.AEStronglyMeasurable.indicator {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} [Zero β] (hfm : MeasureTheory.AEStronglyMeasurable f μ) {s : Set α} (hs : MeasurableSet s) : MeasureTheory.AEStronglyMeasurable (Set.indicator s f) μ

theorem MeasureTheory.AEStronglyMeasurable.nullMeasurableSet_eq_fun {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_5} [TopologicalSpace E] [TopologicalSpace.MetrizableSpace E] {f : α → E} {g : α → E} (hf : MeasureTheory.AEStronglyMeasurable f μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) : MeasureTheory.NullMeasurableSet {x : α | f x = g x}

theorem MeasureTheory.AEStronglyMeasurable.nullMeasurableSet_support {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_5} [TopologicalSpace E] [TopologicalSpace.MetrizableSpace E] [Zero E] {f : α → E} (hf : MeasureTheory.AEStronglyMeasurable f μ) : MeasureTheory.NullMeasurableSet (Function.support f)

theorem MeasureTheory.AEStronglyMeasurable.nullMeasurableSet_mulSupport {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_5} [TopologicalSpace E] [TopologicalSpace.MetrizableSpace E] [One E] {f : α → E} (hf : MeasureTheory.AEStronglyMeasurable f μ) : MeasureTheory.NullMeasurableSet (Function.mulSupport f)

theorem MeasureTheory.AEStronglyMeasurable.nullMeasurableSet_lt {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] [LinearOrder β] [OrderClosedTopology β] [TopologicalSpace.PseudoMetrizableSpace β] {f : α → β} {g : α → β} (hf : MeasureTheory.AEStronglyMeasurable f μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) : MeasureTheory.NullMeasurableSet {a : α | f a < g a}

theorem MeasureTheory.AEStronglyMeasurable.nullMeasurableSet_le {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] [Preorder β] [OrderClosedTopology β] [TopologicalSpace.PseudoMetrizableSpace β] {f : α → β} {g : α → β} (hf : MeasureTheory.AEStronglyMeasurable f μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) : MeasureTheory.NullMeasurableSet {a : α | f a ≤ g a}

theorem aestronglyMeasurable_of_aestronglyMeasurable_trim {β : Type u_2} [TopologicalSpace β] {α : Type u_5} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) {f : α → β} (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.trim μ hm)) : MeasureTheory.AEStronglyMeasurable f μ

theorem MeasureTheory.AEStronglyMeasurable.comp_aemeasurable {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {g : α → β} {γ : Type u_5} : ∀ {x : MeasurableSpace γ} {x_1 : MeasurableSpace α} {f : γ → α} {μ : MeasureTheory.Measure γ}, MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ) → AEMeasurable f → MeasureTheory.AEStronglyMeasurable (g ∘ f) μ

theorem MeasureTheory.AEStronglyMeasurable.comp_measurable {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {g : α → β} {γ : Type u_5} : ∀ {x : MeasurableSpace γ} {x_1 : MeasurableSpace α} {f : γ → α} {μ : MeasureTheory.Measure γ}, MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ) → Measurable f → MeasureTheory.AEStronglyMeasurable (g ∘ f) μ

theorem MeasureTheory.AEStronglyMeasurable.comp_quasiMeasurePreserving {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {g : α → β} {γ : Type u_5} : ∀ {x : MeasurableSpace γ} {x_1 : MeasurableSpace α} {f : γ → α} {μ : MeasureTheory.Measure γ} {ν : MeasureTheory.Measure α}, MeasureTheory.AEStronglyMeasurable g ν → MeasureTheory.Measure.QuasiMeasurePreserving f → MeasureTheory.AEStronglyMeasurable (g ∘ f) μ

theorem MeasureTheory.AEStronglyMeasurable.comp_measurePreserving {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {g : α → β} {γ : Type u_5} : ∀ {x : MeasurableSpace γ} {x_1 : MeasurableSpace α} {f : γ → α} {μ : MeasureTheory.Measure γ} {ν : MeasureTheory.Measure α}, MeasureTheory.AEStronglyMeasurable g ν → MeasureTheory.MeasurePreserving f → MeasureTheory.AEStronglyMeasurable (g ∘ f) μ

theorem MeasureTheory.AEStronglyMeasurable.isSeparable_ae_range {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} (hf : MeasureTheory.AEStronglyMeasurable f μ) : ∃ (t : Set β), TopologicalSpace.IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t

theorem aestronglyMeasurable_iff_aemeasurable_separable {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {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} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {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 : α → β} : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ) ↔ MeasureTheory.AEStronglyMeasurable (g ∘ f) μ

theorem Embedding.aestronglyMeasurable_comp_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace.PseudoMetrizableSpace β] [TopologicalSpace.PseudoMetrizableSpace γ] {g : β → γ} {f : α → β} (hg : Embedding g) : MeasureTheory.AEStronglyMeasurable (fun (x : α) => g (f x)) μ ↔ MeasureTheory.AEStronglyMeasurable f μ

theorem MeasureTheory.MeasurePreserving.aestronglyMeasurable_comp_iff {α : Type u_1} {γ : Type u_3} [TopologicalSpace γ] {β : Type u_5} {f : α → β} {mα : MeasurableSpace α} {μa : MeasureTheory.Measure α} {mβ : MeasurableSpace β} {μb : MeasureTheory.Measure β} (hf : MeasureTheory.MeasurePreserving f) (h₂ : MeasurableEmbedding f) {g : β → γ} : MeasureTheory.AEStronglyMeasurable (g ∘ f) μa ↔ MeasureTheory.AEStronglyMeasurable g μb

theorem aestronglyMeasurable_of_tendsto_ae {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {ι : Type u_5} [TopologicalSpace.PseudoMetrizableSpace β] (u : Filter ι) [Filter.NeBot u] [Filter.IsCountablyGenerated u] {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.

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

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

theorem MeasureTheory.AEStronglyMeasurable.piecewise {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} {g : α → β} {s : Set α} [DecidablePred fun (x : α) => x ∈ s] (hs : MeasurableSet s) (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.restrict μ s)) (hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.restrict μ sᶜ)) : MeasureTheory.AEStronglyMeasurable (Set.piecewise s f g) μ

theorem MeasureTheory.AEStronglyMeasurable.sum_measure {α : Type u_1} {β : Type u_2} {ι : Type u_4} [Countable ι] [TopologicalSpace β] {f : α → β} [TopologicalSpace.PseudoMetrizableSpace β] {m : MeasurableSpace α} {μ : ι → MeasureTheory.Measure α} (h : ∀ (i : ι), MeasureTheory.AEStronglyMeasurable f (μ i)) : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.sum μ)

@[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} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} [TopologicalSpace.PseudoMetrizableSpace β] {ν : MeasureTheory.Measure α} : MeasureTheory.AEStronglyMeasurable f (μ + ν) ↔ MeasureTheory.AEStronglyMeasurable f μ ∧ MeasureTheory.AEStronglyMeasurable f ν

theorem MeasureTheory.AEStronglyMeasurable.add_measure {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] {ν : MeasureTheory.Measure α} {f : α → β} (hμ : MeasureTheory.AEStronglyMeasurable f μ) (hν : MeasureTheory.AEStronglyMeasurable f ν) : MeasureTheory.AEStronglyMeasurable f (μ + ν)

theorem MeasureTheory.AEStronglyMeasurable.iUnion {α : Type u_1} {β : Type u_2} {ι : Type u_4} [Countable ι] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} [TopologicalSpace.PseudoMetrizableSpace β] {s : ι → Set α} (h : ∀ (i : ι), MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.restrict μ (s i))) : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.restrict μ (⋃ (i : ι), s i))

@[simp]

theorem aestronglyMeasurable_iUnion_iff {α : Type u_1} {β : Type u_2} {ι : Type u_4} [Countable ι] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} [TopologicalSpace.PseudoMetrizableSpace β] {s : ι → Set α} : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.restrict μ (⋃ (i : ι), s i)) ↔ ∀ (i : ι), MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.restrict μ (s i))

@[simp]

theorem aestronglyMeasurable_union_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} [TopologicalSpace.PseudoMetrizableSpace β] {s : Set α} {t : Set α} : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.restrict μ (s ∪ t)) ↔ MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.restrict μ s) ∧ MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.restrict μ t)

theorem MeasureTheory.AEStronglyMeasurable.aestronglyMeasurable_uIoc_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] [LinearOrder α] [TopologicalSpace.PseudoMetrizableSpace β] {f : α → β} {a : α} {b : α} : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.restrict μ (Ι a b)) ↔ MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.restrict μ (Set.Ioc a b)) ∧ MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.restrict μ (Set.Ioc b a))

theorem MeasureTheory.AEStronglyMeasurable.smul_measure {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} {R : Type u_5} [Monoid R] [DistribMulAction R ENNReal] [IsScalarTower R ENNReal ENNReal] (h : MeasureTheory.AEStronglyMeasurable f μ) (c : R) : MeasureTheory.AEStronglyMeasurable f (c • μ)

theorem aestronglyMeasurable_smul_const_iff {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_5} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : α → 𝕜} {c : E} (hc : c ≠ 0) : MeasureTheory.AEStronglyMeasurable (fun (x : α) => f x • c) μ ↔ MeasureTheory.AEStronglyMeasurable f μ

theorem aestronglyMeasurable_const_smul_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} {G : Type u_6} [Group G] [MulAction G β] [ContinuousConstSMul G β] (c : G) : MeasureTheory.AEStronglyMeasurable (fun (x : α) => c • f x) μ ↔ MeasureTheory.AEStronglyMeasurable f μ

theorem IsUnit.aestronglyMeasurable_const_smul_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} {M : Type u_5} [Monoid M] [MulAction M β] [ContinuousConstSMul M β] {c : M} (hc : IsUnit c) : MeasureTheory.AEStronglyMeasurable (fun (x : α) => c • f x) μ ↔ MeasureTheory.AEStronglyMeasurable f μ

theorem aestronglyMeasurable_const_smul_iff₀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} {G₀ : Type u_7} [GroupWithZero G₀] [MulAction G₀ β] [ContinuousConstSMul G₀ β] {c : G₀} (hc : c ≠ 0) : MeasureTheory.AEStronglyMeasurable (fun (x : α) => c • f x) μ ↔ MeasureTheory.AEStronglyMeasurable f μ

theorem StronglyMeasurable.apply_continuousLinearMap {α : Type u_1} {𝕜 : Type u_5} [NontriviallyNormedField 𝕜] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_7} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {_m : MeasurableSpace α} {φ : α → F →L[𝕜] E} (hφ : MeasureTheory.StronglyMeasurable φ) (v : F) : MeasureTheory.StronglyMeasurable fun (a : α) => (φ a) v

theorem MeasureTheory.AEStronglyMeasurable.apply_continuousLinearMap {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_5} [NontriviallyNormedField 𝕜] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_7} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {φ : α → F →L[𝕜] E} (hφ : MeasureTheory.AEStronglyMeasurable φ μ) (v : F) : MeasureTheory.AEStronglyMeasurable (fun (a : α) => (φ a) v) μ

theorem ContinuousLinearMap.aestronglyMeasurable_comp₂ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_5} [NontriviallyNormedField 𝕜] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_7} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_8} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (L : E →L[𝕜] F →L[𝕜] G) {f : α → E} {g : α → F} (hf : MeasureTheory.AEStronglyMeasurable f μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) : MeasureTheory.AEStronglyMeasurable (fun (x : α) => (L (f x)) (g x)) μ

theorem aestronglyMeasurable_withDensity_iff {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : α → NNReal} (hf : Measurable f) {g : α → E} : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.withDensity μ fun (x : α) => ↑(f x)) ↔ MeasureTheory.AEStronglyMeasurable (fun (x : α) => ↑(f x) • g x) μ

Almost everywhere finitely strongly measurable functions

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

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

Equations

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

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

theorem MeasureTheory.AEFinStronglyMeasurable.ae_eq_mk {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} [Zero β] (hf : MeasureTheory.AEFinStronglyMeasurable f μ) : f =ᶠ[MeasureTheory.Measure.ae μ] MeasureTheory.AEFinStronglyMeasurable.mk f hf

theorem MeasureTheory.AEFinStronglyMeasurable.aemeasurable {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_5} [Zero β] [MeasurableSpace β] [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [BorelSpace β] {f : α → β} (hf : MeasureTheory.AEFinStronglyMeasurable f μ) : AEMeasurable f

theorem MeasureTheory.AEFinStronglyMeasurable.mul {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} {g : α → β} [MonoidWithZero β] [ContinuousMul β] (hf : MeasureTheory.AEFinStronglyMeasurable f μ) (hg : MeasureTheory.AEFinStronglyMeasurable g μ) : MeasureTheory.AEFinStronglyMeasurable (f * g) μ

theorem MeasureTheory.AEFinStronglyMeasurable.add {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} {g : α → β} [AddMonoid β] [ContinuousAdd β] (hf : MeasureTheory.AEFinStronglyMeasurable f μ) (hg : MeasureTheory.AEFinStronglyMeasurable g μ) : MeasureTheory.AEFinStronglyMeasurable (f + g) μ

theorem MeasureTheory.AEFinStronglyMeasurable.neg {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} [AddGroup β] [TopologicalAddGroup β] (hf : MeasureTheory.AEFinStronglyMeasurable f μ) : MeasureTheory.AEFinStronglyMeasurable (-f) μ

theorem MeasureTheory.AEFinStronglyMeasurable.sub {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} {g : α → β} [AddGroup β] [ContinuousSub β] (hf : MeasureTheory.AEFinStronglyMeasurable f μ) (hg : MeasureTheory.AEFinStronglyMeasurable g μ) : MeasureTheory.AEFinStronglyMeasurable (f - g) μ

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

theorem MeasureTheory.AEFinStronglyMeasurable.sup {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} {g : α → β} [Zero β] [SemilatticeSup β] [ContinuousSup β] (hf : MeasureTheory.AEFinStronglyMeasurable f μ) (hg : MeasureTheory.AEFinStronglyMeasurable g μ) : MeasureTheory.AEFinStronglyMeasurable (f ⊔ g) μ

theorem MeasureTheory.AEFinStronglyMeasurable.inf {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} {g : α → β} [Zero β] [SemilatticeInf β] [ContinuousInf β] (hf : MeasureTheory.AEFinStronglyMeasurable f μ) (hg : MeasureTheory.AEFinStronglyMeasurable g μ) : MeasureTheory.AEFinStronglyMeasurable (f ⊓ g) μ

theorem MeasureTheory.AEFinStronglyMeasurable.exists_set_sigmaFinite {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} [Zero β] [T2Space β] (hf : MeasureTheory.AEFinStronglyMeasurable f μ) : ∃ (t : Set α), MeasurableSet t ∧ f =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ tᶜ)] 0 ∧ MeasureTheory.SigmaFinite (MeasureTheory.Measure.restrict μ t)

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

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

Equations

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

theorem MeasureTheory.AEFinStronglyMeasurable.measurableSet {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} [Zero β] [T2Space β] (hf : MeasureTheory.AEFinStronglyMeasurable f μ) : MeasurableSet (MeasureTheory.AEFinStronglyMeasurable.sigmaFiniteSet hf)

theorem MeasureTheory.AEFinStronglyMeasurable.ae_eq_zero_compl {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} [Zero β] [T2Space β] (hf : MeasureTheory.AEFinStronglyMeasurable f μ) : f =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ (MeasureTheory.AEFinStronglyMeasurable.sigmaFiniteSet hf)ᶜ)] 0

instance MeasureTheory.AEFinStronglyMeasurable.sigmaFinite_restrict {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace β] {f : α → β} [Zero β] [T2Space β] (hf : MeasureTheory.AEFinStronglyMeasurable f μ) : MeasureTheory.SigmaFinite (MeasureTheory.Measure.restrict μ (MeasureTheory.AEFinStronglyMeasurable.sigmaFiniteSet hf))

Equations

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

theorem MeasureTheory.finStronglyMeasurable_iff_measurable {α : Type u_1} {G : Type u_5} [SeminormedAddCommGroup G] [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G] {f : α → G} {_m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] : MeasureTheory.FinStronglyMeasurable f μ ↔ Measurable f

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

theorem MeasureTheory.finStronglyMeasurable_of_measurable {α : Type u_1} {G : Type u_5} [SeminormedAddCommGroup G] [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G] {f : α → G} {_m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] (hf : Measurable f) : MeasureTheory.FinStronglyMeasurable f μ

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

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

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 α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] (hf : AEMeasurable f) : MeasureTheory.AEFinStronglyMeasurable f μ

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

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

theorem MeasureTheory.stronglyMeasurable_uncurry_of_continuous_of_stronglyMeasurable {α : Type u_5} {β : Type u_6} {ι : Type u_7} [TopologicalSpace ι] [TopologicalSpace.MetrizableSpace ι] [MeasurableSpace ι] [SecondCountableTopology ι] [OpensMeasurableSpace ι] [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [MeasurableSpace α] {u : ι → α → β} (hu_cont : ∀ (x : α), Continuous fun (i : ι) => u i x) (h : ∀ (i : ι), MeasureTheory.StronglyMeasurable (u i)) : MeasureTheory.StronglyMeasurable (Function.uncurry u)