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

Goal state before:
pp: β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
inst✝ : SFinite μ
⊢ map (Prod.mk ()) μ = map (Prod.mk ()) μ

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsMarkovKernel κ
⊢ IsMarkovKernel (κ.map Prod.swap)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsMarkovKernel κ
⊢ IsMarkovKernel (κ.map Prod.swap)
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsZeroOrMarkovKernel κ
⊢ IsZeroOrMarkovKernel (κ.map Prod.swap)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsZeroOrMarkovKernel κ
⊢ IsZeroOrMarkovKernel (κ.map Prod.swap)
Module: Mathlib.Probability.Kernel.Composition.CompMap

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel β γ
f : γ → δ
hf : Measurable f
a : α
s : Set δ
hs : MeasurableSet s
⊢ ∫⁻ (b : β), (η b) (f ⁻¹' s) ∂κ a = ∫⁻ (b : β), ((η.map f) b) s ∂κ a

pp: case pos.hs
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel β γ
f : γ → δ
hf : Measurable f
a : α
s : Set δ
hs : MeasurableSet s
⊢ MeasurableSet (f ⁻¹' s)

Tactic:
]

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel β γ
f : γ → δ
hf : Measurable f
a : α
s : Set δ
hs : MeasurableSet s
⊢ ∫⁻ (b : β), (η b) (f ⁻¹' s) ∂κ a = ∫⁻ (b : β), ((η.map f) b) s ∂κ a

case pos.hs
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel β γ
f : γ → δ
hf : Measurable f
a : α
s : Set δ
hs : MeasurableSet s
⊢ MeasurableSet (f ⁻¹' s)
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
⊢ SFinite ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ) ())

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
⊢ SFinite ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ) ())
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsFiniteKernel κ
⊢ IsFiniteKernel (κ.map Prod.swap)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsFiniteKernel κ
⊢ IsFiniteKernel (κ.map Prod.swap)
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteKernel κ
⊢ IsFiniteMeasure ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ) ())

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteKernel κ
⊢ IsFiniteMeasure ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ) ())
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsSFiniteKernel κ
⊢ IsSFiniteKernel (κ.map Prod.swap)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsSFiniteKernel κ
⊢ IsSFiniteKernel (κ.map Prod.swap)
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
s : Set β
hs : MeasurableSet s
⊢ (κ a) (Prod.fst ⁻¹' s) = (κ a) {p | p.1 ∈ s}

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
s : Set β
hs : MeasurableSet s
⊢ (κ a) (Prod.fst ⁻¹' s) = (κ a) {p | p.1 ∈ s}
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsMarkovKernel κ
⊢ IsProbabilityMeasure ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ) ())

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsMarkovKernel κ
⊢ IsProbabilityMeasure ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ) ())
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : IsZeroOrProbabilityMeasure μ
inst✝ : IsZeroOrMarkovKernel κ
⊢ IsZeroOrProbabilityMeasure ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ) ())

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : IsZeroOrProbabilityMeasure μ
inst✝ : IsZeroOrMarkovKernel κ
⊢ IsZeroOrProbabilityMeasure ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ) ())
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
⊢ ∫⁻ (y : β),
      ((swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ (Kernel.id ∥ₖ copy β))
          ((a, a).1, y))
        s ∂κ (a, a).2 =
    ∫⁻ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ∂κ a

pp: case hf
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
⊢ Measurable fun x ↦
    ∫⁻ (y : β),
      ((swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ (Kernel.id ∥ₖ copy β))
          (x, y))
        s ∂κ (a, a).2

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
⊢ ∫⁻ (y : β),
      ((swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ (Kernel.id ∥ₖ copy β))
          ((a, a).1, y))
        s ∂κ (a, a).2 =
    ∫⁻ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ∂κ a

case hf
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
⊢ Measurable fun x ↦
    ∫⁻ (y : β),
      ((swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ (Kernel.id ∥ₖ copy β))
          (x, y))
        s ∂κ (a, a).2
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
g : β → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (a : β × γ), g a.1 ∂κ a = ∫⁻ (bc : β × γ), g bc.1 ∂κ a

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsMarkovKernel κ
⊢ IsMarkovKernel (κ.map Prod.fst)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsMarkovKernel κ
⊢ IsMarkovKernel (κ.map Prod.fst)
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsZeroOrMarkovKernel κ
⊢ IsZeroOrMarkovKernel (κ.map Prod.fst)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsZeroOrMarkovKernel κ
⊢ IsZeroOrMarkovKernel (κ.map Prod.fst)
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsFiniteKernel κ
⊢ IsFiniteKernel (κ.map Prod.fst)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsFiniteKernel κ
⊢ IsFiniteKernel (κ.map Prod.fst)
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsSFiniteKernel κ
⊢ IsSFiniteKernel (κ.map Prod.fst)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsSFiniteKernel κ
⊢ IsSFiniteKernel (κ.map Prod.fst)
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
h : IsFiniteKernel κ.fst
a : α
⊢ (κ a) Set.univ ≤ (κ a) {p | p.1 ∈ Set.univ}

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
h : IsFiniteKernel κ.fst
a : α
⊢ (κ a) Set.univ ≤ (κ a) {p | p.1 ∈ Set.univ}
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hg : Measurable g
hf : Measurable f
x : α
s : Set γ
hs : MeasurableSet s
⊢ (κ x) ((fun x ↦ (f x, g x)) ⁻¹' {p | p.1 ∈ s}) = (κ x) (f ⁻¹' s)

pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hg : Measurable g
hf : Measurable f
x : α
s : Set γ
hs : MeasurableSet s
⊢ MeasurableSet {p | p.1 ∈ s}

Tactic:
]

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hg : Measurable g
hf : Measurable f
x : α
s : Set γ
hs : MeasurableSet s
⊢ (κ x) ((fun x ↦ (f x, g x)) ⁻¹' {p | p.1 ∈ s}) = (κ x) (f ⁻¹' s)

