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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
Ω' : Type u_5
mΩ' : MeasurableSpace Ω'
inst✝¹ : StandardBorelSpace Ω'
inst✝ : Nonempty Ω'
X : α → β
hY : AEMeasurable Y μ
f : Ω → Ω'
hf : Measurable f
hX : AEMeasurable X μ
⊢ ⇑(condDistrib (f ∘ Y) X μ) =ᵐ[Measure.map X μ] ⇑((condDistrib Y X μ).map f)

pp: case neg
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
Ω' : Type u_5
mΩ' : MeasurableSpace Ω'
inst✝¹ : StandardBorelSpace Ω'
inst✝ : Nonempty Ω'
X : α → β
hY : AEMeasurable Y μ
f : Ω → Ω'
hf : Measurable f
hX : ¬AEMeasurable X μ
⊢ ⇑(condDistrib (f ∘ Y) X μ) =ᵐ[Measure.map X μ] ⇑((condDistrib Y X μ).map f)

Tactic:
swap

Goal state after:
case neg
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
Ω' : Type u_5
mΩ' : MeasurableSpace Ω'
inst✝¹ : StandardBorelSpace Ω'
inst✝ : Nonempty Ω'
X : α → β
hY : AEMeasurable Y μ
f : Ω → Ω'
hf : Measurable f
hX : ¬AEMeasurable X μ
⊢ ⇑(condDistrib (f ∘ Y) X μ) =ᵐ[Measure.map X μ] ⇑((condDistrib Y X μ).map f)

case pos
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
Ω' : Type u_5
mΩ' : MeasurableSpace Ω'
inst✝¹ : StandardBorelSpace Ω'
inst✝ : Nonempty Ω'
X : α → β
hY : AEMeasurable Y μ
f : Ω → Ω'
hf : Measurable f
hX : AEMeasurable X μ
⊢ ⇑(condDistrib (f ∘ Y) X μ) =ᵐ[Measure.map X μ] ⇑((condDistrib Y X μ).map f)
Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel

Goal state before:
pp: α : Type u_1
Ω : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
a : α
⊢ ρ.condKernel a = (const Unit ρ).condKernelUnitBorel ((), a)

Tactic:
rw [Measure.condKernel]

Goal state after:
α : Type u_1
Ω : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
a : α
⊢ ((const Unit ρ).condKernelUnitBorel.comap (fun a ↦ ((), a)) ⋯) a = (const Unit ρ).condKernelUnitBorel ((), a)
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case compl
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A✝ : Set γ
this : IsFiniteKernel κ
hgen : mγ = generateFrom {s | ∃ n, MeasurableSet s}
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
A : Set γ
hA : MeasurableSet A
hA_eq : ∫ (x : γ) in A, κ.density ν a x s ∂ν a = (κ a).real (A ×ˢ s)
h : ∫ (x : γ) in A, κ.density ν a x s ∂ν a + ∫ (x : γ) in Aᶜ, κ.density ν a x s ∂ν a = ∫ (x : γ), κ.density ν a x s ∂ν a
⊢ ∫ (x : γ) in Aᶜ, κ.density ν a x s ∂ν a = (κ a).real (Aᶜ ×ˢ s)

Tactic:
rw [hA_eq, integral_density hκν a hs] at h

Goal state after:
case compl
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A✝ : Set γ
this : IsFiniteKernel κ
hgen : mγ = generateFrom {s | ∃ n, MeasurableSet s}
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
A : Set γ
hA : MeasurableSet A
hA_eq : ∫ (x : γ) in A, κ.density ν a x s ∂ν a = (κ a).real (A ×ˢ s)
h : (κ a).real (A ×ˢ s) + ∫ (x : γ) in Aᶜ, κ.density ν a x s ∂ν a = (κ a).real (univ ×ˢ s)
⊢ ∫ (x : γ) in Aᶜ, κ.density ν a x s ∂ν a = (κ a).real (Aᶜ ×ˢ s)
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
mβ : MeasurableSpace β
X : α → β
f : β → Ω
hf : Measurable f
hX : AEMeasurable X μ
⊢ ⇑(condDistrib (f ∘ X) X μ) =ᵐ[Measure.map X μ] ⇑(Kernel.deterministic f hf)

