mathlib-initiative/mathlib-tactics huggingface dataset:
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 γ
inst✝¹ : MeasurableSingletonClass γ
f : α × β → γ
hf : Measurable f
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
x : α
t : Set β := {b | (b, f (x, b)) ∈ s}
ht : MeasurableSet t
this : ∀ b ∈ t, (if f (x, b) ∈ Prod.mk b ⁻¹' s then 1 else 0) = 1
⊢ (κ x) {b | (b, f (x, b)) ∈ s} = (κ x) t

Tactic:
]

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
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel α γ
inst✝ : IsSFiniteKernel η
f : β → δ
hf : Measurable f
⊢ κ.map f ×ₖ η = κ.map f ×ₖ η

Tactic:
]

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✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
⊢ μ ⊗ₘ κ ⟂ₘ ν.singularPart μ ⊗ₘ η ∧ μ ⊗ₘ κ ⟂ₘ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η ↔ μ ⊗ₘ κ ⟂ₘ μ ⊗ₘ η

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
⊢ μ ⊗ₘ κ ⟂ₘ ν.singularPart μ ⊗ₘ η ∧ μ ⊗ₘ κ ⟂ₘ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η ↔ μ ⊗ₘ κ ⟂ₘ μ ⊗ₘ η
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
X' : Type u_5
mX' : MeasurableSpace X'
η : Kernel X' Z
inst✝¹ : IsSFiniteKernel η
ξ : Kernel Z T
inst✝ : IsSFiniteKernel ξ
hκ : IsSFiniteKernel κ
a : X × X'
s : Set (Y × T)
hs : MeasurableSet s
⊢ ∫⁻ (x : Y), ∫⁻ (y : Z), ((Kernel.id ∥ₖ ξ) (x, y)) s ∂η a.2 ∂κ a.1 =
    ∫⁻ (x : Y), ((ξ ∘ₖ η) a.2) (Prod.mk x ⁻¹' s) ∂κ a.1

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
X' : Type u_5
mX' : MeasurableSpace X'
η : Kernel X' Z
inst✝¹ : IsSFiniteKernel η
ξ : Kernel Z T
inst✝ : IsSFiniteKernel ξ
hκ : IsSFiniteKernel κ
a : X × X'
s : Set (Y × T)
hs : MeasurableSet s
⊢ ∫⁻ (x : Y), ∫⁻ (y : Z), ((Kernel.id ∥ₖ ξ) (x, y)) s ∂η a.2 ∂κ a.1 =
    ∫⁻ (x : Y), ((ξ ∘ₖ η) a.2) (Prod.mk x ⁻¹' s) ∂κ a.1
Module: Mathlib.Probability.Kernel.Composition.Prod

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 γ δ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
⊢ ∀ (a : α × γ) (f : δ × β → ℝ≥0∞),
    Measurable f →
      ∫⁻ (b : δ × β), f b ∂((prodMkRight α η ×ₖ prodMkLeft γ κ).comap Prod.swap ⋯) a =
        ∫⁻ (b : δ × β), f b ∂((prodMkRight γ κ ×ₖ prodMkLeft α η).map Prod.swap) a

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 γ δ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
⊢ ∀ (a : α × γ) (f : δ × β → ℝ≥0∞),
    Measurable f →
      ∫⁻ (b : δ × β), f b ∂((prodMkRight α η ×ₖ prodMkLeft γ κ).comap Prod.swap ⋯) a =
        ∫⁻ (b : δ × β), f b ∂((prodMkRight γ κ ×ₖ prodMkLeft α η).map Prod.swap) a
Module: Mathlib.Probability.Kernel.Composition.KernelLemmas

Goal state before:
pp: case pos.e_f
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
X' : Type u_5
mX' : MeasurableSpace X'
η : Kernel X' Z
inst✝¹ : IsSFiniteKernel η
ξ : Kernel Z T
inst✝ : IsSFiniteKernel ξ
hκ : IsSFiniteKernel κ
a : X × X'
s : Set (Y × T)
hs : MeasurableSet s
x : Y
⊢ ∫⁻ (y : Z), ((Kernel.id ∥ₖ ξ) (x, y)) s ∂η a.2 = ∫⁻ (b : Z), (ξ b) (Prod.mk x ⁻¹' s) ∂η a.2

Tactic:
]

Goal state after:
case pos.e_f
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
X' : Type u_5
mX' : MeasurableSpace X'
η : Kernel X' Z
inst✝¹ : IsSFiniteKernel η
ξ : Kernel Z T
inst✝ : IsSFiniteKernel ξ
hκ : IsSFiniteKernel κ
a : X × X'
s : Set (Y × T)
hs : MeasurableSet s
x : Y
⊢ ∫⁻ (y : Z), ((Kernel.id ∥ₖ ξ) (x, y)) s ∂η a.2 = ∫⁻ (b : Z), (ξ b) (Prod.mk x ⁻¹' s) ∂η a.2
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ μ.singularPart ν ⊗ₘ κ ⟂ₘ ν ⊗ₘ η ∧ ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ ⟂ₘ ν ⊗ₘ η ↔
    ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ μ.singularPart ν ⊗ₘ κ ⟂ₘ ν ⊗ₘ η ∧ ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ ⟂ₘ ν ⊗ₘ η ↔
    ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η
Module: Mathlib.Probability.Kernel.Composition.KernelLemmas

Goal state before:
pp: case pos.e_f.e_f
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
X' : Type u_5
mX' : MeasurableSpace X'
η : Kernel X' Z
inst✝¹ : IsSFiniteKernel η
ξ : Kernel Z T
inst✝ : IsSFiniteKernel ξ
hκ : IsSFiniteKernel κ
a : X × X'
s : Set (Y × T)
hs : MeasurableSet s
x : Y
y : Z
⊢ (ξ (x, y).2) (Prod.mk (x, y).1 ⁻¹' s) = (ξ y) (Prod.mk x ⁻¹' s)

Tactic:
]

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✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ ⟂ₘ ν.withDensity (μ.rnDeriv ν) ⊗ₘ η ↔
    ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ ⟂ₘ ν.withDensity (μ.rnDeriv ν) ⊗ₘ η ↔
    ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η
Module: Mathlib.Probability.Kernel.Composition.KernelLemmas

Goal state before:
pp: 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
X' : Type u_5
mX' : MeasurableSpace X'
η : Kernel X' Z
inst✝¹ : IsSFiniteKernel η
ξ : Kernel Z T
inst✝ : IsSFiniteKernel ξ
this : swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ) = swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ)
⊢ swap Y T ∘ₖ (swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ)) = swap Y T ∘ₖ (swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ))

Tactic:
]

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 (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
h2s : ((κ ⊗ₖ η) a) s ≠ ∞
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η) a) s
this : ∀ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ≤ (η (a, b)) (Prod.mk b ⁻¹' t)
ht : MeasurableSet t
⊢ ((κ ⊗ₖ η) a) s ≠ ∞

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
h2s : ((κ ⊗ₖ η) a) s ≠ ∞
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η) a) s
this : ∀ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ≤ (η (a, b)) (Prod.mk b ⁻¹' t)
ht : MeasurableSet t
⊢ ((κ ⊗ₖ η) a) s ≠ ∞
Module: Mathlib.Probability.Kernel.Composition.Prod

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 γ δ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α × γ
f : δ × β → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (b : δ), ∫⁻ (c : β), f (b, c) ∂(prodMkLeft γ κ) x.swap ∂(prodMkRight α η) x.swap =
    ∫⁻ (b : β), ∫⁻ (c : δ), f (b, c).swap ∂(prodMkLeft α η) x ∂(prodMkRight γ κ) x

pp: case hg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α × γ
f : δ × β → ℝ≥0∞
hf : Measurable f
⊢ Measurable fun a ↦ f a.swap

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 γ δ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α × γ
f : δ × β → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (b : δ), ∫⁻ (c : β), f (b, c) ∂(prodMkLeft γ κ) x.swap ∂(prodMkRight α η) x.swap =
    ∫⁻ (b : β), ∫⁻ (c : δ), f (b, c).swap ∂(prodMkLeft α η) x ∂(prodMkRight γ κ) x

case hg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α × γ
f : δ × β → ℝ≥0∞
hf : Measurable f
⊢ Measurable fun a ↦ f a.swap
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 (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
h2s : ((κ ⊗ₖ η) a) s ≠ ∞
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η) a) s
this : ∀ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ≤ (η (a, b)) (Prod.mk b ⁻¹' t)
ht : MeasurableSet t
h2t : ∫⁻ (b : β), (η (a, b)) (Prod.mk b ⁻¹' t) ∂κ a ≠ ∞
⊢ ∀ᵐ (b : β) ∂κ a, (η (a, b)) (Prod.mk b ⁻¹' t) < ∞

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
h2s : ((κ ⊗ₖ η) a) s ≠ ∞
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η) a) s
this : ∀ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ≤ (η (a, b)) (Prod.mk b ⁻¹' t)
ht : MeasurableSet t
h2t : ∫⁻ (b : β), (η (a, b)) (Prod.mk b ⁻¹' t) ∂κ a ≠ ∞
⊢ ∀ᵐ (b : β) ∂κ a, (η (a, b)) (Prod.mk b ⁻¹' t) < ∞
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η ↔ ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η

Tactic:
conv_lhs => rw [μ.haveLebesgueDecomposition_add ν]
  rw [compProd_add_left, MutuallySingular.add_left_iff]
  simp only [(mutuallySingular_singularPart μ ν).compProd_of_left κ η, true_and]
  rw [(withDensity_absolutelyContinuous ν (μ.rnDeriv ν)).mutuallySingular_compProd_iff]
  refine ⟨fun h ξ hξ hξμ hξν ↦ ?_, fun h ↦ ?_⟩
  · exact h.mono_ac ((hξμ.withDensity_rnDeriv hξν).compProd_left _)
      ((hξμ.withDensity_rnDeriv hξν).compProd_left _)
  · refine h _ ?_ ?_ ?_
    · infer_instance
    · exact absolutelyContinuous_of_le (withDensity_rnDeriv_le _ _)
    · exact withDensity_absolutelyContinuous ν (μ.rnDeriv ν)

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✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hκη : μ ⊗ₘ κ ≪ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η + ν.singularPart μ ⊗ₘ η
⊢ μ ⊗ₘ κ ≪ μ ⊗ₘ η

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hκη : μ ⊗ₘ κ ≪ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η + ν.singularPart μ ⊗ₘ η
⊢ μ ⊗ₘ κ ≪ μ ⊗ₘ η
Module: Mathlib.Probability.Kernel.Composition.KernelLemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
X' : Type u_5
Y' : Type u_6
Z' : Type u_7
mX' : MeasurableSpace X'
mY' : MeasurableSpace Y'
mZ' : MeasurableSpace Z'
inst✝³ : IsSFiniteKernel κ
η : Kernel Y Z
inst✝² : IsSFiniteKernel η
κ' : Kernel X' Y'
inst✝¹ : IsSFiniteKernel κ'
η' : Kernel Y' Z'
inst✝ : IsSFiniteKernel η'
⊢ η ∥ₖ η' ∘ₖ (κ ∥ₖ κ') = η ∥ₖ η' ∘ₖ (κ ∥ₖ κ')

Tactic:
]

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 (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
hs : MeasurableSet s
⊢ (fun b ↦ (η (a, b)) (Prod.mk b ⁻¹' s)) =ᵐ[κ a] 0 ↔ (fun b ↦ (η (a, b)) (Prod.mk b ⁻¹' s)) =ᵐ[κ a] 0

pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
hs : MeasurableSet s
⊢ Measurable fun b ↦ (η (a, b)) (Prod.mk b ⁻¹' s)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
hs : MeasurableSet s
⊢ Measurable fun b ↦ (η (a, b)) (Prod.mk b ⁻¹' 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 α β
η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
⊢ ∀ (a : α) (f : γ × β → ℝ≥0∞),
    Measurable f → ∫⁻ (b : γ × β), f b ∂((κ ×ₖ η).map Prod.swap) a = ∫⁻ (b : γ × β), f b ∂(η ×ₖ κ) a

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
⊢ ∀ (a : α) (f : γ × β → ℝ≥0∞),
    Measurable f → ∫⁻ (b : γ × β), f b ∂((κ ×ₖ η).map Prod.swap) a = ∫⁻ (b : γ × β), f b ∂(η ×ₖ κ) a
Module: Mathlib.Probability.Kernel.Composition.KernelLemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
Y' : Type u_6
Z' : Type u_7
mY' : MeasurableSpace Y'
mZ' : MeasurableSpace Z'
inst✝³ : IsSFiniteKernel κ
η : Kernel Y Z
inst✝² : IsSFiniteKernel η
κ' : Kernel X Y'
inst✝¹ : IsSFiniteKernel κ'
η' : Kernel Y' Z'
inst✝ : IsSFiniteKernel η'
⊢ η ∘ₖ κ ∥ₖ (η' ∘ₖ κ') ∘ₖ copy X = η ∘ₖ κ ∥ₖ (η' ∘ₖ κ') ∘ₖ copy X

Tactic:
]

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 (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
h : ((κ ⊗ₖ η) a) s = 0
t : Set (β × γ)
hst : s ⊆ t
mt : MeasurableSet t
ht : (fun b ↦ (η (a, b)) (Prod.mk b ⁻¹' t)) =ᵐ[κ a] 0
⊢ (fun b ↦ (η (a, b)) (Prod.mk b ⁻¹' s)) ≤ᵐ[κ a] 0 ∧ 0 ≤ᵐ[κ a] fun b ↦ (η (a, b)) (Prod.mk b ⁻¹' s)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
h : ((κ ⊗ₖ η) a) s = 0
t : Set (β × γ)
hst : s ⊆ t
mt : MeasurableSet t
ht : (fun b ↦ (η (a, b)) (Prod.mk b ⁻¹' t)) =ᵐ[κ a] 0
⊢ (fun b ↦ (η (a, b)) (Prod.mk b ⁻¹' s)) ≤ᵐ[κ a] 0 ∧ 0 ≤ᵐ[κ a] fun b ↦ (η (a, b)) (Prod.mk b ⁻¹' s)
Module: Mathlib.Probability.Kernel.Composition.MeasureComp

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
⊢ ⇑κ ∘ₘ μ = ⇑κ ∘ₘ μ

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (a : α), (κ a) s ∂μ = ∑' (i : α), (μ {i} • κ i) s

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (a : α), (κ a) s ∂μ = ∑' (i : α), (μ {i} • κ i) s
Module: Mathlib.Probability.Kernel.Composition.MeasureComp

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

pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst✝¹ : SFinite μ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (Prod.snd ⁻¹' s)

Tactic:
]

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

α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst✝¹ : SFinite μ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (Prod.snd ⁻¹' s)
Module: Mathlib.Probability.Kernel.Composition.MeasureComp

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
p : β → Prop
h : ∀ᵐ (ω : β) ∂(κ ∘ₖ Kernel.const Unit μ) (), p ω
⊢ ∀ᵐ (ω' : α) ∂μ, ∀ᵐ (ω : β) ∂κ ω', p ω

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
p : β → Prop
h : ∀ᵐ (ω : β) ∂(κ ∘ₖ Kernel.const Unit μ) (), p ω
⊢ ∀ᵐ (ω' : α) ∂μ, ∀ᵐ (ω : β) ∂κ ω', p ω
Module: Mathlib.Probability.Kernel.Composition.MeasureComp

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
p : β → Prop
hp : MeasurableSet {z | p z}
h : ∀ᵐ (y : α) ∂μ, ∀ᵐ (z : β) ∂κ y, p z
⊢ ∀ᵐ (z : β) ∂(κ ∘ₖ Kernel.const Unit μ) (), p z

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
p : β → Prop
hp : MeasurableSet {z | p z}
h : ∀ᵐ (y : α) ∂μ, ∀ᵐ (z : β) ∂κ y, p z
⊢ ∀ᵐ (z : β) ∂(κ ∘ₖ Kernel.const Unit μ) (), p z
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 η
x : α
f : γ × β → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (b : β), ∫⁻ (c : γ), f (b, c).swap ∂η x ∂κ x = ∫⁻ (b : γ), ∫⁻ (c : β), f (b, c) ∂κ x ∂η x

pp: case hg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α
f : γ × β → ℝ≥0∞
hf : Measurable f
⊢ Measurable fun a ↦ f a.swap

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α
f : γ × β → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (b : β), ∫⁻ (c : γ), f (b, c).swap ∂η x ∂κ x = ∫⁻ (b : γ), ∫⁻ (c : β), f (b, c) ∂κ x ∂η x

case hg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α
f : γ × β → ℝ≥0∞
hf : Measurable f
⊢ Measurable fun a ↦ f a.swap
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 η
⊢ η ∥ₖ κ = η ∥ₖ κ

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
⊢ SFinite (μ ⊗ₘ κ).snd

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
⊢ SFinite (μ ⊗ₘ κ).snd
Module: Mathlib.Probability.Kernel.Composition.MeasureComp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteKernel κ
⊢ IsFiniteMeasure (μ ⊗ₘ κ).snd

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteKernel κ
⊢ IsFiniteMeasure (μ ⊗ₘ κ).snd
Module: Mathlib.Probability.Kernel.Composition.MeasureComp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsMarkovKernel κ
⊢ IsProbabilityMeasure (μ ⊗ₘ κ).snd

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsMarkovKernel κ
⊢ IsProbabilityMeasure (μ ⊗ₘ κ).snd
Module: Mathlib.Probability.Kernel.Composition.MeasureComp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : IsZeroOrProbabilityMeasure μ
inst✝ : IsZeroOrMarkovKernel κ
⊢ IsZeroOrProbabilityMeasure (μ ⊗ₘ κ).snd

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : IsZeroOrProbabilityMeasure μ
inst✝ : IsZeroOrMarkovKernel κ
⊢ IsZeroOrProbabilityMeasure (μ ⊗ₘ κ).snd
Module: Mathlib.Probability.Kernel.Composition.KernelLemmas

Goal state before:
pp: 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
inst✝ : IsSFiniteKernel κ
⊢ η ∥ₖ (κ ∘ₖ Kernel.id) = η ∥ₖ κ

Tactic:
]

Goal state after:
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
inst✝ : IsSFiniteKernel κ
⊢ η ∥ₖ (κ ∘ₖ Kernel.id) = η ∥ₖ κ