case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hg : Measurable g
hf : Measurable f
x : α
s : Set γ
hs : MeasurableSet s
⊢ MeasurableSet {p | p.1 ∈ s}
Module: Mathlib.Probability.Kernel.Composition.CompMap

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
f : β → γ
hf : Measurable f
x : α
s : Set δ
ms : MeasurableSet s
⊢ ∫⁻ (a : β), (η (f a)) s ∂κ x = ∫⁻ (b : β), ((η.comap f hf) b) s ∂κ x

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
f : β → γ
hf : Measurable f
x : α
s : Set δ
ms : MeasurableSet s
⊢ ∫⁻ (a : β), (η (f a)) s ∂κ x = ∫⁻ (b : β), ((η.comap f hf) b) s ∂κ x
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
f : β → γ
hf : Measurable f
⊢ κ = κ

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
s : Set γ
hs : MeasurableSet s
⊢ (κ a) (Prod.snd ⁻¹' s) = (κ a) (Prod.snd ⁻¹' s)

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
g : γ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (a : β × γ), g a.2 ∂κ a = ∫⁻ (bc : β × γ), g bc.2 ∂κ a

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsMarkovKernel κ
⊢ IsMarkovKernel (κ.map Prod.snd)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsMarkovKernel κ
⊢ IsMarkovKernel (κ.map Prod.snd)
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsZeroOrMarkovKernel κ
⊢ IsZeroOrMarkovKernel (κ.map Prod.snd)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsZeroOrMarkovKernel κ
⊢ IsZeroOrMarkovKernel (κ.map Prod.snd)
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsFiniteKernel κ
⊢ IsFiniteKernel (κ.map Prod.snd)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsFiniteKernel κ
⊢ IsFiniteKernel (κ.map Prod.snd)
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsSFiniteKernel κ
⊢ IsSFiniteKernel (κ.map Prod.snd)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst✝ : IsSFiniteKernel κ
⊢ IsSFiniteKernel (κ.map Prod.snd)
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
h : IsFiniteKernel κ.snd
a : α
⊢ (κ a) Set.univ ≤ (κ a) (Prod.snd ⁻¹' Set.univ)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
h : IsFiniteKernel κ.snd
a : α
⊢ (κ a) Set.univ ≤ (κ a) (Prod.snd ⁻¹' Set.univ)
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set ((α × β) × γ)
hs : MeasurableSet s
⊢ ∫⁻ (a : α), ((κ ⊗ₖ η) a) (Prod.mk a ⁻¹' ⇑MeasurableEquiv.prodAssoc.symm ⁻¹' s) ∂μ =
    ∫⁻ (a : α), ∫⁻ (b : β), (η (a, b)) (Prod.mk (a, b) ⁻¹' s) ∂κ a ∂μ

pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set ((α × β) × γ)
hs : MeasurableSet s
⊢ Measurable fun a ↦ (η a) (Prod.mk a ⁻¹' s)

Tactic:
]

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set ((α × β) × γ)
hs : MeasurableSet s
⊢ ∫⁻ (a : α), ((κ ⊗ₖ η) a) (Prod.mk a ⁻¹' ⇑MeasurableEquiv.prodAssoc.symm ⁻¹' s) ∂μ =
    ∫⁻ (a : α), ∫⁻ (b : β), (η (a, b)) (Prod.mk (a, b) ⁻¹' s) ∂κ a ∂μ

case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set ((α × β) × γ)
hs : MeasurableSet s
⊢ Measurable fun a ↦ (η a) (Prod.mk a ⁻¹' s)
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hf : Measurable f
hg : Measurable g
x : α
s : Set δ
hs : MeasurableSet s
⊢ (κ x) ((fun x ↦ (f x, g x)) ⁻¹' Prod.snd ⁻¹' s) = (κ x) (g ⁻¹' s)

pp: case pos.hs
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hf : Measurable f
hg : Measurable g
x : α
s : Set δ
hs : MeasurableSet s
⊢ MeasurableSet (Prod.snd ⁻¹' s)

Tactic:
]

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hf : Measurable f
hg : Measurable g
x : α
s : Set δ
hs : MeasurableSet s
⊢ (κ x) ((fun x ↦ (f x, g x)) ⁻¹' Prod.snd ⁻¹' s) = (κ x) (g ⁻¹' s)

case pos.hs
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hf : Measurable f
hg : Measurable g
x : α
s : Set δ
hs : MeasurableSet s
⊢ MeasurableSet (Prod.snd ⁻¹' s)
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: case pos.e_f
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set ((α × β) × γ)
hs : MeasurableSet s
a : α
⊢ ∫⁻ (b : β), (η (a, b)) (Prod.mk b ⁻¹' Prod.mk a ⁻¹' ⇑MeasurableEquiv.prodAssoc.symm ⁻¹' s) ∂κ a =
    ∫⁻ (b : β), (η (a, b)) (Prod.mk (a, b) ⁻¹' s) ∂κ a

pp: case pos.e_f.hs
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set ((α × β) × γ)
hs : MeasurableSet s
a : α
⊢ MeasurableSet (Prod.mk a ⁻¹' ⇑MeasurableEquiv.prodAssoc.symm ⁻¹' s)

Tactic:
]

Goal state after:
case pos.e_f
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set ((α × β) × γ)
hs : MeasurableSet s
a : α
⊢ ∫⁻ (b : β), (η (a, b)) (Prod.mk b ⁻¹' Prod.mk a ⁻¹' ⇑MeasurableEquiv.prodAssoc.symm ⁻¹' s) ∂κ a =
    ∫⁻ (b : β), (η (a, b)) (Prod.mk (a, b) ⁻¹' s) ∂κ a

case pos.e_f.hs
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set ((α × β) × γ)
hs : MeasurableSet s
a : α
⊢ MeasurableSet (Prod.mk a ⁻¹' ⇑MeasurableEquiv.prodAssoc.symm ⁻¹' s)
Module: Mathlib.Probability.Kernel.Composition.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel α γ
inst✝ : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ∫⁻ (b : β), (η a) (Prod.mk b ⁻¹' s) ∂κ a = ∫⁻ (x : β), (η a) (Prod.mk x ⁻¹' s) ∂κ a

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
κ : Kernel α β
hκ : IsSFiniteKernel κ
this : SFinite μ
s : Set (α × β)
hs : MeasurableSet s
hs_zero : (fun a ↦ (κ a) (Prod.mk a ⁻¹' s)) =ᵐ[ν] 0
⊢ (fun a ↦ (κ a) (Prod.mk a ⁻¹' s)) =ᵐ[μ] 0

Tactic:
]

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
κ : Kernel α β
hκ : IsSFiniteKernel κ
this : SFinite μ
s : Set (α × β)
hs : MeasurableSet s
hs_zero : (fun a ↦ (κ a) (Prod.mk a ⁻¹' s)) =ᵐ[ν] 0
⊢ (fun a ↦ (κ a) (Prod.mk a ⁻¹' s)) =ᵐ[μ] 0
Module: Mathlib.Probability.Kernel.Composition.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
s : Set β
t : Set γ
a : α
⊢ (κ a) s * (η a) t = (κ a) s * (η a) t

Tactic:
]

Goal state after: