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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
h : IsSFiniteKernel κ
⊢ κ ∥ₖ 0 = 0

pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
h : ¬IsSFiniteKernel κ
⊢ κ ∥ₖ 0 = 0

Tactic:
·

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
h : IsSFiniteKernel κ
⊢ κ ∥ₖ 0 = 0
Module: Mathlib.Probability.Kernel.Composition.ParallelComp

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
h : ¬IsSFiniteKernel κ
⊢ κ ∥ₖ 0 = 0

Tactic:
·

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
h : ¬IsSFiniteKernel κ
⊢ κ ∥ₖ 0 = 0
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
⊢ (μ ⊗ₘ κ) s = ∫⁻ (a : α), (κ a) (Prod.mk a ⁻¹' s) ∂μ

Tactic:
compProd,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
⊢ ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ) ()) s = ∫⁻ (a : α), (κ a) (Prod.mk a ⁻¹' s) ∂μ
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : β → γ
hf : Measurable f
⊢ (Kernel.sum fun n ↦ (κ.seq n).map f) = κ.map f

pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : β → γ
hf : ¬Measurable f
⊢ (Kernel.sum fun n ↦ (κ.seq n).map f) = κ.map f

Tactic:
·

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : β → γ
hf : Measurable f
⊢ (Kernel.sum fun n ↦ (κ.seq n).map f) = κ.map f
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : ⇑κ =ᵐ[μ] ⇑η
⊢ μ ⊗ₘ κ = μ ⊗ₘ η

Tactic:
compProd,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : ⇑κ =ᵐ[μ] ⇑η
⊢ (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ) () = μ ⊗ₘ η
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : β → γ
hf : ¬Measurable f
⊢ (Kernel.sum fun n ↦ (κ.seq n).map f) = κ.map f

Tactic:
·

Goal state after:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : β → γ
hf : ¬Measurable f
⊢ (Kernel.sum fun n ↦ (κ.seq n).map f) = κ.map f
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h : μ ⊗ₘ κ = 0
⊢ ∀ᵐ (a : α) ∂μ, κ a = 0

pp: case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h : ∀ᵐ (a : α) ∂μ, κ a = 0
⊢ μ ⊗ₘ κ = 0

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h : μ ⊗ₘ κ = 0
⊢ ∀ᵐ (a : α) ∂μ, κ a = 0
Module: Mathlib.Probability.Kernel.Composition.ParallelComp

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
ι : Type u_5
inst✝¹ : Countable ι
κ : ι → Kernel α β
inst✝ : ∀ (i : ι), IsSFiniteKernel (κ i)
η : Kernel γ δ
h : ¬IsSFiniteKernel η
⊢ Kernel.sum κ ∥ₖ η = Kernel.sum fun i ↦ κ i ∥ₖ η

pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
ι : Type u_5
inst✝¹ : Countable ι
κ : ι → Kernel α β
inst✝ : ∀ (i : ι), IsSFiniteKernel (κ i)
η : Kernel γ δ
h : IsSFiniteKernel η
⊢ Kernel.sum κ ∥ₖ η = Kernel.sum fun i ↦ κ i ∥ₖ η

Tactic:
·

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
ι : Type u_5
inst✝¹ : Countable ι
κ : ι → Kernel α β
inst✝ : ∀ (i : ι), IsSFiniteKernel (κ i)
η : Kernel γ δ
h : ¬IsSFiniteKernel η
⊢ Kernel.sum κ ∥ₖ η = Kernel.sum fun i ↦ κ i ∥ₖ η
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h : ∀ᵐ (a : α) ∂μ, κ a = 0
⊢ μ ⊗ₘ κ = 0

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h : ∀ᵐ (a : α) ∂μ, κ a = 0
⊢ μ ⊗ₘ κ = 0
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
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f✝ : β → γ
g : γ → α
κ : Kernel α β
inst✝ : IsZeroOrMarkovKernel κ
f : β → γ
hf : Measurable f
⊢ IsZeroOrMarkovKernel (κ.map f)

pp: case neg
α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f✝ : β → γ
g : γ → α
κ : Kernel α β
inst✝ : IsZeroOrMarkovKernel κ
f : β → γ
hf : ¬Measurable f
⊢ IsZeroOrMarkovKernel (κ.map f)

Tactic:
·

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f✝ : β → γ
g : γ → α
κ : Kernel α β
inst✝ : IsZeroOrMarkovKernel κ
f : β → γ
hf : Measurable f
⊢ IsZeroOrMarkovKernel (κ.map f)
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: case pos.inl
α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f✝ : β → γ
g : γ → α
f : β → γ
hf : Measurable f
inst✝ : IsZeroOrMarkovKernel 0
⊢ IsZeroOrMarkovKernel (Kernel.map 0 f)

pp: case pos.inr
α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f✝ : β → γ
g : γ → α
κ : Kernel α β
inst✝ : IsZeroOrMarkovKernel κ
f : β → γ
hf : Measurable f
h : IsMarkovKernel κ
⊢ IsZeroOrMarkovKernel (κ.map f)

Tactic:
·

Goal state after:
case pos.inl
α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f✝ : β → γ
g : γ → α
f : β → γ
hf : Measurable f
inst✝ : IsZeroOrMarkovKernel 0
⊢ IsZeroOrMarkovKernel (Kernel.map 0 f)
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: case pos.inr
α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f✝ : β → γ
g : γ → α
κ : Kernel α β
inst✝ : IsZeroOrMarkovKernel κ
f : β → γ
hf : Measurable f
h : IsMarkovKernel κ
⊢ IsZeroOrMarkovKernel (κ.map f)

Tactic:
·

Goal state after:
case pos.inr
α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f✝ : β → γ
g : γ → α
κ : Kernel α β
inst✝ : IsZeroOrMarkovKernel κ
f : β → γ
hf : Measurable f
h : IsMarkovKernel κ
⊢ IsZeroOrMarkovKernel (κ.map f)
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f✝ : β → γ
g : γ → α
κ : Kernel α β
inst✝ : IsZeroOrMarkovKernel κ
f : β → γ
hf : ¬Measurable f
⊢ IsZeroOrMarkovKernel (κ.map f)

Tactic:
·

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f✝ : β → γ
g : γ → α
κ : Kernel α β
inst✝ : IsZeroOrMarkovKernel κ
f : β → γ
hf : ¬Measurable f
⊢ IsZeroOrMarkovKernel (κ.map f)
Module: Mathlib.Probability.Kernel.Composition.ParallelComp

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
ι : Type u_5
inst✝¹ : Countable ι
κ : Kernel α β
η : ι → Kernel γ δ
inst✝ : ∀ (i : ι), IsSFiniteKernel (η i)
h : ¬IsSFiniteKernel κ
⊢ κ ∥ₖ Kernel.sum η = Kernel.sum fun i ↦ κ ∥ₖ η i

pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
ι : Type u_5
inst✝¹ : Countable ι
κ : Kernel α β
η : ι → Kernel γ δ
inst✝ : ∀ (i : ι), IsSFiniteKernel (η i)
h : IsSFiniteKernel κ
⊢ κ ∥ₖ Kernel.sum η = Kernel.sum fun i ↦ κ ∥ₖ η i

Tactic:
·

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
ι : Type u_5
inst✝¹ : Countable ι
κ : Kernel α β
η : ι → Kernel γ δ
inst✝ : ∀ (i : ι), IsSFiniteKernel (η i)
h : ¬IsSFiniteKernel κ
⊢ κ ∥ₖ Kernel.sum η = Kernel.sum fun i ↦ κ ∥ₖ η i
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
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f✝ : β → γ
g : γ → α
κ : Kernel α β
inst✝ : IsFiniteKernel κ
f : β → γ
a : α
hf : Measurable f
⊢ ((κ.map f) a) Set.univ ≤ κ.bound

pp: case neg
α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f✝ : β → γ
g : γ → α
κ : Kernel α β
inst✝ : IsFiniteKernel κ
f : β → γ
a : α
hf : ¬Measurable f
⊢ ((κ.map f) a) Set.univ ≤ κ.bound

Tactic:
·

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f✝ : β → γ
g : γ → α
κ : Kernel α β
inst✝ : IsFiniteKernel κ
f : β → γ
a : α
hf : Measurable f
⊢ ((κ.map f) a) Set.univ ≤ κ.bound
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f✝ : β → γ
g : γ → α
κ : Kernel α β
inst✝ : IsFiniteKernel κ
f : β → γ
a : α
hf : ¬Measurable f
⊢ ((κ.map f) a) Set.univ ≤ κ.bound

Tactic:
·

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f✝ : β → γ
g : γ → α
κ : Kernel α β
inst✝ : IsFiniteKernel κ
f : β → γ
a : α
hf : ¬Measurable f
⊢ ((κ.map f) a) Set.univ ≤ κ.bound
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : β → γ
g : γ → α
hg : Measurable g
inst✝ : IsZeroOrMarkovKernel 0
⊢ IsZeroOrMarkovKernel (Kernel.comap 0 g hg)

pp: case inr
α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : β → γ
g : γ → α
κ : Kernel α β
inst✝ : IsZeroOrMarkovKernel κ
hg : Measurable g
h : IsMarkovKernel κ
⊢ IsZeroOrMarkovKernel (κ.comap g hg)

Tactic:
·

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : β → γ
g : γ → α
hg : Measurable g
inst✝ : IsZeroOrMarkovKernel 0
⊢ IsZeroOrMarkovKernel (Kernel.comap 0 g hg)
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 μ
inst✝ : SFinite ν
κ : Kernel α β
hκ : IsSFiniteKernel κ
⊢ (μ + ν) ⊗ₘ κ = μ ⊗ₘ κ + ν ⊗ₘ κ

pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst✝¹ : SFinite μ
inst✝ : SFinite ν
κ : Kernel α β
hκ : ¬IsSFiniteKernel κ
⊢ (μ + ν) ⊗ₘ κ = μ ⊗ₘ κ + ν ⊗ₘ κ

Tactic:
·

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst✝¹ : SFinite μ
inst✝ : SFinite ν
κ : Kernel α β
hκ : IsSFiniteKernel κ
⊢ (μ + ν) ⊗ₘ κ = μ ⊗ₘ κ + ν ⊗ₘ κ
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : β → γ
g : γ → α
κ : Kernel α β
inst✝ : IsZeroOrMarkovKernel κ
hg : Measurable g
h : IsMarkovKernel κ
⊢ IsZeroOrMarkovKernel (κ.comap g hg)

Tactic:
·

Goal state after:
case inr
α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : β → γ
g : γ → α
κ : Kernel α β
inst✝ : IsZeroOrMarkovKernel κ
hg : Measurable g
h : IsMarkovKernel κ
⊢ IsZeroOrMarkovKernel (κ.comap g hg)
Module: Mathlib.Probability.Kernel.Composition.ParallelComp

Goal state before:
pp: case h₁
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
x : α × γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α × γ
⊢ (κ a.1) Set.univ ≤ κ.bound

pp: case h₂
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
x : α × γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α × γ
⊢ (η a.2) Set.univ ≤ η.bound

Tactic:
·

Goal state after:
case h₁
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
x : α × γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α × γ
⊢ (κ a.1) Set.univ ≤ κ.bound
Module: Mathlib.Probability.Kernel.Composition.ParallelComp

Goal state before:
pp: case h₂
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
x : α × γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α × γ
⊢ (η a.2) Set.univ ≤ η.bound

Tactic:
·

Goal state after:
case h₂
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
x : α × γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α × γ
⊢ (η a.2) Set.univ ≤ η.bound
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst✝¹ : SFinite μ
inst✝ : SFinite ν
κ : Kernel α β
hκ : ¬IsSFiniteKernel κ
⊢ (μ + ν) ⊗ₘ κ = μ ⊗ₘ κ + ν ⊗ₘ κ

Tactic:
·

Goal state after:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst✝¹ : SFinite μ
inst✝ : SFinite ν
κ : Kernel α β
hκ : ¬IsSFiniteKernel κ
⊢ (μ + ν) ⊗ₘ κ = μ ⊗ₘ κ + ν ⊗ₘ κ
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
hμ : SFinite μ
⊢ μ ⊗ₘ (κ + η) = μ ⊗ₘ κ + μ ⊗ₘ η

pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
hμ : ¬SFinite μ
⊢ μ ⊗ₘ (κ + η) = μ ⊗ₘ κ + μ ⊗ₘ η

Tactic:
·

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
hμ : SFinite μ
⊢ μ ⊗ₘ (κ + η) = μ ⊗ₘ κ + μ ⊗ₘ η
Module: Mathlib.Probability.Kernel.Composition.ParallelComp

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
x : α × γ
h : ¬IsSFiniteKernel κ
⊢ IsSFiniteKernel (κ ∥ₖ η)

pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
x : α × γ
h : IsSFiniteKernel κ
⊢ IsSFiniteKernel (κ ∥ₖ η)

Tactic:
·

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
x : α × γ
h : ¬IsSFiniteKernel κ
⊢ IsSFiniteKernel (κ ∥ₖ η)
Module: Mathlib.Probability.Kernel.Composition.ParallelComp

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
x : α × γ
h✝ : IsSFiniteKernel κ
h : ¬IsSFiniteKernel η
⊢ IsSFiniteKernel (κ ∥ₖ η)

pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
x : α × γ
h✝ : IsSFiniteKernel κ
h : IsSFiniteKernel η
⊢ IsSFiniteKernel (κ ∥ₖ η)

Tactic:
·

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
x : α × γ
h✝ : IsSFiniteKernel κ
h : ¬IsSFiniteKernel η
⊢ IsSFiniteKernel (κ ∥ₖ η)
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
hμ : ¬SFinite μ
⊢ μ ⊗ₘ (κ + η) = μ ⊗ₘ κ + μ ⊗ₘ η

Tactic:
·

Goal state after:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
hμ : ¬SFinite μ
⊢ μ ⊗ₘ (κ + η) = μ ⊗ₘ κ + μ ⊗ₘ η
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
ι : Type u_3
inst✝¹ : Countable ι
μ : ι → Measure α
inst✝ : ∀ (i : ι), SFinite (μ i)
⊢ sum μ ⊗ₘ κ = sum fun i ↦ μ i ⊗ₘ κ

Tactic:
compProd,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
ι : Type u_3
inst✝¹ : Countable ι
μ : ι → Measure α
inst✝ : ∀ (i : ι), SFinite (μ i)
⊢ (Kernel.const Unit (sum μ) ⊗ₖ Kernel.prodMkLeft Unit κ) () = sum fun i ↦ μ i ⊗ₘ κ
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
ι : Type u_3
inst✝ : Countable ι
κ : ι → Kernel α β
h : ∀ (i : ι), IsSFiniteKernel (κ i)
⊢ μ ⊗ₘ Kernel.sum κ = sum fun i ↦ μ ⊗ₘ κ i

Tactic:
compProd,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
ι : Type u_3
inst✝ : Countable ι
κ : ι → Kernel α β
h : ∀ (i : ι), IsSFiniteKernel (κ i)
⊢ (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit (Kernel.sum κ)) () = sum fun i ↦ μ ⊗ₘ κ i
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst✝¹ : SFinite μ
κ : Kernel α β
inst✝ : IsMarkovKernel κ
s : Set α
a✝ : MeasurableSet s
⊢ (μ ⊗ₘ κ).fst s = μ s

Tactic:
compProd,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst✝¹ : SFinite μ
κ : Kernel α β
inst✝ : IsMarkovKernel κ
s : Set α
a✝ : MeasurableSet s
⊢ ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ) ()).fst s = μ s
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 (Kernel.prodMkRight γ κ)

Tactic:
by rw [Kernel.prodMkRight]; infer_instance

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✝ : IsZeroOrMarkovKernel κ
⊢ IsZeroOrMarkovKernel (Kernel.prodMkRight γ κ)

Tactic:
by rw [Kernel.prodMkRight]; infer_instance

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✝ : IsFiniteKernel κ
⊢ IsFiniteKernel (Kernel.prodMkRight γ κ)

Tactic:
by rw [Kernel.prodMkRight]; infer_instance

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
f : α × β → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (x : α × β), f x ∂μ ⊗ₘ κ = ∫⁻ (a : α), ∫⁻ (b : β), f (a, b) ∂κ a ∂μ

Tactic:
compProd,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
f : α × β → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (x : α × β), f x ∂(Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ) () = ∫⁻ (a : α), ∫⁻ (b : β), f (a, b) ∂κ a ∂μ