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

Goal state before:
pp: case inr
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 : ℕ
hba : b ≤ a
⊢ IsMarkovKernel (partialTraj κ a b)

Tactic:
·

Goal state after:
case inr
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 : ℕ
hba : b ≤ a
⊢ IsMarkovKernel (partialTraj κ a b)
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: case pos
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : μ s = 0
hX : AEMeasurable X μ
⊢ (Measure.map (fun ω ↦ (X ω, ω)) μ) (Prod.snd ⁻¹' s) = 0

pp: case neg
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : μ s = 0
hX : ¬AEMeasurable X μ
⊢ (Measure.map (fun ω ↦ (X ω, ω)) μ) (Prod.snd ⁻¹' s) = 0

Tactic:
·

Goal state after:
case pos
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : μ s = 0
hX : AEMeasurable X μ
⊢ (Measure.map (fun ω ↦ (X ω, ω)) μ) (Prod.snd ⁻¹' s) = 0
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 : α
x : γ
h : ¬(κ.fst a) (countablePartitionSet n x) = 0
this : countablePartitionSet n x ×ˢ univ = {p | p.1 ∈ countablePartitionSet n x}
⊢ ENNReal.toReal 1 = 1

pp: case neg.h0
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
h : ¬(κ.fst a) (countablePartitionSet n x) = 0
this : countablePartitionSet n x ×ˢ univ = {p | p.1 ∈ countablePartitionSet n x}
⊢ (κ a) {p | p.1 ∈ countablePartitionSet n x} ≠ 0

pp: case neg.hI
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
h : ¬(κ.fst a) (countablePartitionSet n x) = 0
this : countablePartitionSet n x ×ˢ univ = {p | p.1 ∈ countablePartitionSet n x}
⊢ (κ a) {p | p.1 ∈ countablePartitionSet n x} ≠ ∞

Tactic:
·

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
h : ¬(κ.fst a) (countablePartitionSet n x) = 0
this : countablePartitionSet n x ×ˢ univ = {p | p.1 ∈ countablePartitionSet n x}
⊢ ENNReal.toReal 1 = 1
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: case pos
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : μ s = 0
hX : AEMeasurable X μ
⊢ μ ((fun ω ↦ (X ω, ω)) ⁻¹' Prod.snd ⁻¹' s) = 0

pp: case pos.hf
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : μ s = 0
hX : AEMeasurable X μ
⊢ AEMeasurable (fun ω ↦ (X ω, ω)) μ

pp: case pos.hs
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : μ s = 0
hX : AEMeasurable X μ
⊢ MeasurableSet (Prod.snd ⁻¹' s)

Tactic:
·

Goal state after:
case pos
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : μ s = 0
hX : AEMeasurable X μ
⊢ μ ((fun ω ↦ (X ω, ω)) ⁻¹' Prod.snd ⁻¹' s) = 0
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case neg.h0
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
h : ¬(κ.fst a) (countablePartitionSet n x) = 0
this : countablePartitionSet n x ×ˢ univ = {p | p.1 ∈ countablePartitionSet n x}
⊢ (κ a) {p | p.1 ∈ countablePartitionSet n x} ≠ 0

pp: case neg.hI
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
h : ¬(κ.fst a) (countablePartitionSet n x) = 0
this : countablePartitionSet n x ×ˢ univ = {p | p.1 ∈ countablePartitionSet n x}
⊢ (κ a) {p | p.1 ∈ countablePartitionSet n x} ≠ ∞

Tactic:
·

Goal state after:
case neg.h0
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
h : ¬(κ.fst a) (countablePartitionSet n x) = 0
this : countablePartitionSet n x ×ˢ univ = {p | p.1 ∈ countablePartitionSet n x}
⊢ (κ a) {p | p.1 ∈ countablePartitionSet n x} ≠ 0
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case neg.hI
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
h : ¬(κ.fst a) (countablePartitionSet n x) = 0
this : countablePartitionSet n x ×ˢ univ = {p | p.1 ∈ countablePartitionSet n x}
⊢ (κ a) {p | p.1 ∈ countablePartitionSet n x} ≠ ∞

Tactic:
·

Goal state after:
case neg.hI
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
h : ¬(κ.fst a) (countablePartitionSet n x) = 0
this : countablePartitionSet n x ×ˢ univ = {p | p.1 ∈ countablePartitionSet n x}
⊢ (κ a) {p | p.1 ∈ countablePartitionSet n x} ≠ ∞
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: case pos.hf
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : μ s = 0
hX : AEMeasurable X μ
⊢ AEMeasurable (fun ω ↦ (X ω, ω)) μ

pp: case pos.hs
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : μ s = 0
hX : AEMeasurable X μ
⊢ MeasurableSet (Prod.snd ⁻¹' s)

Tactic:
·

Goal state after:
case pos.hf
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : μ s = 0
hX : AEMeasurable X μ
⊢ AEMeasurable (fun ω ↦ (X ω, ω)) μ
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: case pos.hs
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : μ s = 0
hX : AEMeasurable X μ
⊢ MeasurableSet (Prod.snd ⁻¹' s)

Tactic:
·

Goal state after:
case pos.hs
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : μ s = 0
hX : AEMeasurable X μ
⊢ MeasurableSet (Prod.snd ⁻¹' s)
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: case neg
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : μ s = 0
hX : ¬AEMeasurable X μ
⊢ (Measure.map (fun ω ↦ (X ω, ω)) μ) (Prod.snd ⁻¹' s) = 0

Tactic:
·

Goal state after:
case neg
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : μ s = 0
hX : ¬AEMeasurable X μ
⊢ (Measure.map (fun ω ↦ (X ω, ω)) μ) (Prod.snd ⁻¹' s) = 0
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: case neg
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : μ s = 0
hX : ¬AEMeasurable X μ
⊢ 0 (Prod.snd ⁻¹' s) = 0

pp: case neg
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : μ s = 0
hX : ¬AEMeasurable X μ
⊢ ¬AEMeasurable (fun ω ↦ (X ω, ω)) μ

Tactic:
·

Goal state after:
case neg
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : μ s = 0
hX : ¬AEMeasurable X μ
⊢ 0 (Prod.snd ⁻¹' s) = 0
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: case neg
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : μ s = 0
hX : ¬AEMeasurable X μ
⊢ ¬AEMeasurable (fun ω ↦ (X ω, ω)) μ

Tactic:
·

Goal state after:
case neg
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : μ s = 0
hX : ¬AEMeasurable X μ
⊢ ¬AEMeasurable (fun ω ↦ (X ω, ω)) μ
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: case pos
β : Type u_2
F : Type u_4
inst✝ : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
hX : AEMeasurable X μ
⊢ Integrable (fun x ↦ f x.2) (Measure.map (fun ω ↦ (X ω, ω)) μ)

pp: case neg
β : Type u_2
F : Type u_4
inst✝ : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
hX : ¬AEMeasurable X μ
⊢ Integrable (fun x ↦ f x.2) (Measure.map (fun ω ↦ (X ω, ω)) μ)

Tactic:
·

Goal state after:
case pos
β : Type u_2
F : Type u_4
inst✝ : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
hX : AEMeasurable X μ
⊢ Integrable (fun x ↦ f x.2) (Measure.map (fun ω ↦ (X ω, ω)) μ)
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: case neg
β : Type u_2
F : Type u_4
inst✝ : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
hX : ¬AEMeasurable X μ
⊢ Integrable (fun x ↦ f x.2) (Measure.map (fun ω ↦ (X ω, ω)) μ)

Tactic:
·

Goal state after:
case neg
β : Type u_2
F : Type u_4
inst✝ : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
hX : ¬AEMeasurable X μ
⊢ Integrable (fun x ↦ f x.2) (Measure.map (fun ω ↦ (X ω, ω)) μ)
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: α : 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
⊢ ∑' (p : ↑(countablePartition γ n)), (κ.fst a) (⋃ (_ : (κ.fst a) ↑p = 0), ↑p) = 0

pp: case hs
α : 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
⊢ (countablePartition γ n).Countable

pp: case hd
α : 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
⊢ (countablePartition γ n).PairwiseDisjoint fun u ↦ ⋃ (_ : (κ.fst a) u = 0), u

pp: case h
α : 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
⊢ ∀ b ∈ countablePartition γ n, MeasurableSet (⋃ (_ : (κ.fst a) b = 0), b)

Tactic:
·

Goal state after:
α : 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
⊢ ∑' (p : ↑(countablePartition γ n)), (κ.fst a) (⋃ (_ : (κ.fst a) ↑p = 0), ↑p) = 0
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: case neg
β : Type u_2
F : Type u_4
inst✝ : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
hX : ¬AEMeasurable X μ
⊢ Integrable (fun x ↦ f x.2) 0

pp: case neg
β : Type u_2
F : Type u_4
inst✝ : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
hX : ¬AEMeasurable X μ
⊢ ¬AEMeasurable (fun ω ↦ (X ω, ω)) μ

Tactic:
·

Goal state after:
case neg
β : Type u_2
F : Type u_4
inst✝ : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
hX : ¬AEMeasurable X μ
⊢ Integrable (fun x ↦ f x.2) 0
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: case neg
β : Type u_2
F : Type u_4
inst✝ : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
hX : ¬AEMeasurable X μ
⊢ ¬AEMeasurable (fun ω ↦ (X ω, ω)) μ

Tactic:
·

Goal state after:
case neg
β : Type u_2
F : Type u_4
inst✝ : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
hX : ¬AEMeasurable X μ
⊢ ¬AEMeasurable (fun ω ↦ (X ω, ω)) μ
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case hs
α : 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
⊢ (countablePartition γ n).Countable

pp: case hd
α : 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
⊢ (countablePartition γ n).PairwiseDisjoint fun u ↦ ⋃ (_ : (κ.fst a) u = 0), u

pp: case h
α : 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
⊢ ∀ b ∈ countablePartition γ n, MeasurableSet (⋃ (_ : (κ.fst a) b = 0), b)

Tactic:
·

Goal state after:
case hs
α : 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
⊢ (countablePartition γ n).Countable
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inl
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b : ℕ
hba : b ≤ a
⊢ partialTraj κ a b = (Kernel.id ×ₖ (partialTraj κ a b).map (restrict₂ ⋯)).map (_root_.IicProdIoc a b)

pp: case inr
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b : ℕ
hab : a ≤ b
⊢ partialTraj κ a b = (Kernel.id ×ₖ (partialTraj κ a b).map (restrict₂ ⋯)).map (_root_.IicProdIoc a b)

Tactic:
·

Goal state after:
case inl
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b : ℕ
hba : b ≤ a
⊢ partialTraj κ a b = (Kernel.id ×ₖ (partialTraj κ a b).map (restrict₂ ⋯)).map (_root_.IicProdIoc a b)
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case hd
α : 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
⊢ (countablePartition γ n).PairwiseDisjoint fun u ↦ ⋃ (_ : (κ.fst a) u = 0), u

pp: case h
α : 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
⊢ ∀ b ∈ countablePartition γ n, MeasurableSet (⋃ (_ : (κ.fst a) b = 0), b)

Tactic:
·

Goal state after:
case hd
α : 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
⊢ (countablePartition γ n).PairwiseDisjoint fun u ↦ ⋃ (_ : (κ.fst a) u = 0), u
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case h
α : 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
⊢ ∀ b ∈ countablePartition γ n, MeasurableSet (⋃ (_ : (κ.fst a) b = 0), b)

Tactic:
·

Goal state after:
case h
α : 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
⊢ ∀ b ∈ countablePartition γ n, MeasurableSet (⋃ (_ : (κ.fst a) b = 0), b)
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 α (γ × β)
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)

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:
·

Goal state after:
case pos
α : 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)