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.
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.
We provide a solid API for strongly measurable functions, as a basis for the Bochner integral.
Main definitions #
StronglyMeasurable f:f : α → βis the limit of a sequencefs : ℕ → SimpleFunc α β.FinStronglyMeasurable f μ:f : α → βis the limit of a sequencefs : ℕ → SimpleFunc α βsuch that for alln ∈ ℕ, the measure of the support offs nis finite.
References #
- [Hytönen, Tuomas, Jan Van Neerven, Mark Veraar, and Lutz Weis. Analysis in Banach spaces. Springer, 2016.][Hytönen_VanNeerven_Veraar_Wies_2016]
def
MeasureTheory.StronglyMeasurable
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
[MeasurableSpace α]
(f : α → β)
:
A function is StronglyMeasurable if it is the limit of simple functions.
Equations
- MeasureTheory.StronglyMeasurable f = ∃ (fs : ℕ → MeasureTheory.SimpleFunc α β), ∀ (x : α), Filter.Tendsto (fun (n : ℕ) => (fs n) x) Filter.atTop (nhds (f x))
Instances For
The notation for StronglyMeasurable giving the measurable space instance explicitly.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
MeasureTheory.FinStronglyMeasurable
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
[Zero β]
{x✝ : MeasurableSpace α}
(f : α → β)
(μ : Measure α := by volume_tac)
:
A function is FinStronglyMeasurable with respect to a measure if it is the limit of simple
functions with support with finite measure.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Strongly measurable functions #
@[simp]
theorem
MeasureTheory.Subsingleton.stronglyMeasurable
{α : Type u_1}
{β : Type u_2}
{x✝ : MeasurableSpace α}
[TopologicalSpace β]
[Subsingleton β]
(f : α → β)
:
theorem
MeasureTheory.SimpleFunc.stronglyMeasurable
{α : Type u_1}
{β : Type u_2}
{x✝ : MeasurableSpace α}
[TopologicalSpace β]
(f : SimpleFunc α β)
:
theorem
MeasureTheory.StronglyMeasurable.of_finite
{α : Type u_1}
{β : Type u_2}
{x✝ : MeasurableSpace α}
[TopologicalSpace β]
[Finite α]
[MeasurableSingletonClass α]
{f : α → β}
:
theorem
MeasureTheory.stronglyMeasurable_const
{α : Type u_1}
{β : Type u_2}
{x✝ : MeasurableSpace α}
[TopologicalSpace β]
{b : β}
:
StronglyMeasurable fun (x : α) => b
theorem
MeasureTheory.stronglyMeasurable_one
{α : Type u_1}
{β : Type u_2}
{x✝ : MeasurableSpace α}
[TopologicalSpace β]
[One β]
:
theorem
MeasureTheory.stronglyMeasurable_zero
{α : Type u_1}
{β : Type u_2}
{x✝ : MeasurableSpace α}
[TopologicalSpace β]
[Zero β]
:
theorem
MeasureTheory.stronglyMeasurable_const'
{α : Type u_1}
{β : Type u_2}
{x✝ : MeasurableSpace α}
[TopologicalSpace β]
{f : α → β}
(hf : ∀ (x y : α), f x = f y)
:
A version of stronglyMeasurable_const that assumes f x = f y for all x, y.
This version works for functions between empty types.
@[simp]
theorem
MeasureTheory.Subsingleton.stronglyMeasurable'
{α : Type u_1}
{β : Type u_2}
{x✝ : MeasurableSpace α}
[TopologicalSpace β]
[Subsingleton α]
(f : α → β)
:
noncomputable def
MeasureTheory.StronglyMeasurable.approx
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[TopologicalSpace β]
{x✝ : MeasurableSpace α}
(hf : StronglyMeasurable f)
:
ℕ → 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
- hf.approx = Exists.choose hf
Instances For
theorem
MeasureTheory.StronglyMeasurable.tendsto_approx
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[TopologicalSpace β]
{x✝ : MeasurableSpace α}
(hf : StronglyMeasurable f)
(x : α)
:
Filter.Tendsto (fun (n : ℕ) => (hf.approx n) x) Filter.atTop (nhds (f x))
noncomputable def
MeasureTheory.StronglyMeasurable.approxBounded
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[TopologicalSpace β]
{x✝ : MeasurableSpace α}
[Norm β]
[SMul ℝ β]
(hf : StronglyMeasurable f)
(c : ℝ)
:
ℕ → 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
- hf.approxBounded c n = MeasureTheory.SimpleFunc.map (fun (x : β) => (1 ⊓ c / ‖x‖) • x) (hf.approx n)
Instances For
theorem
MeasureTheory.StronglyMeasurable.tendsto_approxBounded_of_norm_le
{α : Type u_1}
{β : Type u_5}
{f : α → β}
[NormedAddCommGroup β]
[NormedSpace ℝ β]
{m : MeasurableSpace α}
(hf : StronglyMeasurable f)
{c : ℝ}
{x : α}
(hfx : ‖f x‖ ≤ c)
:
Filter.Tendsto (fun (n : ℕ) => (hf.approxBounded c n) x) Filter.atTop (nhds (f x))
theorem
MeasureTheory.StronglyMeasurable.tendsto_approxBounded_ae
{α : Type u_1}
{β : Type u_5}
{f : α → β}
[NormedAddCommGroup β]
[NormedSpace ℝ β]
{m m0 : MeasurableSpace α}
{μ : Measure α}
(hf : StronglyMeasurable f)
{c : ℝ}
(hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c)
:
∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => (hf.approxBounded c n) x) Filter.atTop (nhds (f x))
theorem
MeasureTheory.StronglyMeasurable.norm_approxBounded_le
{α : Type u_1}
{β : Type u_5}
{f : α → β}
[SeminormedAddCommGroup β]
[NormedSpace ℝ β]
{m : MeasurableSpace α}
{c : ℝ}
(hf : StronglyMeasurable f)
(hc : 0 ≤ c)
(n : ℕ)
(x : α)
:
theorem
stronglyMeasurable_bot_iff
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[TopologicalSpace β]
[Nonempty β]
[T2Space β]
:
theorem
MeasureTheory.StronglyMeasurable.finStronglyMeasurable_of_set_sigmaFinite
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[TopologicalSpace β]
[Zero β]
{m : MeasurableSpace α}
{μ : Measure α}
(hf_meas : StronglyMeasurable f)
{t : Set α}
(ht : MeasurableSet t)
(hft_zero : ∀ x ∈ tᶜ, f x = 0)
(htμ : SigmaFinite (μ.restrict t))
:
theorem
MeasureTheory.StronglyMeasurable.finStronglyMeasurable
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[TopologicalSpace β]
[Zero β]
{m0 : MeasurableSpace α}
(hf : StronglyMeasurable f)
(μ : Measure α)
[SigmaFinite μ]
:
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 α}
[TopologicalSpace β]
[TopologicalSpace.PseudoMetrizableSpace β]
[MeasurableSpace β]
[BorelSpace β]
(hf : StronglyMeasurable f)
:
A strongly measurable function is measurable.
theorem
MeasureTheory.StronglyMeasurable.aemeasurable
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{x✝ : MeasurableSpace α}
[TopologicalSpace β]
[TopologicalSpace.PseudoMetrizableSpace β]
[MeasurableSpace β]
[BorelSpace β]
{μ : Measure α}
(hf : 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 α}
[TopologicalSpace β]
[TopologicalSpace γ]
{g : β → γ}
{f : α → β}
(hg : Continuous g)
(hf : MeasureTheory.StronglyMeasurable f)
:
MeasureTheory.StronglyMeasurable fun (x : α) => g (f x)
theorem
MeasureTheory.StronglyMeasurable.measurableSet_mulSupport
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{m : MeasurableSpace α}
[One β]
[TopologicalSpace β]
[TopologicalSpace.MetrizableSpace β]
(hf : StronglyMeasurable f)
:
theorem
MeasureTheory.StronglyMeasurable.measurableSet_support
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{m : MeasurableSpace α}
[Zero β]
[TopologicalSpace β]
[TopologicalSpace.MetrizableSpace β]
(hf : StronglyMeasurable f)
:
theorem
MeasureTheory.StronglyMeasurable.mono
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{m m' : MeasurableSpace α}
[TopologicalSpace β]
(hf : StronglyMeasurable f)
(h_mono : m' ≤ m)
:
theorem
MeasureTheory.StronglyMeasurable.prod_mk
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m : MeasurableSpace α}
[TopologicalSpace β]
[TopologicalSpace γ]
{f : α → β}
{g : α → γ}
(hf : StronglyMeasurable f)
(hg : StronglyMeasurable g)
:
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✝¹ : MeasurableSpace γ}
{f : α → β}
{g : γ → α}
(hf : StronglyMeasurable f)
(hg : Measurable g)
:
StronglyMeasurable (f ∘ g)
theorem
MeasureTheory.StronglyMeasurable.of_uncurry_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[TopologicalSpace β]
{x✝ : MeasurableSpace α}
{x✝¹ : MeasurableSpace γ}
{f : α → γ → β}
(hf : StronglyMeasurable (Function.uncurry f))
{x : α}
:
StronglyMeasurable (f x)
theorem
MeasureTheory.StronglyMeasurable.of_uncurry_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[TopologicalSpace β]
{x✝ : MeasurableSpace α}
{x✝¹ : MeasurableSpace γ}
{f : α → γ → β}
(hf : StronglyMeasurable (Function.uncurry f))
{y : γ}
:
StronglyMeasurable fun (x : α) => f x y
theorem
MeasureTheory.StronglyMeasurable.prod_swap
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{x✝ : MeasurableSpace α}
{x✝¹ : MeasurableSpace β}
[TopologicalSpace γ]
{f : β × α → γ}
(hf : StronglyMeasurable f)
:
StronglyMeasurable fun (z : α × β) => f z.swap
theorem
MeasureTheory.StronglyMeasurable.fst
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{x✝ : MeasurableSpace α}
[mβ : MeasurableSpace β]
[TopologicalSpace γ]
{f : α → γ}
(hf : StronglyMeasurable f)
:
StronglyMeasurable fun (z : α × β) => f z.1
theorem
MeasureTheory.StronglyMeasurable.snd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[mα : MeasurableSpace α]
{x✝ : MeasurableSpace β}
[TopologicalSpace γ]
{f : β → γ}
(hf : StronglyMeasurable f)
:
StronglyMeasurable fun (z : α × β) => f z.2
theorem
MeasureTheory.StronglyMeasurable.mul
{α : Type u_1}
{β : Type u_2}
{f g : α → β}
{mα : MeasurableSpace α}
[TopologicalSpace β]
[Mul β]
[ContinuousMul β]
(hf : StronglyMeasurable f)
(hg : StronglyMeasurable g)
:
StronglyMeasurable (f * g)
theorem
MeasureTheory.StronglyMeasurable.add
{α : Type u_1}
{β : Type u_2}
{f g : α → β}
{mα : MeasurableSpace α}
[TopologicalSpace β]
[Add β]
[ContinuousAdd β]
(hf : StronglyMeasurable f)
(hg : StronglyMeasurable g)
:
StronglyMeasurable (f + g)
theorem
MeasureTheory.StronglyMeasurable.mul_const
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{mα : MeasurableSpace α}
[TopologicalSpace β]
[Mul β]
[ContinuousMul β]
(hf : StronglyMeasurable f)
(c : β)
:
StronglyMeasurable fun (x : α) => f x * c
theorem
MeasureTheory.StronglyMeasurable.add_const
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{mα : MeasurableSpace α}
[TopologicalSpace β]
[Add β]
[ContinuousAdd β]
(hf : StronglyMeasurable f)
(c : β)
:
StronglyMeasurable fun (x : α) => f x + c
theorem
MeasureTheory.StronglyMeasurable.const_mul
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{mα : MeasurableSpace α}
[TopologicalSpace β]
[Mul β]
[ContinuousMul β]
(hf : StronglyMeasurable f)
(c : β)
:
StronglyMeasurable fun (x : α) => c * f x
theorem
MeasureTheory.StronglyMeasurable.const_add
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{mα : MeasurableSpace α}
[TopologicalSpace β]
[Add β]
[ContinuousAdd β]
(hf : StronglyMeasurable f)
(c : β)
:
StronglyMeasurable fun (x : α) => c + f x
theorem
MeasureTheory.StronglyMeasurable.pow
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{mα : MeasurableSpace α}
[TopologicalSpace β]
[Monoid β]
[ContinuousMul β]
(hf : StronglyMeasurable f)
(n : ℕ)
:
StronglyMeasurable (f ^ n)
theorem
MeasureTheory.StronglyMeasurable.const_nsmul
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{mα : MeasurableSpace α}
[TopologicalSpace β]
[AddMonoid β]
[ContinuousAdd β]
(hf : StronglyMeasurable f)
(n : ℕ)
:
StronglyMeasurable (n • f)
theorem
MeasureTheory.StronglyMeasurable.inv
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{mα : MeasurableSpace α}
[TopologicalSpace β]
[Inv β]
[ContinuousInv β]
(hf : StronglyMeasurable f)
:
theorem
MeasureTheory.StronglyMeasurable.neg
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{mα : MeasurableSpace α}
[TopologicalSpace β]
[Neg β]
[ContinuousNeg β]
(hf : StronglyMeasurable f)
:
theorem
MeasureTheory.StronglyMeasurable.div
{α : Type u_1}
{β : Type u_2}
{f g : α → β}
{mα : MeasurableSpace α}
[TopologicalSpace β]
[Div β]
[ContinuousDiv β]
(hf : StronglyMeasurable f)
(hg : StronglyMeasurable g)
:
StronglyMeasurable (f / g)
theorem
MeasureTheory.StronglyMeasurable.sub
{α : Type u_1}
{β : Type u_2}
{f g : α → β}
{mα : MeasurableSpace α}
[TopologicalSpace β]
[Sub β]
[ContinuousSub β]
(hf : StronglyMeasurable f)
(hg : StronglyMeasurable g)
:
StronglyMeasurable (f - g)
theorem
MeasureTheory.StronglyMeasurable.mul_iff_right
{α : Type u_1}
{β : Type u_2}
{f g : α → β}
{mα : MeasurableSpace α}
[TopologicalSpace β]
[CommGroup β]
[IsTopologicalGroup β]
(hf : StronglyMeasurable f)
:
theorem
MeasureTheory.StronglyMeasurable.add_iff_right
{α : Type u_1}
{β : Type u_2}
{f g : α → β}
{mα : MeasurableSpace α}
[TopologicalSpace β]
[AddCommGroup β]
[IsTopologicalAddGroup β]
(hf : StronglyMeasurable f)
:
theorem
MeasureTheory.StronglyMeasurable.mul_iff_left
{α : Type u_1}
{β : Type u_2}
{f g : α → β}
{mα : MeasurableSpace α}
[TopologicalSpace β]
[CommGroup β]
[IsTopologicalGroup β]
(hf : StronglyMeasurable f)
:
theorem
MeasureTheory.StronglyMeasurable.add_iff_left
{α : Type u_1}
{β : Type u_2}
{f g : α → β}
{mα : MeasurableSpace α}
[TopologicalSpace β]
[AddCommGroup β]
[IsTopologicalAddGroup β]
(hf : StronglyMeasurable f)
:
theorem
MeasureTheory.StronglyMeasurable.smul
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
[TopologicalSpace β]
{𝕜 : Type u_5}
[TopologicalSpace 𝕜]
[SMul 𝕜 β]
[ContinuousSMul 𝕜 β]
{f : α → 𝕜}
{g : α → β}
(hf : StronglyMeasurable f)
(hg : StronglyMeasurable g)
:
StronglyMeasurable fun (x : α) => f x • g x
theorem
MeasureTheory.StronglyMeasurable.vadd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
[TopologicalSpace β]
{𝕜 : Type u_5}
[TopologicalSpace 𝕜]
[VAdd 𝕜 β]
[ContinuousVAdd 𝕜 β]
{f : α → 𝕜}
{g : α → β}
(hf : StronglyMeasurable f)
(hg : StronglyMeasurable g)
:
StronglyMeasurable fun (x : α) => f x +ᵥ g x
theorem
MeasureTheory.StronglyMeasurable.const_smul
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{mα : MeasurableSpace α}
[TopologicalSpace β]
{𝕜 : Type u_5}
[SMul 𝕜 β]
[ContinuousConstSMul 𝕜 β]
(hf : StronglyMeasurable f)
(c : 𝕜)
:
StronglyMeasurable (c • f)
theorem
MeasureTheory.StronglyMeasurable.const_vadd
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{mα : MeasurableSpace α}
[TopologicalSpace β]
{𝕜 : Type u_5}
[VAdd 𝕜 β]
[ContinuousConstVAdd 𝕜 β]
(hf : StronglyMeasurable f)
(c : 𝕜)
:
StronglyMeasurable (c +ᵥ f)
theorem
MeasureTheory.StronglyMeasurable.const_smul'
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{mα : MeasurableSpace α}
[TopologicalSpace β]
{𝕜 : Type u_5}
[SMul 𝕜 β]
[ContinuousConstSMul 𝕜 β]
(hf : StronglyMeasurable f)
(c : 𝕜)
:
StronglyMeasurable fun (x : α) => c • f x
theorem
MeasureTheory.StronglyMeasurable.const_vadd'
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{mα : MeasurableSpace α}
[TopologicalSpace β]
{𝕜 : Type u_5}
[VAdd 𝕜 β]
[ContinuousConstVAdd 𝕜 β]
(hf : StronglyMeasurable f)
(c : 𝕜)
:
StronglyMeasurable fun (x : α) => c +ᵥ f x
theorem
MeasureTheory.StronglyMeasurable.smul_const
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
[TopologicalSpace β]
{𝕜 : Type u_5}
[TopologicalSpace 𝕜]
[SMul 𝕜 β]
[ContinuousSMul 𝕜 β]
{f : α → 𝕜}
(hf : StronglyMeasurable f)
(c : β)
:
StronglyMeasurable fun (x : α) => f x • c
theorem
MeasureTheory.StronglyMeasurable.vadd_const
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
[TopologicalSpace β]
{𝕜 : Type u_5}
[TopologicalSpace 𝕜]
[VAdd 𝕜 β]
[ContinuousVAdd 𝕜 β]
{f : α → 𝕜}
(hf : StronglyMeasurable f)
(c : β)
:
StronglyMeasurable fun (x : α) => f x +ᵥ c
theorem
Measurable.add_stronglyMeasurable
{α : Type u_5}
{E : Type u_6}
{x✝ : MeasurableSpace α}
[AddGroup E]
[TopologicalSpace E]
[MeasurableSpace E]
[BorelSpace E]
[ContinuousAdd E]
[TopologicalSpace.PseudoMetrizableSpace E]
{g f : α → E}
(hg : Measurable g)
(hf : 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 α}
[AddCommGroup E]
[TopologicalSpace E]
[MeasurableSpace E]
[BorelSpace E]
[ContinuousAdd E]
[ContinuousNeg E]
[TopologicalSpace.PseudoMetrizableSpace E]
{g f : α → E}
(hg : Measurable g)
(hf : 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 α}
[AddGroup E]
[TopologicalSpace E]
[MeasurableSpace E]
[BorelSpace E]
[ContinuousAdd E]
[TopologicalSpace.PseudoMetrizableSpace E]
{g f : α → E}
(hg : Measurable g)
(hf : 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)
:
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}
(hc : IsUnit c)
:
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₀}
(hc : c ≠ 0)
:
theorem
MeasureTheory.StronglyMeasurable.sup
{α : Type u_1}
{β : Type u_2}
{f g : α → β}
[MeasurableSpace α]
[TopologicalSpace β]
[Max β]
[ContinuousSup β]
(hf : StronglyMeasurable f)
(hg : StronglyMeasurable g)
:
StronglyMeasurable (f ⊔ g)
theorem
MeasureTheory.StronglyMeasurable.inf
{α : Type u_1}
{β : Type u_2}
{f g : α → β}
[MeasurableSpace α]
[TopologicalSpace β]
[Min β]
[ContinuousInf β]
(hf : StronglyMeasurable f)
(hg : StronglyMeasurable g)
:
StronglyMeasurable (f ⊓ g)
Big operators: ∏ and ∑ #
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)
:
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)
:
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 : α) => (map (fun (f : α → M) => f x) l).prod
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 : α) => (map (fun (f : α → M) => f x) l).sum
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)
:
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)
:
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 : α) => (map (fun (f : α → M) => f x) s).prod
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 : α) => (map (fun (f : α → M) => f x) s).sum
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 (∏ i ∈ s, 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 (∑ i ∈ s, 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 fun (a : α) => ∏ i ∈ s, f i a
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 : α) => ∑ i ∈ s, f i a
theorem
MeasureTheory.StronglyMeasurable.isSeparable_range
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{m : MeasurableSpace α}
[TopologicalSpace β]
(hf : StronglyMeasurable 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 α}
[TopologicalSpace β]
[TopologicalSpace.PseudoMetrizableSpace β]
(hf : StronglyMeasurable f)
{b : β}
:
theorem
Measurable.stronglyMeasurable
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{mα : MeasurableSpace α}
[MeasurableSpace β]
[TopologicalSpace β]
[TopologicalSpace.PseudoMetrizableSpace β]
[SecondCountableTopology β]
[OpensMeasurableSpace β]
(hf : Measurable 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 β]
:
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 α]
:
theorem
stronglyMeasurable_iff_measurable_separable
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{m : MeasurableSpace α}
[TopologicalSpace β]
[TopologicalSpace.PseudoMetrizableSpace β]
[MeasurableSpace β]
[BorelSpace β]
:
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)
:
A continuous function is strongly measurable when either the source space or the target space is second-countable.
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)
:
A continuous function whose support is contained in a compact set is strongly measurable.
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)
:
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)
:
A continuous function with compact support 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)
:
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)
:
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 : Topology.IsEmbedding g)
:
If g is a topological embedding, then f is strongly measurable iff g ∘ f is.
theorem
stronglyMeasurable_of_tendsto
{α : Type u_1}
{β : Type u_2}
{ι : Type u_5}
{m : MeasurableSpace α}
[TopologicalSpace β]
[TopologicalSpace.PseudoMetrizableSpace β]
(u : Filter ι)
[u.NeBot]
[u.IsCountablyGenerated]
{f : ι → α → β}
{g : α → β}
(hf : ∀ (i : ι), MeasureTheory.StronglyMeasurable (f i))
(lim : Filter.Tendsto f u (nhds g))
:
A sequential limit of strongly measurable functions is strongly measurable.
theorem
MeasureTheory.StronglyMeasurable.piecewise
{α : Type u_1}
{β : Type u_2}
{f g : α → β}
{m : MeasurableSpace α}
[TopologicalSpace β]
{s : Set α}
{x✝ : DecidablePred fun (x : α) => x ∈ s}
(hs : MeasurableSet s)
(hf : StronglyMeasurable f)
(hg : StronglyMeasurable g)
:
StronglyMeasurable (s.piecewise f g)
theorem
MeasureTheory.StronglyMeasurable.ite
{α : Type u_1}
{β : Type u_2}
{f g : α → β}
{x✝ : MeasurableSpace α}
[TopologicalSpace β]
{p : α → Prop}
{x✝¹ : DecidablePred p}
(hp : MeasurableSet {a : α | p a})
(hf : StronglyMeasurable f)
(hg : StronglyMeasurable g)
:
StronglyMeasurable fun (x : α) => if p x then f x else g x
this is slightly different from StronglyMeasurable.piecewise. It can be used to show
StronglyMeasurable (ite (x=0) 0 1) by
exact StronglyMeasurable.ite (measurableSet_singleton 0) stronglyMeasurable_const stronglyMeasurable_const, but replacing StronglyMeasurable.ite by
StronglyMeasurable.piecewise in that example proof does not work.
theorem
MeasurableEmbedding.stronglyMeasurable_extend
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β}
{g : α → γ}
{g' : γ → β}
{mα : MeasurableSpace α}
{mγ : MeasurableSpace γ}
[TopologicalSpace β]
(hg : MeasurableEmbedding g)
(hf : MeasureTheory.StronglyMeasurable f)
(hg' : MeasureTheory.StronglyMeasurable g')
:
theorem
MeasurableEmbedding.exists_stronglyMeasurable_extend
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β}
{g : α → γ}
{x✝ : MeasurableSpace α}
{x✝¹ : MeasurableSpace γ}
[TopologicalSpace β]
(hg : MeasurableEmbedding g)
(hf : MeasureTheory.StronglyMeasurable f)
(hne : γ → 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 t : Set α)
(hs : MeasurableSet s)
(ht : MeasurableSet t)
(h : Set.univ ⊆ s ∪ t)
(hc : MeasureTheory.StronglyMeasurable fun (a : ↑s) => f ↑a)
(hd : MeasureTheory.StronglyMeasurable fun (a : ↑t) => f ↑a)
:
theorem
stronglyMeasurable_of_restrict_of_restrict_compl
{α : Type u_1}
{β : Type u_2}
{x✝ : MeasurableSpace α}
[TopologicalSpace β]
{f : α → β}
{s : Set α}
(hs : MeasurableSet s)
(h₁ : MeasureTheory.StronglyMeasurable (s.restrict f))
(h₂ : MeasureTheory.StronglyMeasurable (sᶜ.restrict f))
:
theorem
MeasureTheory.StronglyMeasurable.indicator
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{x✝ : MeasurableSpace α}
[TopologicalSpace β]
[Zero β]
(hf : StronglyMeasurable f)
{s : Set α}
(hs : MeasurableSet s)
:
StronglyMeasurable (s.indicator f)
theorem
MeasureTheory.StronglyMeasurable.dist
{α : Type u_1}
{x✝ : MeasurableSpace α}
{β : Type u_5}
[PseudoMetricSpace β]
{f g : α → β}
(hf : StronglyMeasurable f)
(hg : StronglyMeasurable g)
:
StronglyMeasurable fun (x : α) => dist (f x) (g x)
theorem
MeasureTheory.StronglyMeasurable.norm
{α : Type u_1}
{x✝ : MeasurableSpace α}
{β : Type u_5}
[SeminormedAddCommGroup β]
{f : α → β}
(hf : StronglyMeasurable f)
:
StronglyMeasurable fun (x : α) => ‖f x‖
theorem
MeasureTheory.StronglyMeasurable.nnnorm
{α : Type u_1}
{x✝ : MeasurableSpace α}
{β : Type u_5}
[SeminormedAddCommGroup β]
{f : α → β}
(hf : StronglyMeasurable f)
:
StronglyMeasurable fun (x : α) => ‖f x‖₊
theorem
MeasureTheory.StronglyMeasurable.enorm
{α : Type u_1}
{x✝ : MeasurableSpace α}
{β : Type u_5}
[SeminormedAddCommGroup β]
{f : α → β}
(hf : StronglyMeasurable f)
:
Measurable fun (x : α) => ‖f x‖ₑ
The enorm of a strongly measurable function is measurable.
Unlike StrongMeasurable.norm and StronglyMeasurable.nnnorm, this lemma proves measurability,
not strong measurability. This is an intentional decision: for functions taking values in
ℝ≥0∞, measurability is much more useful than strong measurability.
@[deprecated MeasureTheory.StronglyMeasurable.enorm (since := "2025-01-21")]
theorem
MeasureTheory.StronglyMeasurable.ennnorm
{α : Type u_1}
{x✝ : MeasurableSpace α}
{β : Type u_5}
[SeminormedAddCommGroup β]
{f : α → β}
(hf : StronglyMeasurable f)
:
Measurable fun (x : α) => ‖f x‖ₑ
Alias of MeasureTheory.StronglyMeasurable.enorm.
The enorm of a strongly measurable function is measurable.
Unlike StrongMeasurable.norm and StronglyMeasurable.nnnorm, this lemma proves measurability,
not strong measurability. This is an intentional decision: for functions taking values in
ℝ≥0∞, measurability is much more useful than strong measurability.
theorem
MeasureTheory.StronglyMeasurable.real_toNNReal
{α : Type u_1}
{x✝ : MeasurableSpace α}
{f : α → ℝ}
(hf : StronglyMeasurable f)
:
StronglyMeasurable fun (x : α) => (f x).toNNReal
theorem
MeasureTheory.StronglyMeasurable.measurableSet_le
{α : Type u_1}
{E : Type u_5}
{m : MeasurableSpace α}
{f g : α → E}
[TopologicalSpace E]
[Preorder E]
[OrderClosedTopology E]
[TopologicalSpace.PseudoMetrizableSpace E]
(hf : StronglyMeasurable f)
(hg : StronglyMeasurable g)
:
theorem
MeasureTheory.StronglyMeasurable.measurableSet_lt
{α : Type u_1}
{E : Type u_5}
{m : MeasurableSpace α}
{f g : α → E}
[TopologicalSpace E]
[Preorder E]
[OrderClosedTopology E]
[TopologicalSpace.PseudoMetrizableSpace E]
(hf : StronglyMeasurable f)
(hg : StronglyMeasurable g)
:
theorem
MeasureTheory.StronglyMeasurable.ae_le_trim_of_stronglyMeasurable
{α : Type u_1}
{E : Type u_5}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{f g : α → E}
[TopologicalSpace E]
[Preorder E]
[OrderClosedTopology E]
[TopologicalSpace.PseudoMetrizableSpace E]
(hm : m ≤ m₀)
(hf : StronglyMeasurable f)
(hg : StronglyMeasurable g)
(hfg : f ≤ᶠ[ae μ] g)
:
theorem
MeasureTheory.StronglyMeasurable.ae_le_trim_iff
{α : Type u_1}
{E : Type u_5}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{f g : α → E}
[TopologicalSpace E]
[Preorder E]
[OrderClosedTopology E]
[TopologicalSpace.PseudoMetrizableSpace E]
(hm : m ≤ m₀)
(hf : StronglyMeasurable f)
(hg : StronglyMeasurable g)
:
theorem
MeasureTheory.StronglyMeasurable.measurableSet_eq_fun
{α : Type u_1}
{E : Type u_5}
{m : MeasurableSpace α}
{f g : α → E}
[TopologicalSpace E]
[TopologicalSpace.MetrizableSpace E]
(hf : StronglyMeasurable f)
(hg : StronglyMeasurable g)
:
theorem
MeasureTheory.StronglyMeasurable.ae_eq_trim_of_stronglyMeasurable
{α : Type u_1}
{E : Type u_5}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{f g : α → E}
[TopologicalSpace E]
[TopologicalSpace.MetrizableSpace E]
(hm : m ≤ m₀)
(hf : StronglyMeasurable f)
(hg : StronglyMeasurable g)
(hfg : f =ᶠ[ae μ] g)
:
theorem
MeasureTheory.StronglyMeasurable.ae_eq_trim_iff
{α : Type u_1}
{E : Type u_5}
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{f g : α → E}
[TopologicalSpace E]
[TopologicalSpace.MetrizableSpace E]
(hm : m ≤ m₀)
(hf : StronglyMeasurable f)
(hg : StronglyMeasurable g)
:
theorem
MeasureTheory.StronglyMeasurable.stronglyMeasurable_in_set
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
[TopologicalSpace β]
[Zero β]
{s : Set α}
{f : α → β}
(hs : MeasurableSet s)
(hf : StronglyMeasurable f)
(hf_zero : ∀ x ∉ s, f x = 0)
:
∃ (fs : ℕ → 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 m₂ : MeasurableSpace α}
[TopologicalSpace E]
[Zero E]
{s : Set α}
{f : α → E}
(hs_m : MeasurableSet s)
(hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t))
(hf : StronglyMeasurable f)
(hf_zero : ∀ x ∉ s, f x = 0)
:
If the restriction to a set s of a σ-algebra m is included in the restriction to s of
another σ-algebra m₂ (hypothesis hs), the set s is m measurable and a function f supported
on s is m-strongly-measurable, then f is also m₂-strongly-measurable.
theorem
MeasureTheory.StronglyMeasurable.exists_spanning_measurableSet_norm_le
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[SeminormedAddCommGroup β]
{m m0 : MeasurableSpace α}
(hm : m ≤ m0)
(hf : StronglyMeasurable f)
(μ : Measure α)
[SigmaFinite (μ.trim hm)]
:
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 α}
{μ : Measure α}
[Zero β]
[TopologicalSpace β]
:
noncomputable def
MeasureTheory.FinStronglyMeasurable.approx
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{f : α → β}
[Zero β]
[TopologicalSpace β]
(hf : FinStronglyMeasurable f μ)
:
ℕ → 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
- hf.approx = Exists.choose hf
Instances For
theorem
MeasureTheory.FinStronglyMeasurable.fin_support_approx
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{f : α → β}
[Zero β]
[TopologicalSpace β]
(hf : FinStronglyMeasurable f μ)
(n : ℕ)
:
theorem
MeasureTheory.FinStronglyMeasurable.tendsto_approx
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{f : α → β}
[Zero β]
[TopologicalSpace β]
(hf : FinStronglyMeasurable f μ)
(x : α)
:
Filter.Tendsto (fun (n : ℕ) => (hf.approx n) x) Filter.atTop (nhds (f x))
theorem
MeasureTheory.FinStronglyMeasurable.stronglyMeasurable
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{f : α → β}
[Zero β]
[TopologicalSpace β]
(hf : FinStronglyMeasurable f μ)
:
A finitely strongly measurable function is strongly measurable.
theorem
MeasureTheory.FinStronglyMeasurable.exists_set_sigmaFinite
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{f : α → β}
[Zero β]
[TopologicalSpace β]
[T2Space β]
(hf : FinStronglyMeasurable f μ)
:
∃ (t : Set α), MeasurableSet t ∧ (∀ x ∈ tᶜ, f x = 0) ∧ SigmaFinite (μ.restrict t)
theorem
MeasureTheory.FinStronglyMeasurable.measurable
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{f : α → β}
[Zero β]
[TopologicalSpace β]
[TopologicalSpace.PseudoMetrizableSpace β]
[MeasurableSpace β]
[BorelSpace β]
(hf : FinStronglyMeasurable f μ)
:
A finitely strongly measurable function is measurable.
theorem
MeasureTheory.FinStronglyMeasurable.mul
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{f g : α → β}
[TopologicalSpace β]
[MonoidWithZero β]
[ContinuousMul β]
(hf : FinStronglyMeasurable f μ)
(hg : FinStronglyMeasurable g μ)
:
FinStronglyMeasurable (f * g) μ
theorem
MeasureTheory.FinStronglyMeasurable.add
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{f g : α → β}
[TopologicalSpace β]
[AddMonoid β]
[ContinuousAdd β]
(hf : FinStronglyMeasurable f μ)
(hg : FinStronglyMeasurable g μ)
:
FinStronglyMeasurable (f + g) μ
theorem
MeasureTheory.FinStronglyMeasurable.neg
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{f : α → β}
[TopologicalSpace β]
[AddGroup β]
[IsTopologicalAddGroup β]
(hf : FinStronglyMeasurable f μ)
:
FinStronglyMeasurable (-f) μ
theorem
MeasureTheory.FinStronglyMeasurable.sub
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{f g : α → β}
[TopologicalSpace β]
[AddGroup β]
[ContinuousSub β]
(hf : FinStronglyMeasurable f μ)
(hg : FinStronglyMeasurable g μ)
:
FinStronglyMeasurable (f - g) μ
theorem
MeasureTheory.FinStronglyMeasurable.const_smul
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{f : α → β}
[TopologicalSpace β]
{𝕜 : Type u_5}
[TopologicalSpace 𝕜]
[AddMonoid β]
[Monoid 𝕜]
[DistribMulAction 𝕜 β]
[ContinuousSMul 𝕜 β]
(hf : FinStronglyMeasurable f μ)
(c : 𝕜)
:
FinStronglyMeasurable (c • f) μ
theorem
MeasureTheory.FinStronglyMeasurable.sup
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{f g : α → β}
[TopologicalSpace β]
[Zero β]
[SemilatticeSup β]
[ContinuousSup β]
(hf : FinStronglyMeasurable f μ)
(hg : FinStronglyMeasurable g μ)
:
FinStronglyMeasurable (f ⊔ g) μ
theorem
MeasureTheory.FinStronglyMeasurable.inf
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{f g : α → β}
[TopologicalSpace β]
[Zero β]
[SemilatticeInf β]
[ContinuousInf β]
(hf : FinStronglyMeasurable f μ)
(hg : FinStronglyMeasurable g μ)
:
FinStronglyMeasurable (f ⊓ g) μ
theorem
MeasureTheory.finStronglyMeasurable_iff_stronglyMeasurable_and_exists_set_sigmaFinite
{α : Type u_5}
{β : Type u_6}
{f : α → β}
[TopologicalSpace β]
[T2Space β]
[Zero β]
{x✝ : MeasurableSpace α}
{μ : Measure α}
:
FinStronglyMeasurable f μ ↔ StronglyMeasurable f ∧ ∃ (t : Set α), MeasurableSet t ∧ (∀ x ∈ tᶜ, f x = 0) ∧ SigmaFinite (μ.restrict t)
theorem
MeasureTheory.finStronglyMeasurable_iff_measurable
{α : 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, 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 α}
(μ : Measure α)
[SigmaFinite μ]
(hf : Measurable f)
:
In a space with second countable topology and a sigma-finite measure, a measurable function
is FinStronglyMeasurable.
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))
:
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 : ι), StronglyMeasurable (u i))
: