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
aemeasurable_proj
{α : Type u_4}
{δ : Type u_5}
{X : δ → Type u_6}
{mX : (a : δ) → MeasurableSpace (X a)}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{g : α → (a : δ) → X a}
(hg : AEMeasurable g μ)
(a : δ)
:
AEMeasurable (fun (x : α) => g x a) μ
theorem
coincide_on_cylinders
{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)
(h :
∀ (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)
(c : Set (T → E))
(hc : c ∈ MeasureTheory.measurableCylinders fun (x : T) => E)
:
(MeasureTheory.Measure.map (fun (ω : Ω) (t : T) => X t ω) P) c = (MeasureTheory.Measure.map (fun (ω : Ω) (t : T) => Y t ω) P) c
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)
: