mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
⊢ (traj κ a).map (frestrictLe b) = partialTraj κ a b

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountablyGenerated 𝓧
f : Ω → 𝓧
hf : Measurable f
⊢ ⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ
      ⇑(Kernel.id ∥ₖ (Kernel.deterministic f hf)†μ) ∘ₘ ⇑(Kernel.copy 𝓧) ∘ₘ ⇑(Kernel.deterministic f hf) ∘ₘ μ =
    ⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ ⇑(Kernel.deterministic f hf ∥ₖ Kernel.id) ∘ₘ ⇑(Kernel.copy Ω) ∘ₘ μ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Deterministic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝³ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝² : IsMarkovKernel κ
inst✝¹ : IsMarkovKernel η
inst✝ : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this : ∀ (b : β), (η b) s * t.indicator 1 b = t.indicator (fun b ↦ (η b) s) b
h₁ : ((η ∘ₖ κ) a) s = 1
b : β
⊢ s ⊆ univ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
x : (i : ↥(Iic a)) → X ↑i
⊢ Measure.map (frestrictLe b) ((traj κ a) x) = (partialTraj κ a b) x

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Deterministic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝³ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝² : IsMarkovKernel κ
inst✝¹ : IsMarkovKernel η
inst✝ : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this : ∀ (b : β), (η b) s * t.indicator 1 b = t.indicator (fun b ↦ (η b) s) b
h₁ : ((η ∘ₖ κ) a) s = 1
⊢ ∫⁻ (b : β) in t, (η b) s ∂κ a ≤ ∫⁻ (a : β) in t, 1 ∂κ a

Tactic:
by

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι✝ : Type u_1
X✝ : ι✝ → Type u_2
mX✝ : (i : ι✝) → MeasurableSpace (X✝ i)
μ✝ : (i : ι✝) → Measure (X✝ i)
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Set ι
hs : Countable ↑s
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
s_ne : Nonempty ↑s
this : s.pi t = ⋂ s', (Subtype.val '' ↑s').pi fun i ↦ if i ∈ s then t i else Set.univ
a✝ b✝ : Finset ↑s
h : a✝ ⊆ b✝
⊢ ∀ i ∈ Subtype.val '' ↑a✝, (if i ∈ s then t i else Set.univ) ⊆ if i ∈ s then t i else Set.univ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Deterministic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝³ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝² : IsMarkovKernel κ
inst✝¹ : IsMarkovKernel η
inst✝ : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this : ∀ (b : β), (η b) s * t.indicator 1 b = t.indicator (fun b ↦ (η b) s) b
h₁ : ((η ∘ₖ κ) a) s = 1
⊢ ∫⁻ (a : β) in t, 1 ∂κ a = (κ a) t

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
⊢ (traj κ b).map (frestrictLe a) = deterministic (frestrictLe₂ hab) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Deterministic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝³ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝² : IsMarkovKernel κ
inst✝¹ : IsMarkovKernel η
inst✝ : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this : ∀ (b : β), (η b) s * t.indicator 1 b = t.indicator (fun b ↦ (η b) s) b
h₁ : ((η ∘ₖ κ) a) s = 1
⊢ ∫⁻ (b : β) in t, (η b) s ∂κ a ≤ (κ a) t

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountablyGenerated 𝓧
f : Ω → 𝓧
hf : Measurable f
⊢ ⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ ⇑(Kernel.deterministic f hf ∥ₖ Kernel.id) ∘ₘ ⇑(Kernel.copy Ω) ∘ₘ μ =
    ⇑(Kernel.deterministic f hf ∥ₖ Kernel.deterministic f hf) ∘ₘ ⇑(Kernel.copy Ω) ∘ₘ μ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
hf : (fun x ↦ x (a + 1)) = (fun x ↦ x ⟨a + 1, ⋯⟩) ∘ frestrictLe (a + 1)
⊢ Measurable (frestrictLe (a + 1))

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
hf : (fun x ↦ x (a + 1)) = (fun x ↦ x ⟨a + 1, ⋯⟩) ∘ frestrictLe (a + 1)
⊢ Measurable fun x ↦ x ⟨a + 1, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι✝ : Type u_1
X✝ : ι✝ → Type u_2
mX✝ : (i : ι✝) → MeasurableSpace (X✝ i)
μ✝ : (i : ι✝) → Measure (X✝ i)
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Set ι
hs : Countable ↑s
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
s_ne : Nonempty ↑s
this : s.pi t = ⋂ s', (Subtype.val '' ↑s').pi fun i ↦ if i ∈ s then t i else Set.univ
⊢ (infinitePi μ) ((Subtype.val '' ↑{s_ne.some}).pi fun i ↦ if i ∈ s then t i else Set.univ) ≠ ∞

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountablyGenerated 𝓧
f : Ω → 𝓧
hf : Measurable f
⊢ ⇑(Kernel.deterministic f hf ∥ₖ Kernel.deterministic f hf) ∘ₘ ⇑(Kernel.copy Ω) ∘ₘ μ =
    ⇑(Kernel.copy 𝓧 ∘ₖ Kernel.deterministic f hf) ∘ₘ μ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountablyGenerated 𝓧
f : Ω → 𝓧
hf : Measurable f
⊢ ⇑(Kernel.copy 𝓧 ∘ₖ Kernel.deterministic f hf) ∘ₘ μ = Measure.map f μ ⊗ₘ Kernel.id

Tactic:
Measure.compProd_id_eq_copy_comp,

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountablyGenerated 𝓧
f : Ω → 𝓧
hf : Measurable f
⊢ ⇑(Kernel.copy 𝓧 ∘ₖ Kernel.deterministic f hf) ∘ₘ μ = ⇑(Kernel.copy 𝓧) ∘ₘ Measure.map f μ
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountablyGenerated 𝓧
f : Ω → 𝓧
hf : Measurable f
⊢ ⇑(Kernel.copy 𝓧 ∘ₖ Kernel.deterministic f hf) ∘ₘ μ = Measure.map f μ ⊗ₘ Kernel.id

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountablyGenerated 𝓧
f : Ω → 𝓧
hf : Measurable f
⊢ ⇑(Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ) =ᵐ[Measure.map f μ] ⇑Kernel.id

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
⊢ ((traj κ a).map fun x ↦ x (a + 1)) = κ a

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Deterministic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝³ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝² : IsMarkovKernel κ
inst✝¹ : IsMarkovKernel η
inst✝ : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this : ∀ (b : β), (η b) s * t.indicator 1 b = t.indicator (fun b ↦ (η b) s) b
h₁ : ((η ∘ₖ κ) a) s = 1
integral_le_kernel : ∫⁻ (b : β) in t, (η b) s ∂κ a ≤ (κ a) t
⊢ (κ a) t - ∫⁻ (a : β) in t, (η a) s ∂κ a = ∫⁻ (b : β) in t, 1 ∂κ a - ∫⁻ (b : β) in t, (η b) s ∂κ a

Tactic:
by

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι✝ : Type u_1
X✝ : ι✝ → Type u_2
mX✝ : (i : ι✝) → MeasurableSpace (X✝ i)
μ✝ : (i : ι✝) → Measure (X✝ i)
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Set ι
hs : Countable ↑s
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
s_ne : Nonempty ↑s
⊢ ∀ (i : ↑s), (μ ↑i) (t ↑i) ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
inst✝³ : IsFiniteKernel κ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ν : Measure 𝓧
inst✝ : SFinite ν
h_ac : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ν
this : (⇑κ ∘ₘ μ) ⊗ₘ κ†μ ≪ ν.prod μ
⊢ ∀ᵐ (b : 𝓧) ∂⇑κ ∘ₘ μ, (κ†μ) b ≪ μ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι✝ : Type u_1
X✝ : ι✝ → Type u_2
mX✝ : (i : ι✝) → MeasurableSpace (X✝ i)
μ✝ : (i : ι✝) → Measure (X✝ i)
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Set ι
hs : Countable ↑s
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
s_ne : Nonempty ↑s
⊢ ∀ (x : ↑s), (μ ↑x) (t ↑x) ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
inst✝³ : IsFiniteKernel κ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ν : Measure 𝓧
inst✝ : SFinite ν
h_ac : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ν
this : μ ⊗ₘ κ ≪ μ.prod ν
⊢ (⇑κ ∘ₘ μ) ⊗ₘ κ†μ ≪ ν.prod μ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Set ι
hs : Countable ↑s
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
⊢ (infinitePi μ) (s.pi t) = ∏' (i : ↑s), (μ ↑i) (t ↑i)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
inst✝³ : IsFiniteKernel κ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ν : Measure 𝓧
inst✝ : SFinite ν
h_ac : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ν
⊢ ∀ᵐ (b : 𝓧) ∂⇑κ ∘ₘ μ, (κ†μ) b ≪ μ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁶ : IsFiniteMeasure μ
inst✝⁵ : IsFiniteKernel κ
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : StandardBorelSpace 𝓧
inst✝¹ : Nonempty 𝓧
inst✝ : IsMarkovKernel κ
this : ⇑κ =ᵐ[⇑(κ†μ) ∘ₘ ⇑κ ∘ₘ μ] ⇑((κ†μ)†(⇑κ ∘ₘ μ))
⊢ ⇑((κ†μ)†(⇑κ ∘ₘ μ)) =ᵐ[μ] ⇑κ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst✝ : Countable ι
t : (i : ι) → Set (X i)
mt : ∀ (i : ι), MeasurableSet (t i)
⊢ (infinitePi μ) (Set.univ.pi t) = ∏' (i : ι), (μ i) (t i)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Deterministic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝³ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝² : IsMarkovKernel κ
inst✝¹ : IsMarkovKernel η
inst✝ : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this : ∀ (b : β), (η b) s * t.indicator 1 b = t.indicator (fun b ↦ (η b) s) b
h₁ : ((η ∘ₖ κ) a) s = 1
integral_le_kernel : ∫⁻ (b : β) in t, (η b) s ∂κ a ≤ (κ a) t
⊢ (κ a) t ≠ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst✝¹ : Countable ι
inst✝ : ∀ (i : ι), MeasurableSingletonClass (X i)
f : (i : ι) → X i
⊢ ∀ (i : ι), MeasurableSet {f i}

Tactic:
by

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst✝¹ : Countable ι
inst✝ : ∀ (i : ι), MeasurableSingletonClass (X i)
f : (i : ι) → X i
⊢ (infinitePi μ) {f} = ∏' (i : ι), (μ i) {f i}

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁶ : IsFiniteMeasure μ
inst✝⁵ : IsFiniteKernel κ
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : StandardBorelSpace 𝓧
inst✝¹ : Nonempty 𝓧
inst✝ : IsMarkovKernel κ
⊢ ⇑((κ†μ)†(⇑κ ∘ₘ μ)) =ᵐ[μ] ⇑κ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), MeasurableSingletonClass (X i)
f : (i : ι) → X i
⊢ (infinitePi μ) {f} = ∏ i, (μ i) {f i}

Tactic:
by

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
f : (i : ι) → X i
⊢ ∀ (s : Finset ι) (t : (i : ι) → Set (X i)),
    (∀ (i : ι), MeasurableSet (t i)) → (dirac f) ((↑s).pi t) = ∏ i ∈ s, (dirac (f i)) (t i)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
⊢ Measurable (Function.eval i)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
s : Set (X i)
hs : MeasurableSet s
⊢ i ∈ {i}

Tactic:
by

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
s : Set (X i)
hs : MeasurableSet s
⊢ Function.eval i = Function.eval ⟨i, ⋯⟩ ∘ {i}.restrict

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Deterministic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝³ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝² : IsMarkovKernel κ
inst✝¹ : IsMarkovKernel η
inst✝ : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this : ∀ (b : β), (η b) s * t.indicator 1 b = t.indicator (fun b ↦ (η b) s) b
h₁ : ((η ∘ₖ κ) a) s = 1
integral_le_kernel : ∫⁻ (b : β) in t, (η b) s ∂κ a ≤ (κ a) t
b : β
⊢ s ⊆ univ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Deterministic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝³ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝² : IsMarkovKernel κ
inst✝¹ : IsMarkovKernel η
inst✝ : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this : ∀ (b : β), (η b) s * t.indicator 1 b = t.indicator (fun b ↦ (η b) s) b
h₁ : ((η ∘ₖ κ) a) s = 1
integral_le_kernel : ∫⁻ (b : β) in t, (η b) s ∂κ a ≤ (κ a) t
⊢ ∫⁻ (b : β) in t, 1 ∂κ a - ∫⁻ (b : β) in t, (η b) s ∂κ a = ∫⁻ (b : β) in t, 1 - (η b) s ∂κ a

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁶ : IsFiniteMeasure μ
inst✝⁵ : IsFiniteKernel κ
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : StandardBorelSpace 𝓧
inst✝¹ : Nonempty 𝓧
η : Kernel 𝓧 𝓨
inst✝ : IsFiniteKernel η
⊢ (⇑(η ∘ₖ κ) ∘ₘ μ) ⊗ₘ (κ†μ ∘ₖ η†(⇑κ ∘ₘ μ)) = ⇑(Kernel.swap Ω 𝓨) ∘ₘ μ ⊗ₘ (η ∘ₖ κ)

Tactic:
simp_rw [Measure.compProd_eq_comp_prod, ← Kernel.parallelComp_comp_copy,
    ← Kernel.parallelComp_id_left_comp_parallelComp, ← Measure.comp_assoc]

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁶ : IsFiniteMeasure μ
inst✝⁵ : IsFiniteKernel κ
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : StandardBorelSpace 𝓧
inst✝¹ : Nonempty 𝓧
η : Kernel 𝓧 𝓨
inst✝ : IsFiniteKernel η
⊢ ⇑(Kernel.id ∥ₖ κ†μ) ∘ₘ ⇑(Kernel.id ∥ₖ η†(⇑κ ∘ₘ μ)) ∘ₘ ⇑(Kernel.copy 𝓨) ∘ₘ ⇑η ∘ₘ ⇑κ ∘ₘ μ =
    ⇑(Kernel.swap Ω 𝓨) ∘ₘ ⇑(Kernel.id ∥ₖ η) ∘ₘ ⇑(Kernel.id ∥ₖ κ) ∘ₘ ⇑(Kernel.copy Ω) ∘ₘ μ
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁶ : IsFiniteMeasure μ
inst✝⁵ : IsFiniteKernel κ
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : StandardBorelSpace 𝓧
inst✝¹ : Nonempty 𝓧
η : Kernel 𝓧 𝓨
inst✝ : IsFiniteKernel η
⊢ ⇑(Kernel.id ∥ₖ κ†μ) ∘ₘ ⇑(Kernel.id ∥ₖ η†(⇑κ ∘ₘ μ)) ∘ₘ ⇑(Kernel.copy 𝓨) ∘ₘ ⇑η ∘ₘ ⇑κ ∘ₘ μ =
    ⇑(Kernel.id ∥ₖ κ†μ) ∘ₘ ⇑(η ∥ₖ Kernel.id) ∘ₘ ⇑(Kernel.copy 𝓧) ∘ₘ ⇑κ ∘ₘ μ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a n : ℕ
η : Kernel ((i : ↥(Iic a)) → X ↑i) ((n : ℕ) → X n)
hη : ∀ b ≥ n, η.map (frestrictLe b) = partialTraj κ a b
⊢ η = traj κ a

