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

Goal state before:
pp: case inl.succ
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 k : ℕ
hak : a ≤ k
a✝ : IsFiniteKernel (partialTraj κ a k)
⊢ IsFiniteKernel ((Kernel.id ×ₖ (κ k).map ⇑(piSingleton k) ∘ₖ partialTraj κ a k).map (_root_.IicProdIoc k (k + 1)))

Tactic:
]

Goal state after:
case inl.succ
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 k : ℕ
hak : a ≤ k
a✝ : IsFiniteKernel (partialTraj κ a k)
⊢ IsFiniteKernel ((Kernel.id ×ₖ (κ k).map ⇑(piSingleton k) ∘ₖ partialTraj κ a k).map (_root_.IicProdIoc k (k + 1)))
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 : ℕ), IsFiniteKernel (κ n)
a b : ℕ
hba : b ≤ a
⊢ IsFiniteKernel (deterministic (frestrictLe₂ hba) ⋯)

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 : ℕ), IsFiniteKernel (κ n)
a b : ℕ
hba : b ≤ a
⊢ IsFiniteKernel (deterministic (frestrictLe₂ hba) ⋯)
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inl.base
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 : ℕ
⊢ IsZeroOrMarkovKernel Kernel.id

Tactic:
]

Goal state after:
case inl.base
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 : ℕ
⊢ IsZeroOrMarkovKernel Kernel.id
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 α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ ∀ᵐ (x : γ) ∂ν a, Tendsto (fun m ↦ κ.density ν a x (seq m)) atTop (𝓝 0)

Tactic:
refine tendsto_of_integral_tendsto_of_antitone ?_ (integrable_const _) ?_ ?_ ?_
  · exact fun m ↦ integrable_density hκν _ (hseq_meas m)
  · rw [integral_zero]
    exact tendsto_integral_density_of_antitone hκν a seq hseq hseq_iInter hseq_meas
  · exact ae_of_all _ (fun c n m hnm ↦ density_mono_set hκν a c (hseq hnm))
  · exact ae_of_all _ (fun x m ↦ density_nonneg hκν a x (seq m))

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

Goal state before:
pp: case inl.succ
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 k : ℕ
hak : a ≤ k
a✝ : IsZeroOrMarkovKernel (partialTraj κ a k)
⊢ IsZeroOrMarkovKernel
    ((Kernel.id ×ₖ (κ k).map ⇑(piSingleton k) ∘ₖ partialTraj κ a k).map (_root_.IicProdIoc k (k + 1)))

Tactic:
]

Goal state after:
case inl.succ
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 k : ℕ
hak : a ≤ k
a✝ : IsZeroOrMarkovKernel (partialTraj κ a k)
⊢ IsZeroOrMarkovKernel
    ((Kernel.id ×ₖ (κ k).map ⇑(piSingleton k) ∘ₖ partialTraj κ a k).map (_root_.IicProdIoc k (k + 1)))
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 : α
x : γ
⊢ ((κ a) (countablePartitionSet n x ×ˢ univ) / (κ.fst a) (countablePartitionSet n x)).toReal =
    if (κ.fst a) (countablePartitionSet n x) = 0 then 0 else 1

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 : α
x : γ
⊢ ((κ a) (countablePartitionSet n x ×ˢ univ) / (κ.fst a) (countablePartitionSet n x)).toReal =
    if (κ.fst a) (countablePartitionSet n x) = 0 then 0 else 1
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 : ℕ), IsZeroOrMarkovKernel (κ n)
a b : ℕ
hba : b ≤ a
⊢ IsZeroOrMarkovKernel (deterministic (frestrictLe₂ hba) ⋯)

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 : ℕ), IsZeroOrMarkovKernel (κ n)
a b : ℕ
hba : b ≤ a
⊢ IsZeroOrMarkovKernel (deterministic (frestrictLe₂ hba) ⋯)
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inl.base
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 : ℕ
⊢ IsMarkovKernel Kernel.id

Tactic:
]

Goal state after:
case inl.base
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 : ℕ
⊢ IsMarkovKernel Kernel.id
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) < ∞
⊢ ∫ (x : α) in X ⁻¹' t, f (X x, Y x) ∂μ = ∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ

Tactic:
]

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

Goal state before:
pp: case inl.succ
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 k : ℕ
hak : a ≤ k
a✝ : IsMarkovKernel (partialTraj κ a k)
⊢ IsMarkovKernel ((Kernel.id ×ₖ (κ k).map ⇑(piSingleton k) ∘ₖ partialTraj κ a k).map (_root_.IicProdIoc k (k + 1)))

Tactic:
]

Goal state after:
case inl.succ
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 k : ℕ
hak : a ≤ k
a✝ : IsMarkovKernel (partialTraj κ a k)
⊢ IsMarkovKernel ((Kernel.id ×ₖ (κ k).map ⇑(piSingleton k) ∘ₖ partialTraj κ a k).map (_root_.IicProdIoc k (k + 1)))
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: α : 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 : AEStronglyMeasurable f (Measure.map (fun a ↦ (X a, Y a)) μ)
hf_int : Integrable (fun a ↦ f (X a, Y a)) μ
⊢ Integrable (f ∘ fun a ↦ (X a, Y a)) μ

Tactic:
]

Goal state after:
α : 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 : AEStronglyMeasurable f (Measure.map (fun a ↦ (X a, Y a)) μ)
hf_int : Integrable (fun a ↦ f (X a, Y a)) μ
⊢ Integrable (f ∘ fun a ↦ (X a, Y a)) μ
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
⊢ ((κ a) (countablePartitionSet n x ×ˢ univ) / (κ a) {p | p.1 ∈ countablePartitionSet n x}).toReal = 1

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
⊢ ((κ a) (countablePartitionSet n x ×ˢ univ) / (κ a) {p | p.1 ∈ countablePartitionSet n x}).toReal = 1
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: α : 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 : StronglyMeasurable f
hf_int : Integrable (fun a ↦ f (X a, Y a)) μ
⊢ Integrable (f ∘ fun x ↦ (X x, Y x)) μ

Tactic:
]

Goal state after:
α : 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 : StronglyMeasurable f
hf_int : Integrable (fun a ↦ f (X a, Y a)) μ
⊢ Integrable (f ∘ fun x ↦ (X x, Y x)) μ
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: β : 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
⊢ (Measure.map (fun ω ↦ (X ω, ω)) μ) (Prod.snd ⁻¹' s) = 0

Tactic:
]

Goal state after:
β : 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
⊢ (Measure.map (fun ω ↦ (X ω, ω)) μ) (Prod.snd ⁻¹' s) = 0
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 (deterministic (frestrictLe₂ hba) ⋯)

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 (deterministic (frestrictLe₂ hba) ⋯)
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

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

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

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 ω, ω)) μ

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.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 : ¬(κ a) {p | p.1 ∈ countablePartitionSet n x} = 0
this : countablePartitionSet n x ×ˢ univ = {p | p.1 ∈ countablePartitionSet n x}
⊢ (κ a) {p | p.1 ∈ countablePartitionSet n x} ≠ 0

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 : ¬(κ a) {p | p.1 ∈ 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.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 μ
⊢ μ 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 μ
⊢ μ s = 0
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 : α
⊢ (κ.fst a) {a_1 | ¬κ.densityProcess κ.fst n a a_1 univ = 1} = 0

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 : α
⊢ (κ.fst a) {a_1 | ¬κ.densityProcess κ.fst n a a_1 univ = 1} = 0
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
a : ℕ
⊢ (Kernel.id ×ₖ (κ a).map ⇑(piSingleton a)).map (_root_.IicProdIoc a (a + 1)) =
    (Kernel.id ×ₖ (κ a).map ⇑(piSingleton a)).map (_root_.IicProdIoc a (a + 1))

Tactic:
]

Goal state after:
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 : α
x : γ
hx : ¬(if (κ.fst a) (countablePartitionSet n x) = 0 then 0 else 1) = 1
⊢ (κ.fst a) (countablePartitionSet n x) = 0

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 : α
x : γ
hx : ¬(if (κ.fst a) (countablePartitionSet n x) = 0 then 0 else 1) = 1
⊢ (κ.fst a) (countablePartitionSet n x) = 0
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
⊢ (Kernel.id ×ₖ (κ b).map ⇑(piSingleton b) ∘ₖ partialTraj κ a b).map (_root_.IicProdIoc b (b + 1)) =
    (Kernel.id ×ₖ (κ b).map ⇑(piSingleton b) ∘ₖ partialTraj κ a b).map (_root_.IicProdIoc b (b + 1))

Tactic:
]

Goal state after:
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

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.IonescuTulcea.PartialTraj

Goal state before:
pp: case succ
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
hab : a ≤ b
k : ℕ
h : b ≤ k
hk : partialTraj κ b k ∘ₖ partialTraj κ a b = partialTraj κ a k
⊢ partialTraj κ a (k + 1) = partialTraj κ a (k + 1)

Tactic:
]

Goal state after:
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 μ
hf : AEStronglyMeasurable (fun x ↦ f x.2) (Measure.map (fun ω ↦ (X ω, ω)) μ)
⊢ ∫⁻ (a : Ω), ‖f (X a, a).2‖ₑ ∂μ < ∞

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 μ
hf : AEStronglyMeasurable (fun x ↦ f x.2) (Measure.map (fun ω ↦ (X ω, ω)) μ)
⊢ ∫⁻ (a : Ω), ‖f (X a, a).2‖ₑ ∂μ < ∞
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

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 ω, ω)) μ