Characterizing independence via bounded continuous functions #
Given two random variables X : Ω → E and Y : Ω → F such that E and F are Borel spaces
satisfying HasOuterApproxClosed, X and Y are independent if for any real bounded continuous
functions f and g, ∫ ω, f (X ω) * g (Y ω) ∂P = (∫ ω, f (X ω) ∂P) * (∫ ω, g (Y ω) ∂P).
Consider now X : (s : S) → Ω → E s, with Fintype S and each E s being a Borel space satisfying
HasOuterApproxClosed. Then to apply the above result we need that Π s, E s is a Borel space,
and therefore that each E s is second countable. We can circumvent this restriction by proving
that fun ω s ↦ X s ω and Y are independent if for any family of bounded continuous functions
f : (s : S) → E s → ℝ and any bounded continuous function g : F → ℝ we have
∫ ω, ∏ s, f s (X s ω) * g (Y ω) ∂P = ∫ ω, ∏ s, f s (X s ω) ∂P * ∫ ω, g (Y ω) ∂P.
We can use this result in the case where S := Unit to deduce the first statement we mentioned.
We take this approach in this file. We first prove pi_indepFun_pi_of_prod_bcf, which allows to
prove the result when E and F are product spaces without assuming second countability, and
then we deduce the other cases from there.
Building on this, we also prove process_indepFun_process_of_prod_bcf. This time we do not require
Fintype S and require the hypothesis to be satisfied for each I : Finset S. Then we similarly
deduce other versions where one of the variables is not necessarily a process.
We then turn to independence between an event and a random variable. We prove
indicator_indepFun_pi_of_prod_bcf: the indicator of an event A is independent
of a finite family of random variables X : (s : S) → Ω → E s if for any family of bounded
continuous functions f : (s : S) → E s → ℝ we have
∫ ω in A, ∏ s, f s (X s ω) ∂P = P.real A * ∫ ω, ∏ s, f s (X s ω) ∂P. Once again we deduce
other versions from this, and also write versions where X is a stochastic process.
Then we build on that to show that a σ-algebra m is independent from a stochastic process X
if for any A such that MeasurableSet[m] A, any I : Finset S and any bounded continuous
function f : (Π s : I, E s) → ℝ, we have ∫ ω in A, f (X · ω) ∂P = P.real A * ∫ ω, f (X · ω) ∂P.
This again is formulated with different versions. We also provide versions in terms of
IndepSets instead of Indep.
Main statement #
indep_comap_process_of_bcf: Aσ-algebramis independent from a stochastic processXif for anyAsuch thatMeasurableSet[m] A, anyI : Finset S, and any bounded continuous functionf : (Π s : I, E s) → ℝ, we have∫ ω in A, f (X · ω) ∂P = P.real A * ∫ ω, f (X · ω) ∂P.
Notations #
to avoid writing boundedContinuousFunction in the names, which is quite lengthy, we abbreviate it
to bcf.
Tags #
independence, bounded continuous functions
theorem
IndepFun.singleton_indepSets_of_indicator
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{𝓧 : Type u_4}
[mX : MeasurableSpace 𝓧]
{A : Set Ω}
{X : Ω → 𝓧}
(h : ProbabilityTheory.IndepFun (A.indicator 1) X P)
:
ProbabilityTheory.IndepSets {A} {s : Set Ω | MeasurableSet s} P
If the indicator of a set A is indepent from a variable X, then set A is independent
from the sigma algebra generated by X.
theorem
pi_indepFun_pi_of_prod_bcf
{Ω : Type u_1}
{S : Type u_2}
{T : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : S → Type u_4}
{F : T → Type u_5}
[(s : S) → TopologicalSpace (E s)]
[(s : S) → MeasurableSpace (E s)]
[∀ (s : S), BorelSpace (E s)]
[∀ (s : S), HasOuterApproxClosed (E s)]
[(t : T) → TopologicalSpace (F t)]
[(t : T) → MeasurableSpace (F t)]
[∀ (t : T), BorelSpace (F t)]
[∀ (t : T), HasOuterApproxClosed (F t)]
{X : (s : S) → Ω → E s}
{Y : (t : T) → Ω → F t}
[Fintype S]
[Fintype T]
[MeasureTheory.IsFiniteMeasure P]
(mX : ∀ (s : S), AEMeasurable (X s) P)
(mY : ∀ (t : T), AEMeasurable (Y t) P)
(h :
∀ (f : (s : S) → BoundedContinuousFunction (E s) ℝ) (g : (t : T) → BoundedContinuousFunction (F t) ℝ),
∫ (x : Ω), ((∏ s : S, ⇑(f s) ∘ X s) * ∏ t : T, ⇑(g t) ∘ Y t) x ∂P = (∫ (x : Ω), (∏ s : S, ⇑(f s) ∘ X s) x ∂P) * ∫ (x : Ω), (∏ t : T, ⇑(g t) ∘ Y t) x ∂P)
:
ProbabilityTheory.IndepFun (fun (ω : Ω) (s : S) => X s ω) (fun (ω : Ω) (t : T) => Y t ω) P
theorem
pi_indepFun_pi_of_bcf
{Ω : Type u_1}
{S : Type u_2}
{T : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : S → Type u_4}
{F : T → Type u_5}
[(s : S) → TopologicalSpace (E s)]
[(s : S) → MeasurableSpace (E s)]
[∀ (s : S), BorelSpace (E s)]
[∀ (s : S), HasOuterApproxClosed (E s)]
[(t : T) → TopologicalSpace (F t)]
[(t : T) → MeasurableSpace (F t)]
[∀ (t : T), BorelSpace (F t)]
[∀ (t : T), HasOuterApproxClosed (F t)]
{X : (s : S) → Ω → E s}
{Y : (t : T) → Ω → F t}
[Fintype S]
[Fintype T]
[MeasureTheory.IsFiniteMeasure P]
(mX : ∀ (s : S), AEMeasurable (X s) P)
(mY : ∀ (t : T), AEMeasurable (Y t) P)
(h :
∀ (f : BoundedContinuousFunction ((s : S) → E s) ℝ) (g : BoundedContinuousFunction ((t : T) → F t) ℝ),
∫ (x : Ω), (fun (ω : Ω) => (f fun (x : S) => X x ω) * g fun (x : T) => Y x ω) x ∂P = (∫ (x : Ω), (fun (ω : Ω) => f fun (x : S) => X x ω) x ∂P) * ∫ (x : Ω), (fun (ω : Ω) => g fun (x : T) => Y x ω) x ∂P)
:
ProbabilityTheory.IndepFun (fun (ω : Ω) (s : S) => X s ω) (fun (ω : Ω) (t : T) => Y t ω) P
Two families of random variables $(X_1, ..., X_p)$ and $(Y_1, ..., Y_q)$ are independent if for all real bounded continuous functions $f$ and $g$, $$P[f(X_1, ..., X_p) g(Y_1, ..., Y_q)] = P[f(X_1, ..., X_p)] * P[g(Y_1, ..., Y_q)].$$
theorem
indepFun_pi_of_prod_bcf
{Ω : Type u_1}
{T : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{F : T → Type u_5}
{G : Type u_6}
[(t : T) → TopologicalSpace (F t)]
[(t : T) → MeasurableSpace (F t)]
[∀ (t : T), BorelSpace (F t)]
[∀ (t : T), HasOuterApproxClosed (F t)]
[TopologicalSpace G]
[MeasurableSpace G]
[BorelSpace G]
[HasOuterApproxClosed G]
{Y : (t : T) → Ω → F t}
{Z : Ω → G}
[Fintype T]
[MeasureTheory.IsFiniteMeasure P]
(mZ : AEMeasurable Z P)
(mY : ∀ (t : T), AEMeasurable (Y t) P)
(h :
∀ (f : BoundedContinuousFunction G ℝ) (g : (t : T) → BoundedContinuousFunction (F t) ℝ),
∫ (x : Ω), (⇑f ∘ Z * ∏ t : T, ⇑(g t) ∘ Y t) x ∂P = (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (∏ t : T, ⇑(g t) ∘ Y t) x ∂P)
:
ProbabilityTheory.IndepFun Z (fun (ω : Ω) (t : T) => Y t ω) P
theorem
indepFun_pi_of_bcf
{Ω : Type u_1}
{T : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{F : T → Type u_5}
{G : Type u_6}
[(t : T) → TopologicalSpace (F t)]
[(t : T) → MeasurableSpace (F t)]
[∀ (t : T), BorelSpace (F t)]
[∀ (t : T), HasOuterApproxClosed (F t)]
[TopologicalSpace G]
[MeasurableSpace G]
[BorelSpace G]
[HasOuterApproxClosed G]
{Y : (t : T) → Ω → F t}
{Z : Ω → G}
[Fintype T]
[MeasureTheory.IsFiniteMeasure P]
(mZ : AEMeasurable Z P)
(mY : ∀ (t : T), AEMeasurable (Y t) P)
(h :
∀ (f : BoundedContinuousFunction G ℝ) (g : BoundedContinuousFunction ((t : T) → F t) ℝ),
∫ (x : Ω), (fun (ω : Ω) => f (Z ω) * g fun (x : T) => Y x ω) x ∂P = (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (fun (ω : Ω) => g fun (x : T) => Y x ω) x ∂P)
:
ProbabilityTheory.IndepFun Z (fun (ω : Ω) (t : T) => Y t ω) P
theorem
pi_indepFun_of_prod_bcf
{Ω : Type u_1}
{S : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : S → Type u_4}
{H : Type u_7}
[(s : S) → TopologicalSpace (E s)]
[(s : S) → MeasurableSpace (E s)]
[∀ (s : S), BorelSpace (E s)]
[∀ (s : S), HasOuterApproxClosed (E s)]
[TopologicalSpace H]
[MeasurableSpace H]
[BorelSpace H]
[HasOuterApproxClosed H]
{X : (s : S) → Ω → E s}
{U : Ω → H}
[Fintype S]
[MeasureTheory.IsFiniteMeasure P]
(mX : ∀ (s : S), AEMeasurable (X s) P)
(mU : AEMeasurable U P)
(h :
∀ (f : (s : S) → BoundedContinuousFunction (E s) ℝ) (g : BoundedContinuousFunction H ℝ),
∫ (x : Ω), ((∏ s : S, ⇑(f s) ∘ X s) * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (∏ s : S, ⇑(f s) ∘ X s) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P)
:
ProbabilityTheory.IndepFun (fun (ω : Ω) (s : S) => X s ω) U P
theorem
pi_indepFun_of_bcf
{Ω : Type u_1}
{S : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : S → Type u_4}
{H : Type u_7}
[(s : S) → TopologicalSpace (E s)]
[(s : S) → MeasurableSpace (E s)]
[∀ (s : S), BorelSpace (E s)]
[∀ (s : S), HasOuterApproxClosed (E s)]
[TopologicalSpace H]
[MeasurableSpace H]
[BorelSpace H]
[HasOuterApproxClosed H]
{X : (s : S) → Ω → E s}
{U : Ω → H}
[Fintype S]
[MeasureTheory.IsFiniteMeasure P]
(mX : ∀ (s : S), AEMeasurable (X s) P)
(mU : AEMeasurable U P)
(h :
∀ (f : BoundedContinuousFunction ((s : S) → E s) ℝ) (g : BoundedContinuousFunction H ℝ),
∫ (x : Ω), (fun (ω : Ω) => (f fun (x : S) => X x ω) * g (U ω)) x ∂P = (∫ (x : Ω), (fun (ω : Ω) => f fun (x : S) => X x ω) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P)
:
ProbabilityTheory.IndepFun (fun (ω : Ω) (s : S) => X s ω) U P
theorem
indepFun_of_bcf
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{G : Type u_6}
{H : Type u_7}
[TopologicalSpace G]
[MeasurableSpace G]
[BorelSpace G]
[HasOuterApproxClosed G]
[TopologicalSpace H]
[MeasurableSpace H]
[BorelSpace H]
[HasOuterApproxClosed H]
{Z : Ω → G}
{U : Ω → H}
[MeasureTheory.IsFiniteMeasure P]
(mZ : AEMeasurable Z P)
(mU : AEMeasurable U P)
(h :
∀ (f : BoundedContinuousFunction G ℝ) (g : BoundedContinuousFunction H ℝ),
∫ (x : Ω), (⇑f ∘ Z * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P)
:
Two random variables $X$ and $Y$ are independent if for all real bounded continuous functions $f$ and $g$, $$P[f(X) g(Y)] = P[f(X)] * P[g(Y)].$$
theorem
indicator_indepFun_pi_of_prod_bcf
{Ω : Type u_1}
{S : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : S → Type u_4}
[(s : S) → TopologicalSpace (E s)]
[(s : S) → MeasurableSpace (E s)]
[∀ (s : S), BorelSpace (E s)]
[∀ (s : S), HasOuterApproxClosed (E s)]
{X : (s : S) → Ω → E s}
[Fintype S]
[MeasureTheory.IsProbabilityMeasure P]
{A : Set Ω}
(mA : MeasureTheory.NullMeasurableSet A P)
(mX : ∀ (s : S), AEMeasurable (X s) P)
(h :
∀ (f : (s : S) → BoundedContinuousFunction (E s) ℝ),
∫ (ω : Ω) in A, ∏ s : S, (f s) (X s ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s : S, (f s) (X s ω) ∂P)
:
ProbabilityTheory.IndepFun (A.indicator 1) (fun (ω : Ω) (s : S) => X s ω) P
theorem
indicator_indepFun_pi_of_bcf
{Ω : Type u_1}
{S : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : S → Type u_4}
[(s : S) → TopologicalSpace (E s)]
[(s : S) → MeasurableSpace (E s)]
[∀ (s : S), BorelSpace (E s)]
[∀ (s : S), HasOuterApproxClosed (E s)]
{X : (s : S) → Ω → E s}
[Fintype S]
[MeasureTheory.IsProbabilityMeasure P]
{A : Set Ω}
(mA : MeasureTheory.NullMeasurableSet A P)
(mX : ∀ (s : S), AEMeasurable (X s) P)
(h :
∀ (f : BoundedContinuousFunction ((s : S) → E s) ℝ),
∫ (ω : Ω) in A, f fun (x : S) => X x ω ∂P = P.real A * ∫ (ω : Ω), f fun (x : S) => X x ω ∂P)
:
ProbabilityTheory.IndepFun (A.indicator 1) (fun (ω : Ω) (s : S) => X s ω) P
The indicator of a set $A$ and a family of random variables $(X_1, ..., X_p)$ are independent if for all real bounded continuous function $f$, $$P[\mathbb{I}_A f(X_1, ..., X_p)] = P(A) P[f(X_1, ..., X_p)].$$
theorem
indicator_indepFun_of_bcf
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{G : Type u_6}
[TopologicalSpace G]
[MeasurableSpace G]
[BorelSpace G]
[HasOuterApproxClosed G]
{Z : Ω → G}
[MeasureTheory.IsProbabilityMeasure P]
{A : Set Ω}
(mA : MeasureTheory.NullMeasurableSet A P)
(mZ : AEMeasurable Z P)
(h : ∀ (f : BoundedContinuousFunction G ℝ), ∫ (ω : Ω) in A, f (Z ω) ∂P = P.real A * ∫ (ω : Ω), f (Z ω) ∂P)
:
ProbabilityTheory.IndepFun (A.indicator 1) Z P
The indicator of a set $A$ and a random variable $X$ are independent if for all real bounded continuous function $f$, $$P[\mathbb{I}_A f(X)] = P(A) P[f(X)].$$
theorem
indepSets_comap_pi_of_prod_bcf
{Ω : Type u_1}
{S : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : S → Type u_4}
[(s : S) → TopologicalSpace (E s)]
[(s : S) → MeasurableSpace (E s)]
[∀ (s : S), BorelSpace (E s)]
[∀ (s : S), HasOuterApproxClosed (E s)]
{X : (s : S) → Ω → E s}
[Fintype S]
[MeasureTheory.IsProbabilityMeasure P]
{𝒜 : Set (Set Ω)}
(m𝒜 : ∀ A ∈ 𝒜, MeasureTheory.NullMeasurableSet A P)
(mX : ∀ (s : S), AEMeasurable (X s) P)
(h :
∀ A ∈ 𝒜,
∀ (f : (s : S) → BoundedContinuousFunction (E s) ℝ),
∫ (ω : Ω) in A, ∏ s : S, (f s) (X s ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s : S, (f s) (X s ω) ∂P)
:
ProbabilityTheory.IndepSets 𝒜 {A : Set Ω | MeasurableSet A} P
theorem
indepSets_comap_pi_of_bcf
{Ω : Type u_1}
{S : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : S → Type u_4}
[(s : S) → TopologicalSpace (E s)]
[(s : S) → MeasurableSpace (E s)]
[∀ (s : S), BorelSpace (E s)]
[∀ (s : S), HasOuterApproxClosed (E s)]
{X : (s : S) → Ω → E s}
[Fintype S]
[MeasureTheory.IsProbabilityMeasure P]
{𝒜 : Set (Set Ω)}
(m𝒜 : ∀ A ∈ 𝒜, MeasureTheory.NullMeasurableSet A P)
(mX : ∀ (s : S), AEMeasurable (X s) P)
(h :
∀ A ∈ 𝒜,
∀ (f : BoundedContinuousFunction ((s : S) → E s) ℝ),
∫ (ω : Ω) in A, f fun (x : S) => X x ω ∂P = P.real A * ∫ (ω : Ω), f fun (x : S) => X x ω ∂P)
:
ProbabilityTheory.IndepSets 𝒜 {A : Set Ω | MeasurableSet A} P
theorem
indepSets_comap_of_bcf
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{G : Type u_6}
[TopologicalSpace G]
[MeasurableSpace G]
[BorelSpace G]
[HasOuterApproxClosed G]
{Z : Ω → G}
[MeasureTheory.IsProbabilityMeasure P]
{𝒜 : Set (Set Ω)}
(m𝒜 : ∀ A ∈ 𝒜, MeasureTheory.NullMeasurableSet A P)
(mZ : AEMeasurable Z P)
(h : ∀ A ∈ 𝒜, ∀ (f : BoundedContinuousFunction G ℝ), ∫ (ω : Ω) in A, f (Z ω) ∂P = P.real A * ∫ (ω : Ω), f (Z ω) ∂P)
:
ProbabilityTheory.IndepSets 𝒜 {A : Set Ω | MeasurableSet A} P
theorem
indep_comap_pi_of_prod_bcf
{Ω : Type u_1}
{S : Type u_2}
{m mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : S → Type u_4}
[(s : S) → TopologicalSpace (E s)]
[(s : S) → MeasurableSpace (E s)]
[∀ (s : S), BorelSpace (E s)]
[∀ (s : S), HasOuterApproxClosed (E s)]
{X : (s : S) → Ω → E s}
[Fintype S]
[MeasureTheory.IsProbabilityMeasure P]
(hm : m ≤ mΩ)
(mX : ∀ (s : S), AEMeasurable (X s) P)
(h :
∀ (A : Set Ω),
MeasurableSet A →
∀ (f : (s : S) → BoundedContinuousFunction (E s) ℝ),
∫ (ω : Ω) in A, ∏ s : S, (f s) (X s ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s : S, (f s) (X s ω) ∂P)
:
ProbabilityTheory.Indep m (MeasurableSpace.comap (fun (ω : Ω) (s : S) => X s ω) MeasurableSpace.pi) P
theorem
indep_comap_pi_of_bcf
{Ω : Type u_1}
{S : Type u_2}
{m mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : S → Type u_4}
[(s : S) → TopologicalSpace (E s)]
[(s : S) → MeasurableSpace (E s)]
[∀ (s : S), BorelSpace (E s)]
[∀ (s : S), HasOuterApproxClosed (E s)]
{X : (s : S) → Ω → E s}
[Fintype S]
[MeasureTheory.IsProbabilityMeasure P]
(hm : m ≤ mΩ)
(mX : ∀ (s : S), AEMeasurable (X s) P)
(h :
∀ (A : Set Ω),
MeasurableSet A →
∀ (f : BoundedContinuousFunction ((s : S) → E s) ℝ),
∫ (ω : Ω) in A, f fun (x : S) => X x ω ∂P = P.real A * ∫ (ω : Ω), f fun (x : S) => X x ω ∂P)
:
ProbabilityTheory.Indep m (MeasurableSpace.comap (fun (ω : Ω) (s : S) => X s ω) MeasurableSpace.pi) P
A sigma-algebra $\mathcal{A}$ and a family of random variables $(X_1, ..., X_p)$ are independent if for all set $A \in \mathcal{A}$ and for all real bounded continuous function $f$, $$P[\mathbb{I}_A f(X_1, ..., X_p)] = P(A) P[f(X_1, ..., X_p)].$$
theorem
indep_comap_of_bcf
{Ω : Type u_1}
{m mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{G : Type u_6}
[TopologicalSpace G]
[MeasurableSpace G]
[BorelSpace G]
[HasOuterApproxClosed G]
{Z : Ω → G}
[MeasureTheory.IsProbabilityMeasure P]
(hm : m ≤ mΩ)
(mZ : AEMeasurable Z P)
(h :
∀ (A : Set Ω),
MeasurableSet A →
∀ (f : BoundedContinuousFunction G ℝ), ∫ (ω : Ω) in A, f (Z ω) ∂P = P.real A * ∫ (ω : Ω), f (Z ω) ∂P)
:
A sigma-algebra $\mathcal{A}$ and a random variable $X$ are independent if for all set $A \in \mathcal{A}$ and for all real bounded continuous function $f$, $$P[\mathbb{I}_A f(X)] = P(A) P[f(X)].$$
theorem
process_indepFun_process_of_prod_bcf
{Ω : Type u_1}
{S : Type u_2}
{T : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : S → Type u_4}
{F : T → Type u_5}
[(s : S) → TopologicalSpace (E s)]
[(s : S) → MeasurableSpace (E s)]
[∀ (s : S), BorelSpace (E s)]
[∀ (s : S), HasOuterApproxClosed (E s)]
[(t : T) → TopologicalSpace (F t)]
[(t : T) → MeasurableSpace (F t)]
[∀ (t : T), BorelSpace (F t)]
[∀ (t : T), HasOuterApproxClosed (F t)]
{X : (s : S) → Ω → E s}
{Y : (t : T) → Ω → F t}
[MeasureTheory.IsZeroOrProbabilityMeasure P]
(mX : ∀ (s : S), Measurable (X s))
(mY : ∀ (t : T), Measurable (Y t))
(h :
∀ (I : Finset S) (J : Finset T) (f : (s : ↥I) → BoundedContinuousFunction (E ↑s) ℝ)
(g : (t : ↥J) → BoundedContinuousFunction (F ↑t) ℝ),
∫ (x : Ω), ((∏ s : ↥I, ⇑(f s) ∘ X ↑s) * ∏ t : ↥J, ⇑(g t) ∘ Y ↑t) x ∂P = (∫ (x : Ω), (∏ s : ↥I, ⇑(f s) ∘ X ↑s) x ∂P) * ∫ (x : Ω), (∏ t : ↥J, ⇑(g t) ∘ Y ↑t) x ∂P)
:
ProbabilityTheory.IndepFun (fun (ω : Ω) (s : S) => X s ω) (fun (ω : Ω) (t : T) => Y t ω) P
theorem
process_indepFun_process_of_bcf
{Ω : Type u_1}
{S : Type u_2}
{T : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : S → Type u_4}
{F : T → Type u_5}
[(s : S) → TopologicalSpace (E s)]
[(s : S) → MeasurableSpace (E s)]
[∀ (s : S), BorelSpace (E s)]
[∀ (s : S), HasOuterApproxClosed (E s)]
[(t : T) → TopologicalSpace (F t)]
[(t : T) → MeasurableSpace (F t)]
[∀ (t : T), BorelSpace (F t)]
[∀ (t : T), HasOuterApproxClosed (F t)]
{X : (s : S) → Ω → E s}
{Y : (t : T) → Ω → F t}
[MeasureTheory.IsZeroOrProbabilityMeasure P]
(mX : ∀ (s : S), Measurable (X s))
(mY : ∀ (t : T), Measurable (Y t))
(h :
∀ (I : Finset S) (J : Finset T) (f : BoundedContinuousFunction ((s : ↥I) → E ↑s) ℝ)
(g : BoundedContinuousFunction ((t : ↥J) → F ↑t) ℝ),
∫ (x : Ω), (fun (ω : Ω) => (f fun (x : ↥I) => X (↑x) ω) * g fun (x : ↥J) => Y (↑x) ω) x ∂P = (∫ (x : Ω), (fun (ω : Ω) => f fun (x : ↥I) => X (↑x) ω) x ∂P) * ∫ (x : Ω), (fun (ω : Ω) => g fun (x : ↥J) => Y (↑x) ω) x ∂P)
:
ProbabilityTheory.IndepFun (fun (ω : Ω) (s : S) => X s ω) (fun (ω : Ω) (t : T) => Y t ω) P
Two stochastic processes $(X_s)_{s \in S}$ and $(Y_t)_{t \in T}$ are independent if for all $s_1, ..., s_p \in S, t_1, ..., t_q \in T$ and for all real bounded continuous functions $f$ and $g$, $$P[f(X_{s_1}, ..., X_{s_p}) g(Y_{t_1}, ..., Y_{t_q})] = P[f(X_{s_1}, ..., X_{s_p})] * P[g(Y_{t_1}, ..., Y_{t_q})].$$
theorem
indepFun_process_of_prod_bcf
{Ω : Type u_1}
{T : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{F : T → Type u_5}
{G : Type u_6}
[(t : T) → TopologicalSpace (F t)]
[(t : T) → MeasurableSpace (F t)]
[∀ (t : T), BorelSpace (F t)]
[∀ (t : T), HasOuterApproxClosed (F t)]
[TopologicalSpace G]
[MeasurableSpace G]
[BorelSpace G]
[HasOuterApproxClosed G]
{Y : (t : T) → Ω → F t}
{Z : Ω → G}
[MeasureTheory.IsZeroOrProbabilityMeasure P]
(mZ : AEMeasurable Z P)
(mY : ∀ (t : T), Measurable (Y t))
(h :
∀ (f : BoundedContinuousFunction G ℝ) (J : Finset T) (g : (t : ↥J) → BoundedContinuousFunction (F ↑t) ℝ),
∫ (x : Ω), (⇑f ∘ Z * ∏ t : ↥J, ⇑(g t) ∘ Y ↑t) x ∂P = (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (∏ t : ↥J, ⇑(g t) ∘ Y ↑t) x ∂P)
:
ProbabilityTheory.IndepFun Z (fun (ω : Ω) (t : T) => Y t ω) P
theorem
indepFun_process_of_bcf
{Ω : Type u_1}
{T : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{F : T → Type u_5}
{G : Type u_6}
[(t : T) → TopologicalSpace (F t)]
[(t : T) → MeasurableSpace (F t)]
[∀ (t : T), BorelSpace (F t)]
[∀ (t : T), HasOuterApproxClosed (F t)]
[TopologicalSpace G]
[MeasurableSpace G]
[BorelSpace G]
[HasOuterApproxClosed G]
{Y : (t : T) → Ω → F t}
{Z : Ω → G}
[MeasureTheory.IsZeroOrProbabilityMeasure P]
(mZ : AEMeasurable Z P)
(mY : ∀ (t : T), Measurable (Y t))
(h :
∀ (f : BoundedContinuousFunction G ℝ) (J : Finset T) (g : BoundedContinuousFunction ((t : ↥J) → F ↑t) ℝ),
∫ (x : Ω), (fun (ω : Ω) => f (Z ω) * g fun (x : ↥J) => Y (↑x) ω) x ∂P = (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (fun (ω : Ω) => g fun (x : ↥J) => Y (↑x) ω) x ∂P)
:
ProbabilityTheory.IndepFun Z (fun (ω : Ω) (t : T) => Y t ω) P
theorem
process_indepFun_of_prod_bcf
{Ω : Type u_1}
{S : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : S → Type u_4}
{H : Type u_7}
[(s : S) → TopologicalSpace (E s)]
[(s : S) → MeasurableSpace (E s)]
[∀ (s : S), BorelSpace (E s)]
[∀ (s : S), HasOuterApproxClosed (E s)]
[TopologicalSpace H]
[MeasurableSpace H]
[BorelSpace H]
[HasOuterApproxClosed H]
{X : (s : S) → Ω → E s}
{U : Ω → H}
[MeasureTheory.IsZeroOrProbabilityMeasure P]
(mX : ∀ (s : S), Measurable (X s))
(mU : AEMeasurable U P)
(h :
∀ (I : Finset S) (f : (s : ↥I) → BoundedContinuousFunction (E ↑s) ℝ) (g : BoundedContinuousFunction H ℝ),
∫ (x : Ω), ((∏ s : ↥I, ⇑(f s) ∘ X ↑s) * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (∏ s : ↥I, ⇑(f s) ∘ X ↑s) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P)
:
ProbabilityTheory.IndepFun (fun (ω : Ω) (s : S) => X s ω) U P
theorem
process_indepFun_of_bcf
{Ω : Type u_1}
{S : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : S → Type u_4}
{H : Type u_7}
[(s : S) → TopologicalSpace (E s)]
[(s : S) → MeasurableSpace (E s)]
[∀ (s : S), BorelSpace (E s)]
[∀ (s : S), HasOuterApproxClosed (E s)]
[TopologicalSpace H]
[MeasurableSpace H]
[BorelSpace H]
[HasOuterApproxClosed H]
{X : (s : S) → Ω → E s}
{U : Ω → H}
[MeasureTheory.IsZeroOrProbabilityMeasure P]
(mX : ∀ (s : S), Measurable (X s))
(mU : AEMeasurable U P)
(h :
∀ (I : Finset S) (f : BoundedContinuousFunction ((s : ↥I) → E ↑s) ℝ) (g : BoundedContinuousFunction H ℝ),
∫ (x : Ω), (fun (ω : Ω) => (f fun (x : ↥I) => X (↑x) ω) * g (U ω)) x ∂P = (∫ (x : Ω), (fun (ω : Ω) => f fun (x : ↥I) => X (↑x) ω) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P)
:
ProbabilityTheory.IndepFun (fun (ω : Ω) (s : S) => X s ω) U P
theorem
indicator_indepFun_process_of_prod_bcf
{Ω : Type u_1}
{S : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : S → Type u_4}
[(s : S) → TopologicalSpace (E s)]
[(s : S) → MeasurableSpace (E s)]
[∀ (s : S), BorelSpace (E s)]
[∀ (s : S), HasOuterApproxClosed (E s)]
{X : (s : S) → Ω → E s}
[MeasureTheory.IsProbabilityMeasure P]
{A : Set Ω}
(mA : MeasureTheory.NullMeasurableSet A P)
(mX : ∀ (s : S), Measurable (X s))
(h :
∀ (I : Finset S) (f : (s : ↥I) → BoundedContinuousFunction (E ↑s) ℝ),
∫ (ω : Ω) in A, ∏ s : ↥I, (f s) (X (↑s) ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s : ↥I, (f s) (X (↑s) ω) ∂P)
:
ProbabilityTheory.IndepFun (A.indicator 1) (fun (ω : Ω) (s : S) => X s ω) P
theorem
indicator_indepFun_process_of_bcf
{Ω : Type u_1}
{S : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : S → Type u_4}
[(s : S) → TopologicalSpace (E s)]
[(s : S) → MeasurableSpace (E s)]
[∀ (s : S), BorelSpace (E s)]
[∀ (s : S), HasOuterApproxClosed (E s)]
{X : (s : S) → Ω → E s}
[MeasureTheory.IsProbabilityMeasure P]
{A : Set Ω}
(mA : MeasureTheory.NullMeasurableSet A P)
(mX : ∀ (s : S), Measurable (X s))
(h :
∀ (I : Finset S) (f : BoundedContinuousFunction ((s : ↥I) → E ↑s) ℝ),
∫ (ω : Ω) in A, f fun (x : ↥I) => X (↑x) ω ∂P = P.real A * ∫ (ω : Ω), f fun (x : ↥I) => X (↑x) ω ∂P)
:
ProbabilityTheory.IndepFun (A.indicator 1) (fun (ω : Ω) (s : S) => X s ω) P
The indicator of a set $A$ and a stochastic process $(X_s)_{s \in S}$ are independent if for all $s_1, ..., s_p \in S$ and for all real bounded continuous function $f$, $$P[\mathbb{I}_A f(X_{s_1}, ..., X_{s_p})] = P(A) P[f(X_{s_1}, ..., X_{s_p})].$$
theorem
indepSets_comap_process_of_prod_bcf
{Ω : Type u_1}
{S : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : S → Type u_4}
[(s : S) → TopologicalSpace (E s)]
[(s : S) → MeasurableSpace (E s)]
[∀ (s : S), BorelSpace (E s)]
[∀ (s : S), HasOuterApproxClosed (E s)]
{X : (s : S) → Ω → E s}
[MeasureTheory.IsProbabilityMeasure P]
{𝒜 : Set (Set Ω)}
(m𝒜 : ∀ A ∈ 𝒜, MeasureTheory.NullMeasurableSet A P)
(mX : ∀ (s : S), Measurable (X s))
(h :
∀ A ∈ 𝒜,
∀ (I : Finset S) (f : (s : ↥I) → BoundedContinuousFunction (E ↑s) ℝ),
∫ (ω : Ω) in A, ∏ s : ↥I, (f s) (X (↑s) ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s : ↥I, (f s) (X (↑s) ω) ∂P)
:
ProbabilityTheory.IndepSets 𝒜 {A : Set Ω | MeasurableSet A} P
theorem
indepSets_comap_process_of_bcf
{Ω : Type u_1}
{S : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : S → Type u_4}
[(s : S) → TopologicalSpace (E s)]
[(s : S) → MeasurableSpace (E s)]
[∀ (s : S), BorelSpace (E s)]
[∀ (s : S), HasOuterApproxClosed (E s)]
{X : (s : S) → Ω → E s}
[MeasureTheory.IsProbabilityMeasure P]
{𝒜 : Set (Set Ω)}
(m𝒜 : ∀ A ∈ 𝒜, MeasureTheory.NullMeasurableSet A P)
(mX : ∀ (s : S), Measurable (X s))
(h :
∀ A ∈ 𝒜,
∀ (I : Finset S) (f : BoundedContinuousFunction ((s : ↥I) → E ↑s) ℝ),
∫ (ω : Ω) in A, f fun (x : ↥I) => X (↑x) ω ∂P = P.real A * ∫ (ω : Ω), f fun (x : ↥I) => X (↑x) ω ∂P)
:
ProbabilityTheory.IndepSets 𝒜 {A : Set Ω | MeasurableSet A} P
theorem
indep_comap_process_of_prod_bcf
{Ω : Type u_1}
{S : Type u_2}
{m mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : S → Type u_4}
[(s : S) → TopologicalSpace (E s)]
[(s : S) → MeasurableSpace (E s)]
[∀ (s : S), BorelSpace (E s)]
[∀ (s : S), HasOuterApproxClosed (E s)]
{X : (s : S) → Ω → E s}
[MeasureTheory.IsProbabilityMeasure P]
(hm : m ≤ mΩ)
(mX : ∀ (s : S), Measurable (X s))
(h :
∀ (A : Set Ω),
MeasurableSet A →
∀ (I : Finset S) (f : (s : ↥I) → BoundedContinuousFunction (E ↑s) ℝ),
∫ (ω : Ω) in A, ∏ s : ↥I, (f s) (X (↑s) ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s : ↥I, (f s) (X (↑s) ω) ∂P)
:
ProbabilityTheory.Indep m (MeasurableSpace.comap (fun (ω : Ω) (s : S) => X s ω) MeasurableSpace.pi) P
theorem
indep_comap_process_of_bcf
{Ω : Type u_1}
{S : Type u_2}
{m mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : S → Type u_4}
[(s : S) → TopologicalSpace (E s)]
[(s : S) → MeasurableSpace (E s)]
[∀ (s : S), BorelSpace (E s)]
[∀ (s : S), HasOuterApproxClosed (E s)]
{X : (s : S) → Ω → E s}
[MeasureTheory.IsProbabilityMeasure P]
(hm : m ≤ mΩ)
(mX : ∀ (s : S), Measurable (X s))
(h :
∀ (A : Set Ω),
MeasurableSet A →
∀ (I : Finset S) (f : BoundedContinuousFunction ((s : ↥I) → E ↑s) ℝ),
∫ (ω : Ω) in A, f fun (x : ↥I) => X (↑x) ω ∂P = P.real A * ∫ (ω : Ω), f fun (x : ↥I) => X (↑x) ω ∂P)
:
ProbabilityTheory.Indep m (MeasurableSpace.comap (fun (ω : Ω) (s : S) => X s ω) MeasurableSpace.pi) P
A sigma-algebra $\mathcal{A}$ and a stochastic process $(X_s)_{s \in S}$ are independent if for all $A \in \mathcal{A}$, for all $s_1, ..., s_p \in S$ and for all real bounded continuous function $f$, $$P[\mathbb{I}_A f(X_{s_1}, ..., X_{s_p})] = P(A) P[f(X_{s_1}, ..., X_{s_p})].$$