Tactic:
by

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
⊢ map (Function.eval i) (infinitePi μ) = μ i

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Deterministic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝³ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝² : IsMarkovKernel κ
inst✝¹ : IsMarkovKernel η
inst✝ : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this : ∀ (b : β), (η b) s * t.indicator 1 b = t.indicator (fun b ↦ (η b) s) b
h₁ : ((η ∘ₖ κ) a) s = 1
integral_le_kernel : ∫⁻ (b : β) in t, (η b) s ∂κ a ≤ (κ a) t
x : β
⊢ (η x) s ≠ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
Y : ι → Type u_3
inst✝ : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hf : ∀ (i : ι), Measurable (f i)
this : ∀ (i : ι), IsProbabilityMeasure (map (f i) (μ i))
s : Finset ι
t : (i : ι) → Set (Y i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ Measurable fun x i ↦ f i (x i)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁶ : IsFiniteMeasure μ
inst✝⁵ : IsFiniteKernel κ
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : StandardBorelSpace 𝓧
inst✝¹ : Nonempty 𝓧
η : Kernel 𝓧 𝓨
inst✝ : IsFiniteKernel η
⊢ ⇑(Kernel.id ∥ₖ κ†μ) ∘ₘ ⇑(η ∥ₖ Kernel.id) ∘ₘ ⇑(Kernel.copy 𝓧) ∘ₘ ⇑κ ∘ₘ μ =
    ⇑(η ∥ₖ Kernel.id) ∘ₘ ⇑(Kernel.id ∥ₖ κ†μ) ∘ₘ ⇑(Kernel.copy 𝓧) ∘ₘ ⇑κ ∘ₘ μ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
⊢ traj κ b ∘ₖ partialTraj κ a b = traj κ a

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁶ : IsFiniteMeasure μ
inst✝⁵ : IsFiniteKernel κ
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : StandardBorelSpace 𝓧
inst✝¹ : Nonempty 𝓧
η : Kernel 𝓧 𝓨
inst✝ : IsFiniteKernel η
⊢ ⇑(η ∥ₖ Kernel.id) ∘ₘ ⇑(Kernel.id ∥ₖ κ†μ) ∘ₘ ⇑(Kernel.copy 𝓧) ∘ₘ ⇑κ ∘ₘ μ =
    ⇑(η ∥ₖ Kernel.id) ∘ₘ ⇑(κ ∥ₖ Kernel.id) ∘ₘ ⇑(Kernel.copy Ω) ∘ₘ μ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
Y : ι → Type u_3
inst✝ : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hf : ∀ (i : ι), Measurable (f i)
this : ∀ (i : ι), IsProbabilityMeasure (map (f i) (μ i))
s : Finset ι
t : (i : ι) → Set (Y i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ (fun x i ↦ f i (x i)) ⁻¹' (↑s).pi t = (↑s).pi fun i ↦ f i ⁻¹' t i

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Deterministic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝³ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝² : IsMarkovKernel κ
inst✝¹ : IsMarkovKernel η
inst✝ : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this : ∀ (b : β), (η b) s * t.indicator 1 b = t.indicator (fun b ↦ (η b) s) b
h₁ : ((η ∘ₖ κ) a) s = 1
integral_le_kernel : ∫⁻ (b : β) in t, (η b) s ∂κ a ≤ (κ a) t
⊢ ∫⁻ (b : β), 1 - (η b) s ∂κ a = ∫⁻ (x : β), (η x) sᶜ ∂κ a

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Deterministic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝³ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝² : IsMarkovKernel κ
inst✝¹ : IsMarkovKernel η
inst✝ : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this : ∀ (b : β), (η b) s * t.indicator 1 b = t.indicator (fun b ↦ (η b) s) b
h₁ : ((η ∘ₖ κ) a) s = 1
integral_le_kernel : ∫⁻ (b : β) in t, (η b) s ∂κ a ≤ (κ a) t
⊢ ∫⁻ (x : β), (η x) sᶜ ∂κ a = ((η ∘ₖ κ) a) sᶜ

Tactic:
by

Goal state after: