Indistinguishability of processes

In Mathlib, E-valued stochastic processes over a probability space Ω and indexed by a type ι are represented as a family of E-valued random variables X : ι → Ω → E rather than as an ι → E-valued random variable, following the convention on paper.

Two stochastic processes are said to be indistinguishable if they are almost everywhere equal as ι → E-valued random variable, i.e. (fun ω t ↦ X t ω) =ᵐ[P] (fun ω t ↦ Y t ω). This spelling creates a lot of friction when manipulating indistinguishable processes, making it harder to use for instance the gcongr tactic.

In this file we introduce a predicate Indistinguishable P X Y, denoted X ≡ᵐ[P] Y, which states that ∀ᵐ ω ∂P, ∀ t, X t ω = Y t ω. The symbol ≡ can be typed with \==.

The recommended spelling for Indistinguishable in names is indist.

def ProbabilityTheory.Indistinguishable {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} (P : MeasureTheory.Measure Ω) (X Y : ι → Ω → E) : Prop

Two processes are indistinguishable if almost surely they agree everywhere.

Equations

• (X ≡ᵐ[P] Y) = ∀ᵐ (ω : Ω) ∂P, ∀ (t : ι), X t ω = Y t ω

def ProbabilityTheory.«term_≡ᵐ[_]_» : Lean.TrailingParserDescr

Two processes are indistinguishable if almost surely they agree everywhere.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ProbabilityTheory.Indistinguishable.refl {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} (P : MeasureTheory.Measure Ω) (X : ι → Ω → E) : X ≡ᵐ[P] X

theorem ProbabilityTheory.Indistinguishable.rfl {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : ι → Ω → E} : X ≡ᵐ[P] X

theorem ProbabilityTheory.Indistinguishable.symm {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X Y : ι → Ω → E} (h : X ≡ᵐ[P] Y) : Y ≡ᵐ[P] X

theorem ProbabilityTheory.Indistinguishable.trans {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X Y Z : ι → Ω → E} (h1 : X ≡ᵐ[P] Y) (h2 : Y ≡ᵐ[P] Z) : X ≡ᵐ[P] Z

instance ProbabilityTheory.Indistinguishable.instIsTransForallForall {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} : IsTrans (ι → Ω → E) fun (x1 x2 : ι → Ω → E) => x1 ≡ᵐ[P] x2

theorem ProbabilityTheory.Indistinguishable.fun_comp {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X Y : ι → Ω → E} {F : Type u_4} (h : X ≡ᵐ[P] Y) (f : E → F) : (fun (t : ι) (ω : Ω) => f (X t ω)) ≡ᵐ[P] fun (t : ι) (ω : Ω) => f (Y t ω)

theorem ProbabilityTheory.Indistinguishable.fun_comp₂ {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X Y : ι → Ω → E} {F : Type u_4} {G : Type u_5} {Z T : ι → Ω → F} (h1 : X ≡ᵐ[P] Y) (h2 : Z ≡ᵐ[P] T) (f : E → F → G) : (fun (t : ι) (ω : Ω) => f (X t ω) (Z t ω)) ≡ᵐ[P] fun (t : ι) (ω : Ω) => f (Y t ω) (T t ω)

theorem ProbabilityTheory.Indistinguishable.inv {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X Y : ι → Ω → E} [Inv E] (h : X ≡ᵐ[P] Y) : X⁻¹ ≡ᵐ[P] Y⁻¹

theorem ProbabilityTheory.Indistinguishable.neg {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X Y : ι → Ω → E} [Neg E] (h : X ≡ᵐ[P] Y) : -X ≡ᵐ[P] -Y

theorem ProbabilityTheory.Indistinguishable.fun_neg {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X Y : ι → Ω → E} [Neg E] (h : X ≡ᵐ[P] Y) : (fun (i : ι) (i_1 : Ω) => -X i i_1) ≡ᵐ[P] fun (i : ι) (i_1 : Ω) => -Y i i_1

Eta-expanded form of ProbabilityTheory.Indistinguishable.neg

