theorem
modification_of_indistinduishable
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X Y : T → Ω → E}
(h : ∀ᵐ (ω : Ω) ∂P, ∀ (t : T), X t ω = Y t ω)
(t : T)
:
theorem
finite_distributions_eq
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X Y : T → Ω → E}
[MeasurableSpace E]
{I : Finset T}
(h : ∀ (t : T), X t =ᵐ[P] Y t)
:
MeasureTheory.Measure.map (fun (ω : Ω) => I.restrict fun (x : T) => X x ω) P = MeasureTheory.Measure.map (fun (ω : Ω) => I.restrict fun (x : T) => Y x ω) P
theorem
isProjectiveMeasureFamily_map_restrict
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
[MeasurableSpace E]
(hX : AEMeasurable (fun (ω : Ω) (t : T) => X t ω) P)
:
MeasureTheory.IsProjectiveMeasureFamily fun (I : Finset T) =>
MeasureTheory.Measure.map (fun (ω : Ω) => I.restrict fun (x : T) => X x ω) P
theorem
isProjectiveLimit_map
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
[MeasurableSpace E]
(hX : AEMeasurable (fun (ω : Ω) (t : T) => X t ω) P)
:
MeasureTheory.IsProjectiveLimit (MeasureTheory.Measure.map (fun (ω : Ω) (t : T) => X t ω) P) fun (I : Finset T) =>
MeasureTheory.Measure.map (fun (ω : Ω) => I.restrict fun (x : T) => X x ω) P
theorem
finite_distributions_eq_iff_same_law
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X Y : T → Ω → E}
[MeasurableSpace E]
(hX : AEMeasurable (fun (t : Ω) (ω : T) => X ω t) P)
(hY : AEMeasurable (fun (t : Ω) (ω : T) => Y ω t) P)
[MeasureTheory.IsProbabilityMeasure P]
:
(∀ (I : Finset T),
MeasureTheory.Measure.map (fun (ω : Ω) => I.restrict fun (x : T) => X x ω) P = MeasureTheory.Measure.map (fun (ω : Ω) => I.restrict fun (x : T) => Y x ω) P) ↔ MeasureTheory.Measure.map (fun (ω : Ω) (t : T) => X t ω) P = MeasureTheory.Measure.map (fun (ω : Ω) (t : T) => Y t ω) P
theorem
indistinduishable_of_modification
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X Y : T → Ω → E}
[TopologicalSpace E]
[TopologicalSpace T]
[TopologicalSpace.SeparableSpace T]
[T2Space E]
(hX : ∀ᵐ (ω : Ω) ∂P, Continuous fun (t : T) => X t ω)
(hY : ∀ᵐ (ω : Ω) ∂P, Continuous fun (t : T) => Y t ω)
(h : ∀ (t : T), X t =ᵐ[P] Y t)
: