ProbabilityTheory.Memℒp.uniformIntegrable_of_identDistrib
theorem ProbabilityTheory.Memℒp.uniformIntegrable_of_identDistrib :
∀ {α : Type u_1} [inst : MeasurableSpace α] {E : Type u_5} [inst_1 : MeasurableSpace E]
[inst_2 : NormedAddCommGroup E] [inst_3 : BorelSpace E] {μ : MeasureTheory.Measure α}
[inst_4 : MeasureTheory.IsFiniteMeasure μ] {ι : Type u_6} {f : ι → α → E} {j : ι} {p : ENNReal},
1 ≤ p →
p ≠ ⊤ →
MeasureTheory.Memℒp (f j) p μ →
(∀ (i : ι), ProbabilityTheory.IdentDistrib (f i) (f j) μ μ) → MeasureTheory.UniformIntegrable f p μ
This theorem, named `ProbabilityTheory.Memℒp.uniformIntegrable_of_identDistrib`, states that for a measurable space `α` and a normed group `E`, given a measure `μ` on `α` that is finite, a sequence of functions `f : ι → α → E`, an index `j : ι`, and a non-infinite extended nonnegative real number `p` that is greater than or equal to 1, if the function `f j` has the property `MeasureTheory.Memℒp` (that is, it is almost everywhere strongly measurable and the integral of its norm to the power `p` is finite) and all functions `f i` in the sequence are identically distributed to `f j`, then the sequence of functions `f` is `p`-uniformly integrable in the measure theory sense and is uniformly bounded, as indicated by the property `MeasureTheory.UniformIntegrable`.
More concisely: If `μ` is a finite measure on a measurable space `α`, `E` is a normed group, `p ≥ 1` is a non-infinite extended nonnegative real number, `f : ι → α → E` is a sequence of almost everywhere strongly measurable functions with `μ`-finite `∫αℝ|f j(x)|^p dμ(x)` for some `j : ι`, and all functions in the sequence are identically distributed, then `f` is `p`-uniformly integrable and uniformly bounded in the measure theory sense.
|
ProbabilityTheory.IdentDistrib.measure_preimage_eq
theorem ProbabilityTheory.IdentDistrib.measure_preimage_eq :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
[inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → γ} {g : β → γ},
ProbabilityTheory.IdentDistrib f g μ ν → ∀ {s : Set γ}, MeasurableSet s → ↑↑μ (f ⁻¹' s) = ↑↑ν (g ⁻¹' s)
This theorem, referred to as an alias of `ProbabilityTheory.IdentDistrib.measure_mem_eq`, states that for any three types `α`, `β`, and `γ`, given measurable spaces over these types and measures `μ` and `ν` over `α` and `β` respectively, and functions `f` and `g` from `α` to `γ` and `β` to `γ` respectively, if the functions `f` and `g` distribute `μ` and `ν` identically (as per `ProbabilityTheory.IdentDistrib`), then for any measurable set `s` in `γ`, the measure of the preimage of `s` under `f` with respect to `μ` is equal to the measure of the preimage of `s` under `g` with respect to `ν`. In mathematical terms, this theorem states that for any measurable set $s$ in the codomain, $μ(f^{-1}(s)) = ν(g^{-1}(s))$ when $f$ and $g$ distribute $μ$ and $ν$ identically.
More concisely: If measurable functions `f` and `g` distribute measures `μ` and `ν` identically, then for any measurable set `s` in the codomain, `μ(f⁻¹(s)) = ν(g⁻¹(s))`.
|
ProbabilityTheory.IdentDistrib.symm
theorem ProbabilityTheory.IdentDistrib.symm :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
[inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → γ} {g : β → γ},
ProbabilityTheory.IdentDistrib f g μ ν → ProbabilityTheory.IdentDistrib g f ν μ
This theorem, `ProbabilityTheory.IdentDistrib.symm`, states that for any three Types `α`, `β`, and `γ`, and given measurable spaces over `α`, `β`, and `γ`, as well as measures `μ` over `α` and `ν` over `β`, and functions `f : α → γ` and `g : β → γ`, if the identity distribution law holds for `f`, `g`, `μ`, and `ν`, then it also holds for `g`, `f`, `ν`, and `μ`. In other words, the identity distribution law is symmetric with respect to the input functions and measures.
More concisely: If functions `f : α → γ` and `g : β → γ` preserve measures `μ` over `α` and `ν` over `β`, respectively, and the identity distribution law holds for `(f, g, μ, ν)`, then it also holds for `(g, f, ν, μ)`.
|
ProbabilityTheory.Memℒp.uniformIntegrable_of_identDistrib_aux
theorem ProbabilityTheory.Memℒp.uniformIntegrable_of_identDistrib_aux :
∀ {α : Type u_1} [inst : MeasurableSpace α] {E : Type u_5} [inst_1 : MeasurableSpace E]
[inst_2 : NormedAddCommGroup E] [inst_3 : BorelSpace E] {μ : MeasureTheory.Measure α}
[inst_4 : MeasureTheory.IsFiniteMeasure μ] {ι : Type u_6} {f : ι → α → E} {j : ι} {p : ENNReal},
1 ≤ p →
p ≠ ⊤ →
MeasureTheory.Memℒp (f j) p μ →
(∀ (i : ι), MeasureTheory.StronglyMeasurable (f i)) →
(∀ (i : ι), ProbabilityTheory.IdentDistrib (f i) (f j) μ μ) → MeasureTheory.UniformIntegrable f p μ
This theorem, titled `ProbabilityTheory.Memℒp.uniformIntegrable_of_identDistrib_aux`, states that for a set of conditions, we can show that a family of measurable functions is uniformly integrable. The conditions are as follows: We have two types, `α` and `E`, with `α` having a measurable space structure and `E` having a measurable space structure, a normed add commutative group structure, and a Borel space structure. We also have a measure `μ` on `α` which is a finite measure, and a family of functions `f` from an index set `ι` to `α → E`. If we take any `j` from `ι`, and an extended nonnegative real number `p` such that `p` is greater than or equal to one and less than infinity, and it is the case that `f j` belongs to the set `MeasureTheory.Memℒp` for measure `μ` and real number `p`, and every function `f i` for `i` in `ι` is strongly measurable and is identically distributed as `f j` (according to the `ProbabilityTheory.IdentDistrib` predicate), then the function family `f` is uniformly integrable with respect to measure `μ` and real number `p`.
More concisely: If `μ` is a finite measure on a measurable space `α` with a normed add commutative group and Borel space structure, and `f` is a family of identically distributed, strongly measurable functions from an index set `ι` to `α → E` with each `f j` in `MeasureTheory.Memℒp` for some `p ≥ 1`, then `f` is uniformly integrable with respect to `μ` and `p`.
|
ProbabilityTheory.IdentDistrib.comp
theorem ProbabilityTheory.IdentDistrib.comp :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : MeasurableSpace α]
[inst_1 : MeasurableSpace β] [inst_2 : MeasurableSpace γ] [inst_3 : MeasurableSpace δ]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → γ} {g : β → γ} {u : γ → δ},
ProbabilityTheory.IdentDistrib f g μ ν → Measurable u → ProbabilityTheory.IdentDistrib (u ∘ f) (u ∘ g) μ ν
The theorem `ProbabilityTheory.IdentDistrib.comp` states that for all types `α`, `β`, `γ`, `δ`, given measurable spaces over these types, measures `μ` and `ν` over `α` and `β` respectively, and functions `f : α → γ`, `g : β → γ` and `u : γ → δ`, if `f` and `g` are distributions that are identically distributed under measures `μ` and `ν` respectively, and `u` is a measurable function, then the composed functions `u ∘ f` and `u ∘ g` are also identically distributed under measures `μ` and `ν`. This theorem essentially expresses the property that the identical distribution of two random variables is preserved under the action of a measurable function.
More concisely: If measurable functions $f : \alpha \rightarrow \gamma$ and $g : \beta \rightarrow \gamma$ are identically distributed under measures $\mu$ and $\nu$ over types $\alpha$ and $\beta$ respectively, and $u : \gamma \rightarrow \delta$ is a measurable function, then $u \circ f$ and $u \circ g$ are identically distributed under measures $\mu$ and $\nu$.
|
ProbabilityTheory.IdentDistrib.aestronglyMeasurable_fst
theorem ProbabilityTheory.IdentDistrib.aestronglyMeasurable_fst :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
[inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → γ} {g : β → γ}
[inst_3 : TopologicalSpace γ] [inst_4 : TopologicalSpace.MetrizableSpace γ] [inst_5 : OpensMeasurableSpace γ]
[inst_6 : SecondCountableTopology γ],
ProbabilityTheory.IdentDistrib f g μ ν → MeasureTheory.AEStronglyMeasurable f μ
This theorem states that if we have a pair of identically distributed functions, `f` and `g`, with `f` mapping from type `α` to `γ`, and `g` mapping from type `β` to `γ`, under measures `μ` and `ν` respectively, then in a second countable metrizable topological space on `γ`, the function `f` is almost everywhere strongly measurable with respect to measure `μ`. It means that `f` is almost everywhere equal to the limit of a sequence of simple functions. Note that while `g` is also almost everywhere strongly measurable, it should be examined using `h.symm.aestronglyMeasurable_fst` because `h.aestronglyMeasurable_snd` has a different meaning.
More concisely: If `f` and `g` are identically distributed functions from measurable spaces `(α, μ)` and `(β, ν)` to a second countable metrizable topological space `(γ, τ)`, then `f` is almost everywhere strongly measurable with respect to `μ`.
|
ProbabilityTheory.IdentDistrib.of_ae_eq
theorem ProbabilityTheory.IdentDistrib.of_ae_eq :
∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace γ]
{μ : MeasureTheory.Measure α} {f g : α → γ},
AEMeasurable f μ → μ.ae.EventuallyEq f g → ProbabilityTheory.IdentDistrib f g μ μ
The theorem `ProbabilityTheory.IdentDistrib.of_ae_eq` states that for any measurable spaces `α` and `γ`, and a measure `μ` on `α`, if a function `f` from `α` to `γ` is almost everywhere measurable with respect to `μ`, and `f` is almost everywhere equal to another function `g` (also from `α` to `γ`) with respect to the same measure `μ`, then the identity distribution property holds for `f` and `g` with respect to measure `μ`. The identity distribution property in probability theory typically means that the distribution of `f` and `g` under the measure `μ` are the same.
More concisely: If measurable functions `f` and `g` on measurable spaces `α` with respect to measure `μ` are almost everywhere equal, then they have the same distribution under `μ`.
|
ProbabilityTheory.IdentDistrib.aestronglyMeasurable_snd
theorem ProbabilityTheory.IdentDistrib.aestronglyMeasurable_snd :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
[inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → γ} {g : β → γ}
[inst_3 : TopologicalSpace γ] [inst_4 : TopologicalSpace.MetrizableSpace γ] [inst_5 : BorelSpace γ],
ProbabilityTheory.IdentDistrib f g μ ν →
MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.AEStronglyMeasurable g ν
The theorem `ProbabilityTheory.IdentDistrib.aestronglyMeasurable_snd` asserts that if two functions `f` and `g`, mapping from different spaces (`α` and `β` respectively) to a common space `γ`, are identically distributed with respect to two measures (`μ` on `α` and `ν` on `β`), and if `f` is almost everywhere strongly measurable with respect to `μ` (meaning it is almost everywhere equal to the limit of a sequence of simple functions), then `g` is also almost everywhere strongly measurable with respect to `ν`. This theorem holds in the context where `γ` is a topological space, `γ` has a metrizable topology, and `γ` is a Borel space.
More concisely: If two functions between different spaces with a common Borel space value, having identical distributions under two measures and with one function almost everywhere equal to the limit of simple functions, then the other function is almost everywhere strongly measurable under the respective measure.
|