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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ✝ : Kernel α β
η✝ : Kernel γ δ
x : α × γ
κ : Kernel α β
η : Kernel γ δ
h : IsSFiniteKernel κ ∧ IsSFiniteKernel η
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set (β × δ)
hs : MeasurableSet s
this :
  (fun y ↦ ((prodMkLeft α η) y.1) (Prod.mk y.2 ⁻¹' s)) = fun y ↦
    ((prodMkRight β (prodMkLeft α η)) y) (Prod.mk y.2 ⁻¹' s)
⊢ Measurable fun y ↦ ((prodMkLeft α η) y.1) (Prod.mk y.2 ⁻¹' s)

Tactic:
this

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ✝ : Kernel α β
η✝ : Kernel γ δ
x : α × γ
κ : Kernel α β
η : Kernel γ δ
h : IsSFiniteKernel κ ∧ IsSFiniteKernel η
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set (β × δ)
hs : MeasurableSet s
this :
  (fun y ↦ ((prodMkLeft α η) y.1) (Prod.mk y.2 ⁻¹' s)) = fun y ↦
    ((prodMkRight β (prodMkLeft α η)) y) (Prod.mk y.2 ⁻¹' s)
⊢ Measurable fun y ↦ ((prodMkRight β (prodMkLeft α η)) y) (Prod.mk y.2 ⁻¹' s)
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
f : β ≃ᵐ γ
η : Kernel α γ
⊢ κ.map ⇑f = η ↔ κ = η.map ⇑f.symm

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
f : β ≃ᵐ γ
η : Kernel α γ
⊢ κ.map ⇑f = η ↔ κ = η.map ⇑f.symm
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:
[

Goal state after:
α : 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) ∂μ
Module: Mathlib.Probability.Kernel.Composition.ParallelComp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → γ
g : β → δ
hf : Measurable f
hg : Measurable g
x : α × β
⊢ (deterministic f hf ∥ₖ deterministic g hg) x = (deterministic (Prod.map f g) ⋯) x

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → γ
g : β → δ
hf : Measurable f
hg : Measurable g
x : α × β
⊢ (deterministic f hf ∥ₖ deterministic g hg) x = (deterministic (Prod.map f g) ⋯) x
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
a : α
s : Set γ
hs : MeasurableSet s
⊢ ∑' (i : ℕ), (((κ.seq i).map f) a) s = ∑' (i : ℕ), ((κ.seq i) a) (f ⁻¹' s)

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
a : α
s : Set γ
hs : MeasurableSet s
⊢ ∑' (i : ℕ), (((κ.seq i).map f) a) s = ∑' (i : ℕ), ((κ.seq i) a) (f ⁻¹' s)
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

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 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 η
x : α × γ
s✝ : Set (β × δ)
a✝ : MeasurableSet s✝
⊢ ((Kernel.sum κ ∥ₖ η) x) s✝ = ((Kernel.sum fun i ↦ κ i ∥ₖ η) x) s✝

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 δ
ι : Type u_5
inst✝¹ : Countable ι
κ : ι → Kernel α β
inst✝ : ∀ (i : ι), IsSFiniteKernel (κ i)
η : Kernel γ δ
h : IsSFiniteKernel η
x : α × γ
s✝ : Set (β × δ)
a✝ : MeasurableSet s✝
⊢ ((Kernel.sum κ ∥ₖ η) x) s✝ = ((Kernel.sum fun i ↦ κ i ∥ₖ η) x) s✝
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
κ : Kernel α β
inst✝ : IsMarkovKernel κ
hf : Measurable f
a : α
⊢ ((κ.map f) a) Set.univ = 1

Tactic:
map_apply' κ hf a MeasurableSet.univ,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
κ : Kernel α β
inst✝ : IsMarkovKernel κ
hf : Measurable f
a : α
⊢ (κ a) (f ⁻¹' Set.univ) = 1
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ((κ ⊗ₖ η) a) s = (κ a ⊗ₘ η.sectR a) s

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ((κ ⊗ₖ η) a) s = (κ a ⊗ₘ η.sectR a) s
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s : Set (α × α)
hs : MeasurableSet s
h_meas : ∀ (a : α), MeasurableSet (Prod.mk a ⁻¹' s)
⊢ ∫⁻ (a : α), (Kernel.id a) (Prod.mk a ⁻¹' s) ∂μ = μ (Function.diag ⁻¹' s)

Tactic:
[

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s : Set (α × α)
hs : MeasurableSet s
h_meas : ∀ (a : α), MeasurableSet (Prod.mk a ⁻¹' s)
⊢ ∫⁻ (a : α), (Kernel.id a) (Prod.mk a ⁻¹' s) ∂μ = μ (Function.diag ⁻¹' s)
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 δ
ι : Type u_5
inst✝¹ : Countable ι
κ : Kernel α β
η : ι → Kernel γ δ
inst✝ : ∀ (i : ι), IsSFiniteKernel (η i)
h : IsSFiniteKernel κ
x : α × γ
s✝ : Set (β × δ)
a✝ : MeasurableSet s✝
⊢ ((κ ∥ₖ Kernel.sum η) x) s✝ = ((Kernel.sum fun i ↦ κ ∥ₖ η i) x) s✝

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 δ
ι : Type u_5
inst✝¹ : Countable ι
κ : Kernel α β
η : ι → Kernel γ δ
inst✝ : ∀ (i : ι), IsSFiniteKernel (η i)
h : IsSFiniteKernel κ
x : α × γ
s✝ : Set (β × δ)
a✝ : MeasurableSet s✝
⊢ ((κ ∥ₖ Kernel.sum η) x) s✝ = ((Kernel.sum fun i ↦ κ ∥ₖ η i) x) s✝
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
g : γ → α
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hg : Measurable g
a : γ
s : Set β
hs : MeasurableSet s
⊢ ∑' (i : ℕ), (((κ.seq i).comap g hg) a) s = ∑' (i : ℕ), ((κ.seq i) (g a)) s

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
g : γ → α
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hg : Measurable g
a : γ
s : Set β
hs : MeasurableSet s
⊢ ∑' (i : ℕ), (((κ.seq i).comap g hg) a) s = ∑' (i : ℕ), ((κ.seq i) (g a)) s
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite μ
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
⊢ (μ ⊗ₘ Kernel.const α ν) s = (μ.prod ν) s

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite μ
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
⊢ (μ ⊗ₘ Kernel.const α ν) s = (μ.prod ν) s
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 κ
⊢ (μ + ν) ⊗ₘ κ = μ ⊗ₘ κ + ν ⊗ₘ κ

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.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 μ
⊢ μ ⊗ₘ (κ + η) = μ ⊗ₘ κ + μ ⊗ₘ η

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 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 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 (κ ∥ₖ η)
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_5
inst✝ : Countable ι
κ : ι → Kernel α β
a✝¹ : γ × α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((Kernel.sum fun i ↦ prodMkLeft γ (κ i)) a✝¹) s✝ = ((prodMkLeft γ (Kernel.sum κ)) a✝¹) s✝

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_5
inst✝ : Countable ι
κ : ι → Kernel α β
a✝¹ : γ × α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((Kernel.sum fun i ↦ prodMkLeft γ (κ i)) a✝¹) s✝ = ((prodMkLeft γ (Kernel.sum κ)) a✝¹) 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_5
inst✝ : Countable ι
κ : ι → Kernel α β
a✝¹ : α × γ
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((Kernel.sum fun i ↦ prodMkRight γ (κ i)) a✝¹) s✝ = ((prodMkRight γ (Kernel.sum κ)) a✝¹) s✝

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_5
inst✝ : Countable ι
κ : ι → Kernel α β
a✝¹ : α × γ
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((Kernel.sum fun i ↦ prodMkRight γ (κ i)) a✝¹) s✝ = ((prodMkRight γ (Kernel.sum κ)) a✝¹) s✝
Module: Mathlib.Probability.Kernel.Composition.CompMap

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
hf : Measurable f
κ : Kernel α β
a : α
s : Set γ
hs : MeasurableSet s
⊢ ((deterministic f hf ∘ₖ κ) a) s = ((κ.map f) a) s

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
hf : Measurable f
κ : Kernel α β
a : α
s : Set γ
hs : MeasurableSet s
⊢ ((deterministic f hf ∘ₖ κ) a) s = ((κ.map f) a) s
Module: Mathlib.Probability.Kernel.Composition.CompMap

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
g : γ → α
κ : Kernel α β
hg : Measurable g
a : γ
s : Set β
hs : MeasurableSet s
⊢ ((κ ∘ₖ deterministic g hg) a) s = ((κ.comap g hg) a) s

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
g : γ → α
κ : Kernel α β
hg : Measurable g
a : γ
s : Set β
hs : MeasurableSet s
⊢ ((κ ∘ₖ deterministic g hg) a) s = ((κ.comap g hg) a) s
Module: Mathlib.Probability.Kernel.Composition.CompMap

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
⊢ swap α β ∘ₖ swap β α = Kernel.id

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
⊢ swap α β ∘ₖ swap β α = Kernel.id
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
⊢ ∫⁻ (c : γ × β), g c ∂κ.swapRight a = ∫⁻ (bc : β × γ), g bc.swap ∂κ a

Tactic:
by
  rw [swapRight_eq, lintegral_map _ measurable_swap a hg]

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

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
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.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 β (γ × δ)
⊢ (η ∘ₖ κ).snd = η.snd ∘ₖ κ

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 β (γ × δ)
⊢ (η ∘ₖ κ).snd = η.snd ∘ₖ κ
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
⊢ ((κ ×ₖ η) a) s = ∫⁻ (b : β), (η a) (Prod.mk b ⁻¹' s) ∂κ a

Tactic:
[

Goal state after:
α : 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
⊢ ((κ ×ₖ η) a) s = ∫⁻ (b : β), (η a) (Prod.mk b ⁻¹' s) ∂κ a
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
⊢ ((κ ×ₖ η) a) s = ∫⁻ (b : β), (η a) (Prod.mk b ⁻¹' s) ∂κ a

Tactic:
by
  simp_rw [prod, comp_apply, copy_apply, Measure.dirac_bind (Kernel.measurable _) (a, a),
    parallelComp_apply, Measure.prod_apply hs]

Goal state after:
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 : α
g : β × γ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (c : β × γ), g c ∂(κ ×ₖ η) a = ∫⁻ (b : β), ∫⁻ (c : γ), g (b, c) ∂η a ∂κ a

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel α γ
inst✝ : IsSFiniteKernel η
a : α
g : β × γ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (c : β × γ), g c ∂(κ ×ₖ η) a = ∫⁻ (b : β), ∫⁻ (c : γ), g (b, c) ∂η a ∂κ a
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 : α
g : β × γ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (c : β × γ), g c ∂(κ ∥ₖ η) (a, a) = ∫⁻ (b : β), ∫⁻ (c : γ), g (b, c) ∂η a ∂κ a

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel α γ
inst✝ : IsSFiniteKernel η
a : α
g : β × γ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (c : β × γ), g c ∂(κ ∥ₖ η) (a, a) = ∫⁻ (b : β), ∫⁻ (c : γ), g (b, c) ∂η a ∂κ a
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case e_f
α : 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 : α
b : β
h_int : ∀ (x : γ), ∫⁻ (y : β), ((swap γ β) (x, y)) s ∂Measure.dirac b = (Prod.mk b ⁻¹' s).indicator 1 x
⊢ ∫⁻ (x : γ), ∫⁻ (y : β), ((swap γ β) (x, y)) s ∂Measure.dirac b ∂η (a, b) = (η (a, b)) (Prod.mk b ⁻¹' s)

Tactic:
[

Goal state after:
case e_f
α : 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 : α
b : β
h_int : ∀ (x : γ), ∫⁻ (y : β), ((swap γ β) (x, y)) s ∂Measure.dirac b = (Prod.mk b ⁻¹' s).indicator 1 x
⊢ ∫⁻ (x : γ), ∫⁻ (y : β), ((swap γ β) (x, y)) s ∂Measure.dirac b ∂η (a, b) = (η (a, b)) (Prod.mk b ⁻¹' s)
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η η' : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : IsSFiniteKernel η'
h : ∀ (a : α), ∀ᵐ (b : β) ∂κ a, η (a, b) = η' (a, b)
hκ : ¬IsSFiniteKernel κ
⊢ κ ⊗ₖ η = κ ⊗ₖ η'

Tactic:
[

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η η' : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : IsSFiniteKernel η'
h : ∀ (a : α), ∀ᵐ (b : β) ∂κ a, η (a, b) = η' (a, b)
hκ : ¬IsSFiniteKernel κ
⊢ κ ⊗ₖ η = κ ⊗ₖ η'
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : SFinite ν
hκ : ¬IsSFiniteKernel κ
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η

pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : SFinite ν
hκ : IsSFiniteKernel κ
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η

Tactic:
· rw [compProd_of_not_isSFiniteKernel _ _ hκ]; simp

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ⟂ₘ ν
κ η : Kernel α β
hμ : SFinite μ
hν : SFinite ν
hκ : IsSFiniteKernel κ
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
Module: Mathlib.Probability.Kernel.Composition.KernelLemmas

Goal state before:
pp: case pos
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
η : Kernel Z T
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
ac : X × Z
s : Set (T × Y)
hs : MeasurableSet s
⊢ ((swap Y T ∘ₖ (κ ∥ₖ η)) ac) s = ((η ∥ₖ κ ∘ₖ swap X Z) ac) s

Tactic:
[

Goal state after:
case pos
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
η : Kernel Z T
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
ac : X × Z
s : Set (T × Y)
hs : MeasurableSet s
⊢ ((swap Y T ∘ₖ (κ ∥ₖ η)) ac) s = ((η ∥ₖ κ ∘ₖ swap X Z) ac) s
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : κ ⊗ₖ η = 0
⊢ ∀ (a : α), ∀ᵐ (b : β) ∂κ a, η (a, b) = 0

Tactic:
[

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : κ ⊗ₖ η = 0
⊢ ∀ (a : α), ∀ᵐ (b : β) ∂κ a, η (a, b) = 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 α β
inst✝¹ : IsMarkovKernel κ
η : Kernel α γ
inst✝ : IsSFiniteKernel η
x : α
s✝ : Set γ
a✝ : MeasurableSet s✝
⊢ ((κ ×ₖ η).snd x) s✝ = (η x) s✝

Tactic:
simp [snd_apply, prod_apply]

Goal state after:
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 α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsMarkovKernel η
x : α
⊢ ((κ ⊗ₖ η) x) (Prod.fst ⁻¹' s) = (κ x) s

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 α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsMarkovKernel η
x : α
⊢ ((κ ⊗ₖ η) x) (Prod.fst ⁻¹' s) = (κ x) s