pp: case neg
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
mβ : MeasurableSpace β
X : α → β
f : β → Ω
hf : Measurable f
hX : ¬AEMeasurable X μ
⊢ ⇑(condDistrib (f ∘ X) X μ) =ᵐ[Measure.map X μ] ⇑(Kernel.deterministic f hf)

Tactic:
swap

Goal state after:
case neg
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
mβ : MeasurableSpace β
X : α → β
f : β → Ω
hf : Measurable f
hX : ¬AEMeasurable X μ
⊢ ⇑(condDistrib (f ∘ X) X μ) =ᵐ[Measure.map X μ] ⇑(Kernel.deterministic f hf)

case pos
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
mβ : MeasurableSpace β
X : α → β
f : β → Ω
hf : Measurable f
hX : AEMeasurable X μ
⊢ ⇑(condDistrib (f ∘ X) X μ) =ᵐ[Measure.map X μ] ⇑(Kernel.deterministic f hf)
Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁴ : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ✝ : Measure (α × Ω)
inst✝¹ : IsFiniteMeasure ρ✝
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
⊢ IsMarkovKernel ρ.condKernel

Tactic:
rw [Measure.condKernel]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁴ : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ✝ : Measure (α × Ω)
inst✝¹ : IsFiniteMeasure ρ✝
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
⊢ IsMarkovKernel ((const Unit ρ).condKernelUnitBorel.comap (fun a ↦ ((), a)) ⋯)
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
γ : Type u_5
mγ : MeasurableSpace γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst✝ : IsProbabilityMeasure ν
hX : AEMeasurable X μ
⊢ ⇑(condDistrib (fun ω ↦ Y ω.1) (fun ω ↦ X ω.1) (μ.prod ν)) =ᵐ[Measure.map X μ] ⇑(condDistrib Y X μ)

pp: case neg
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
γ : Type u_5
mγ : MeasurableSpace γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst✝ : IsProbabilityMeasure ν
hX : ¬AEMeasurable X μ
⊢ ⇑(condDistrib (fun ω ↦ Y ω.1) (fun ω ↦ X ω.1) (μ.prod ν)) =ᵐ[Measure.map X μ] ⇑(condDistrib Y X μ)

Tactic:
swap

Goal state after:
case neg
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
γ : Type u_5
mγ : MeasurableSpace γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst✝ : IsProbabilityMeasure ν
hX : ¬AEMeasurable X μ
⊢ ⇑(condDistrib (fun ω ↦ Y ω.1) (fun ω ↦ X ω.1) (μ.prod ν)) =ᵐ[Measure.map X μ] ⇑(condDistrib Y X μ)

case pos
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
γ : Type u_5
mγ : MeasurableSpace γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst✝ : IsProbabilityMeasure ν
hX : AEMeasurable X μ
⊢ ⇑(condDistrib (fun ω ↦ Y ω.1) (fun ω ↦ X ω.1) (μ.prod ν)) =ᵐ[Measure.map X μ] ⇑(condDistrib Y X μ)
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
γ : Type u_5
mγ : MeasurableSpace γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst✝ : IsProbabilityMeasure ν
hX : AEMeasurable X μ
⊢ ⇑(condDistrib (fun ω ↦ Y ω.2) (fun ω ↦ X ω.2) (ν.prod μ)) =ᵐ[Measure.map X μ] ⇑(condDistrib Y X μ)

pp: case neg
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
γ : Type u_5
mγ : MeasurableSpace γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst✝ : IsProbabilityMeasure ν
hX : ¬AEMeasurable X μ
⊢ ⇑(condDistrib (fun ω ↦ Y ω.2) (fun ω ↦ X ω.2) (ν.prod μ)) =ᵐ[Measure.map X μ] ⇑(condDistrib Y X μ)

Tactic:
swap

Goal state after:
case neg
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
γ : Type u_5
mγ : MeasurableSpace γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst✝ : IsProbabilityMeasure ν
hX : ¬AEMeasurable X μ
⊢ ⇑(condDistrib (fun ω ↦ Y ω.2) (fun ω ↦ X ω.2) (ν.prod μ)) =ᵐ[Measure.map X μ] ⇑(condDistrib Y X μ)

case pos
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
γ : Type u_5
mγ : MeasurableSpace γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst✝ : IsProbabilityMeasure ν
hX : AEMeasurable X μ
⊢ ⇑(condDistrib (fun ω ↦ Y ω.2) (fun ω ↦ X ω.2) (ν.prod μ)) =ᵐ[Measure.map X μ] ⇑(condDistrib Y X μ)
Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps

Goal state before:
pp: case refine_3
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrder ι
inst✝¹ : DecidableLE ι
X : ι → Type u_2
inst✝ : LocallyFiniteOrderBot ι
a b : ι
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X ↑i)
x : ((i : ↥(Iic a)) → X ↑i) × ((i : ↥(Ioc a b)) → X ↑i)
x✝ :
  (∀ (a_1 : ι) (b_1 : a_1 ≤ a), x.1 ⟨a_1, ⋯⟩ ∈ s ⟨a_1, ⋯⟩) ∧
    ∀ (a_1 : ι) (b_1 : a < a_1 ∧ a_1 ≤ b), x.2 ⟨a_1, ⋯⟩ ∈ s ⟨a_1, ⋯⟩
i : ι
hi : i ≤ b
h1 : ∀ (a_1 : ι) (b_1 : a_1 ≤ a), x.1 ⟨a_1, ⋯⟩ ∈ s ⟨a_1, ⋯⟩
h2 : ∀ (a_1 : ι) (b_1 : a < a_1 ∧ a_1 ≤ b), x.2 ⟨a_1, ⋯⟩ ∈ s ⟨a_1, ⋯⟩
⊢ (if h : i ≤ a then x.1 ⟨i, ⋯⟩ else x.2 ⟨i, ⋯⟩) ∈ s ⟨i, ⋯⟩

Tactic:
split_ifs with hi3

Goal state after:
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrder ι
inst✝¹ : DecidableLE ι
X : ι → Type u_2
inst✝ : LocallyFiniteOrderBot ι
a b : ι
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X ↑i)
x : ((i : ↥(Iic a)) → X ↑i) × ((i : ↥(Ioc a b)) → X ↑i)
x✝ :
  (∀ (a_1 : ι) (b_1 : a_1 ≤ a), x.1 ⟨a_1, ⋯⟩ ∈ s ⟨a_1, ⋯⟩) ∧
    ∀ (a_1 : ι) (b_1 : a < a_1 ∧ a_1 ≤ b), x.2 ⟨a_1, ⋯⟩ ∈ s ⟨a_1, ⋯⟩
i : ι
hi : i ≤ b
h1 : ∀ (a_1 : ι) (b_1 : a_1 ≤ a), x.1 ⟨a_1, ⋯⟩ ∈ s ⟨a_1, ⋯⟩
h2 : ∀ (a_1 : ι) (b_1 : a < a_1 ∧ a_1 ≤ b), x.2 ⟨a_1, ⋯⟩ ∈ s ⟨a_1, ⋯⟩
hi3 : i ≤ a
⊢ x.1 ⟨i, ⋯⟩ ∈ s ⟨i, ⋯⟩

case neg
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrder ι
inst✝¹ : DecidableLE ι
X : ι → Type u_2
inst✝ : LocallyFiniteOrderBot ι
a b : ι
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X ↑i)
x : ((i : ↥(Iic a)) → X ↑i) × ((i : ↥(Ioc a b)) → X ↑i)
x✝ :
  (∀ (a_1 : ι) (b_1 : a_1 ≤ a), x.1 ⟨a_1, ⋯⟩ ∈ s ⟨a_1, ⋯⟩) ∧
    ∀ (a_1 : ι) (b_1 : a < a_1 ∧ a_1 ≤ b), x.2 ⟨a_1, ⋯⟩ ∈ s ⟨a_1, ⋯⟩
i : ι
hi : i ≤ b
h1 : ∀ (a_1 : ι) (b_1 : a_1 ≤ a), x.1 ⟨a_1, ⋯⟩ ∈ s ⟨a_1, ⋯⟩
h2 : ∀ (a_1 : ι) (b_1 : a < a_1 ∧ a_1 ≤ b), x.2 ⟨a_1, ⋯⟩ ∈ s ⟨a_1, ⋯⟩
hi3 : ¬i ≤ a
⊢ x.2 ⟨i, ⋯⟩ ∈ s ⟨i, ⋯⟩
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inr
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
hab✝ : a ≤ b
hab : a < b
⊢ (if h : b ≤ a then deterministic (frestrictLe₂ h) ⋯
    else
      Nat.leRec Kernel.id
        (fun k x κ_k ↦ (Kernel.id ×ₖ (κ k).map ⇑(piSingleton k) ∘ₖ κ_k).map (_root_.IicProdIoc k (k + 1))) ⋯) =
    Nat.leRec Kernel.id
      (fun k x κ_k ↦ (Kernel.id ×ₖ (κ k).map ⇑(piSingleton k) ∘ₖ κ_k).map (_root_.IicProdIoc k (k + 1))) hab✝

Tactic:
dif_neg (not_le.2 hab)

Goal state after:
case inr
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
hab✝ : a ≤ b
hab : a < b
⊢ Nat.leRec Kernel.id (fun k x κ_k ↦ (Kernel.id ×ₖ (κ k).map ⇑(piSingleton k) ∘ₖ κ_k).map (_root_.IicProdIoc k (k + 1)))
      ⋯ =
    Nat.leRec Kernel.id
      (fun k x κ_k ↦ (Kernel.id ×ₖ (κ k).map ⇑(piSingleton k) ∘ₖ κ_k).map (_root_.IicProdIoc k (k + 1))) hab✝
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
h_cont : ContinuousAt ENNReal.toReal ((κ a) univ)
⊢ Tendsto (fun m ↦ (κ a).real (univ ×ˢ seq m)) atTop (𝓝 ((κ a).real univ))

pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
⊢ {a | a ≠ ∞} ∈ 𝓝 ((κ a) univ)

Tactic:
swap

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
⊢ {a | a ≠ ∞} ∈ 𝓝 ((κ a) univ)

case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
h_cont : ContinuousAt ENNReal.toReal ((κ a) univ)
⊢ Tendsto (fun m ↦ (κ a).real (univ ×ˢ seq m)) atTop (𝓝 ((κ a).real univ))
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
hab : a ≤ b
⊢ Nat.leRec Kernel.id (fun k x κ_k ↦ (Kernel.id ×ₖ (κ k).map ⇑(piSingleton k) ∘ₖ κ_k).map (_root_.IicProdIoc k (k + 1)))
      ⋯ =
    (Kernel.id ×ₖ (κ b).map ⇑(piSingleton b) ∘ₖ partialTraj κ a b).map (_root_.IicProdIoc b (b + 1))

Tactic:
induction b, hab using Nat.le_induction with

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

Goal state before:
pp: case inl
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a✝ b✝ c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
a b : ℕ
hab : a ≤ b
⊢ IsSFiniteKernel (partialTraj κ a b)

Tactic:
induction b, hab using Nat.le_induction with

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a ↦ (X a, Y a)) μ)
hf_int' : Integrable (fun a ↦ f (X a, Y a)) μ
t : Set β
ht : MeasurableSet t
a✝ : μ (X ⁻¹' t) < ∞
⊢ ∫ (y : β), ∫ (y_1 : Ω), f (y, y_1) ∂(condDistrib Y X μ) y ∂Measure.map X (μ.restrict (X ⁻¹' t)) =
    ∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ

pp: case refine_2
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a ↦ (X a, Y a)) μ)
hf_int' : Integrable (fun a ↦ f (X a, Y a)) μ
t : Set β
ht : MeasurableSet t
a✝ : μ (X ⁻¹' t) < ∞
⊢ AEStronglyMeasurable (fun x' ↦ ∫ (y : Ω), f (x', y) ∂(condDistrib Y X μ) x') (Measure.map X (μ.restrict (X ⁻¹' t)))

Tactic:
swap

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a ↦ (X a, Y a)) μ)
hf_int' : Integrable (fun a ↦ f (X a, Y a)) μ
t : Set β
ht : MeasurableSet t
a✝ : μ (X ⁻¹' t) < ∞
⊢ AEStronglyMeasurable (fun x' ↦ ∫ (y : Ω), f (x', y) ∂(condDistrib Y X μ) x') (Measure.map X (μ.restrict (X ⁻¹' t)))

case refine_2
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a ↦ (X a, Y a)) μ)
hf_int' : Integrable (fun a ↦ f (X a, Y a)) μ
t : Set β
ht : MeasurableSet t
a✝ : μ (X ⁻¹' t) < ∞
⊢ ∫ (y : β), ∫ (y_1 : Ω), f (y, y_1) ∂(condDistrib Y X μ) y ∂Measure.map X (μ.restrict (X ⁻¹' t)) =
    ∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inl
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a✝ b✝ c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsFiniteKernel (κ n)
a b : ℕ
hab : a ≤ b
⊢ IsFiniteKernel (partialTraj κ a b)

Tactic:
induction b, hab using Nat.le_induction with

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

Goal state before:
pp: case inl
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a✝ b✝ c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsZeroOrMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
⊢ IsZeroOrMarkovKernel (partialTraj κ a b)

Tactic:
induction b, hab using Nat.le_induction with

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

Goal state before:
pp: case inl
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a✝ b✝ c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
⊢ IsMarkovKernel (partialTraj κ a b)

Tactic:
induction b, hab using Nat.le_induction with

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
this✝ : {x | ¬κ.densityProcess κ.fst n a x univ = 1} ⊆ {x | (κ.fst a) (countablePartitionSet n x) = 0}
this : {x | (κ.fst a) (countablePartitionSet n x) = 0} ⊆ ⋃ u ∈ countablePartition γ n, ⋃ (_ : (κ.fst a) u = 0), u
s : Set γ
hs : s ∈ countablePartition γ n
h : ¬(κ.fst a) s = 0
⊢ MeasurableSet (⋃ (_ : (κ.fst a) s = 0), s)

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
h0 : (κ a) {p | p.1 ∈ countablePartitionSet n x} = 0
⊢ Tendsto (fun m ↦ (κ a) (countablePartitionSet n x ×ˢ seq m) / (κ a) {p | p.1 ∈ countablePartitionSet n x}) atTop
    (𝓝 ((κ a) (countablePartitionSet n x ×ˢ univ) / (κ a) {p | p.1 ∈ countablePartitionSet n x}))

Tactic:
suffices ∀ m, κ a (countablePartitionSet n x ×ˢ seq m) = 0 by
      simp only [this, h0, ENNReal.zero_div, tendsto_const_nhds_iff]
      suffices κ a (countablePartitionSet n x ×ˢ univ) = 0 by
        simp only [this, ENNReal.zero_div]
      convert! h0
      ext x
      simp only [mem_prod, mem_univ, and_true, mem_ofPred_eq]

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
h0 : (κ a) {p | p.1 ∈ countablePartitionSet n x} = 0
⊢ ∀ (m : ℕ), (κ a) (countablePartitionSet n x ×ˢ seq m) = 0
Module: Mathlib.Probability.Distributions.SetBernoulli

Goal state before:
pp: case neg
ι : Type u_1
p : ↑I
inst✝ : Countable ι
s : Set (Set ι)
hs : MeasurableSet s
h : ∅ ∉ s
⊢ setBer(∅, p) {s_1 | s_1 ∈ s ∧ s_1 ⊆ ∅} = (dirac ∅) s

Tactic:
· have : {t | t ∈ s ∧ t ⊆ ∅} = ∅ := by grind
    rw [this]
    simp_all

Goal state after:
Module: Mathlib.Probability.CondVar

Goal state before:
pp: case inl
Ω : Type u_1
m₀ : MeasurableSpace Ω
X : Ω → ℝ
⊢ Var[X; 0 | ⊥] =ᵐ[0] fun x ↦ ⨍ (ω : Ω), (X ω - ⨍ (ω' : Ω), X ω' ∂0) ^ 2 ∂0

Tactic:
rw [ae_zero]

Goal state after:
case inl
Ω : Type u_1
m₀ : MeasurableSpace Ω
X : Ω → ℝ
⊢ Var[X; 0 | ⊥] =ᶠ[⊥] fun x ↦ ⨍ (ω : Ω), (X ω - ⨍ (ω' : Ω), X ω' ∂0) ^ 2 ∂0
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
hfg : ∀ (a : α), g a ≤ᵐ[κ a] f a
⊢ κ.withDensity ((fun a x ↦ f a x - g a x) + g) = κ.withDensity f

pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
hfg : ∀ (a : α), g a ≤ᵐ[κ a] f a
⊢ Measurable (Function.uncurry fun a x ↦ f a x - g a x)

Tactic:
swap

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
hfg : ∀ (a : α), g a ≤ᵐ[κ a] f a
⊢ Measurable (Function.uncurry fun a x ↦ f a x - g a x)

α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
hfg : ∀ (a : α), g a ≤ᵐ[κ a] f a
⊢ κ.withDensity ((fun a x ↦ f a x - g a x) + g) = κ.withDensity f