theorem ProbabilityTheory.Indistinguishable.fun_inv {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X Y : ι → Ω → E} [Inv E] (h : X ≡ᵐ[P] Y) : (fun (i : ι) (i_1 : Ω) => (X i i_1)⁻¹) ≡ᵐ[P] fun (i : ι) (i_1 : Ω) => (Y i i_1)⁻¹

Eta-expanded form of ProbabilityTheory.Indistinguishable.inv

theorem ProbabilityTheory.Indistinguishable.mul {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X Y : ι → Ω → E} [Mul E] {Z T : ι → Ω → E} (h1 : X ≡ᵐ[P] Y) (h2 : Z ≡ᵐ[P] T) : X * Z ≡ᵐ[P] Y * T

theorem ProbabilityTheory.Indistinguishable.add {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X Y : ι → Ω → E} [Add E] {Z T : ι → Ω → E} (h1 : X ≡ᵐ[P] Y) (h2 : Z ≡ᵐ[P] T) : X + Z ≡ᵐ[P] Y + T

theorem ProbabilityTheory.Indistinguishable.fun_mul {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X Y : ι → Ω → E} [Mul E] {Z T : ι → Ω → E} (h1 : X ≡ᵐ[P] Y) (h2 : Z ≡ᵐ[P] T) : (fun (i : ι) (i_1 : Ω) => X i i_1 * Z i i_1) ≡ᵐ[P] fun (i : ι) (i_1 : Ω) => Y i i_1 * T i i_1

Eta-expanded form of ProbabilityTheory.Indistinguishable.mul

theorem ProbabilityTheory.Indistinguishable.fun_add {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X Y : ι → Ω → E} [Add E] {Z T : ι → Ω → E} (h1 : X ≡ᵐ[P] Y) (h2 : Z ≡ᵐ[P] T) : (fun (i : ι) (i_1 : Ω) => X i i_1 + Z i i_1) ≡ᵐ[P] fun (i : ι) (i_1 : Ω) => Y i i_1 + T i i_1

Eta-expanded form of ProbabilityTheory.Indistinguishable.add

theorem ProbabilityTheory.Indistinguishable.div {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X Y : ι → Ω → E} [Div E] {Z T : ι → Ω → E} (h1 : X ≡ᵐ[P] Y) (h2 : Z ≡ᵐ[P] T) : X / Z ≡ᵐ[P] Y / T

theorem ProbabilityTheory.Indistinguishable.sub {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X Y : ι → Ω → E} [Sub E] {Z T : ι → Ω → E} (h1 : X ≡ᵐ[P] Y) (h2 : Z ≡ᵐ[P] T) : X - Z ≡ᵐ[P] Y - T

theorem ProbabilityTheory.Indistinguishable.fun_div {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X Y : ι → Ω → E} [Div E] {Z T : ι → Ω → E} (h1 : X ≡ᵐ[P] Y) (h2 : Z ≡ᵐ[P] T) : (fun (i : ι) (i_1 : Ω) => X i i_1 / Z i i_1) ≡ᵐ[P] fun (i : ι) (i_1 : Ω) => Y i i_1 / T i i_1

Eta-expanded form of ProbabilityTheory.Indistinguishable.div

theorem ProbabilityTheory.Indistinguishable.fun_sub {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X Y : ι → Ω → E} [Sub E] {Z T : ι → Ω → E} (h1 : X ≡ᵐ[P] Y) (h2 : Z ≡ᵐ[P] T) : (fun (i : ι) (i_1 : Ω) => X i i_1 - Z i i_1) ≡ᵐ[P] fun (i : ι) (i_1 : Ω) => Y i i_1 - T i i_1

Eta-expanded form of ProbabilityTheory.Indistinguishable.sub

theorem ProbabilityTheory.Indistinguishable.smul {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X Y : ι → Ω → E} {F : Type u_4} {Z T : ι → Ω → F} [SMul F E] (h1 : X ≡ᵐ[P] Y) (h2 : Z ≡ᵐ[P] T) : Z • X ≡ᵐ[P] T • Y

theorem ProbabilityTheory.Indistinguishable.vadd {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X Y : ι → Ω → E} {F : Type u_4} {Z T : ι → Ω → F} [VAdd F E] (h1 : X ≡ᵐ[P] Y) (h2 : Z ≡ᵐ[P] T) : Z +ᵥ X ≡ᵐ[P] T +ᵥ Y

theorem ProbabilityTheory.Indistinguishable.fun_smul {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X Y : ι → Ω → E} {F : Type u_4} {Z T : ι → Ω → F} [SMul F E] (h1 : X ≡ᵐ[P] Y) (h2 : Z ≡ᵐ[P] T) : (fun (i : ι) (i_1 : Ω) => Z i i_1 • X i i_1) ≡ᵐ[P] fun (i : ι) (i_1 : Ω) => T i i_1 • Y i i_1

Eta-expanded form of ProbabilityTheory.Indistinguishable.smul

theorem ProbabilityTheory.Indistinguishable.fun_vadd {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X Y : ι → Ω → E} {F : Type u_4} {Z T : ι → Ω → F} [VAdd F E] (h1 : X ≡ᵐ[P] Y) (h2 : Z ≡ᵐ[P] T) : (fun (i : ι) (i_1 : Ω) => Z i i_1 +ᵥ X i i_1) ≡ᵐ[P] fun (i : ι) (i_1 : Ω) => T i i_1 +ᵥ Y i i_1

Eta-expanded form of ProbabilityTheory.Indistinguishable.vadd

theorem ProbabilityTheory.Indistinguishable.const_smul {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X Y : ι → Ω → E} {F : Type u_4} [SMul F E] {c : F} (h : X ≡ᵐ[P] Y) : c • X ≡ᵐ[P] c • Y

theorem ProbabilityTheory.Indistinguishable.const_vadd {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X Y : ι → Ω → E} {F : Type u_4} [VAdd F E] {c : F} (h : X ≡ᵐ[P] Y) : c +ᵥ X ≡ᵐ[P] c +ᵥ Y

theorem ProbabilityTheory.Indistinguishable.fun_const_smul {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X Y : ι → Ω → E} {F : Type u_4} [SMul F E] {c : F} (h : X ≡ᵐ[P] Y) : (fun (i : ι) (i_1 : Ω) => c • X i i_1) ≡ᵐ[P] fun (i : ι) (i_1 : Ω) => c • Y i i_1

Eta-expanded form of ProbabilityTheory.Indistinguishable.const_smul

theorem ProbabilityTheory.Indistinguishable.fun_const_vadd {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X Y : ι → Ω → E} {F : Type u_4} [VAdd F E] {c : F} (h : X ≡ᵐ[P] Y) : (fun (i : ι) (i_1 : Ω) => c +ᵥ X i i_1) ≡ᵐ[P] fun (i : ι) (i_1 : Ω) => c +ᵥ Y i i_1

Eta-expanded form of ProbabilityTheory.Indistinguishable.const_vadd

theorem ProbabilityTheory.Indistinguishable.prodMk {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X Y : ι → Ω → E} {F : Type u_4} {Z T : ι → Ω → F} (h1 : X ≡ᵐ[P] Y) (h2 : Z ≡ᵐ[P] T) : (fun (t : ι) (ω : Ω) => (X t ω, Z t ω)) ≡ᵐ[P] fun (t : ι) (ω : Ω) => (Y t ω, T t ω)

theorem ProbabilityTheory.Indistinguishable.ae_eq {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X Y : ι → Ω → E} (h : X ≡ᵐ[P] Y) : (fun (ω : Ω) (t : ι) => X t ω) =ᵐ[P] fun (ω : Ω) (t : ι) => Y t ω

theorem ProbabilityTheory.Indistinguishable.ae_eq_eval {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X Y : ι → Ω → E} (h : X ≡ᵐ[P] Y) (t : ι) : X t =ᵐ[P] Y t

theorem Filter.EventuallyEq.indist {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X Y : ι → Ω → E} (h : (fun (ω : Ω) (t : ι) => X t ω) =ᵐ[P] fun (ω : Ω) (t : ι) => Y t ω) : X ≡ᵐ[P] Y