awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst : IsSFiniteKernel κ
η : Kernel ε β'
inst_1 : IsSFiniteKernel η
ξ : Kernel (β × ε) δ
inst_2 : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : β × ε) ↦
    ∫⁻ (c : δ),
      (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : β × ε) → Measure δ) b

Tactic:
exact (measurable_measure_prodMk_left hs).lintegral_kernel

Premises used: Measurable.lintegral_kernel, measurable_measure_prodMk_left
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst : IsSFiniteKernel κ
η : Kernel ε β'
inst_1 : IsSFiniteKernel η
ξ : Kernel (β × ε) δ
inst_2 : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : δ) ↦
    (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞) (Prod.mk b ⁻¹' s)

Tactic:
measurable_measure_prodMk_left hs

Premises used: measurable_measure_prodMk_left
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst : IsSFiniteKernel κ
η : Kernel ε β'
inst_1 : IsSFiniteKernel η
ξ : Kernel (β × ε) δ
inst_2 : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : δ) ↦
    (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞) (Prod.mk b ⁻¹' s)

Tactic:
exact measurable_measure_prodMk_left hs

Premises used: measurable_measure_prodMk_left
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst : IsSFiniteKernel κ
η : Kernel ε β'
inst_1 : IsSFiniteKernel η
ξ : Kernel (β × ε) δ
inst_2 : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : β × ε) ↦
    (((ξ ×ₖ prodMkLeft β η : (a : β × ε) → Measure (δ × β')) b : Measure (δ × β')) : (a : Set (δ × β')) → ℝ≥0∞) s

Tactic:
Kernel.measurable_coe _ hs

Premises used: ProbabilityTheory.Kernel.measurable_coe
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst : IsSFiniteKernel κ
η : Kernel ε β'
inst_1 : IsSFiniteKernel η
ξ : Kernel (β × ε) δ
inst_2 : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : β × ε) ↦
    (((ξ ×ₖ prodMkLeft β η : (a : β × ε) → Measure (δ × β')) b : Measure (δ × β')) : (a : Set (δ × β')) → ℝ≥0∞) s

Tactic:
exact Kernel.measurable_coe _ hs

Premises used: ProbabilityTheory.Kernel.measurable_coe
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst : IsSFiniteKernel κ
η : Kernel ε β'
inst_1 : IsSFiniteKernel η
ξ : Kernel (ε × β) δ
inst_2 : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
h :
  ∀ (ω : γ) (s : Set (δ × β')) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞)
      ((((ξ ×ₖ prodMkRight β η ∘ₖ (deterministic f hf ×ₖ κ) : (a : γ) → Measure (δ × β')) ω : Measure (δ × β')) :
            (a : Set (δ × β')) → ℝ≥0∞)
          s :
        ℝ≥0∞)
      ((((ξ ∘ₖ (deterministic f hf ×ₖ κ) ×ₖ (η ∘ₖ deterministic f hf) : (a : γ) → Measure (δ × β')) ω :
              Measure (δ × β')) :
            (a : Set (δ × β')) → ℝ≥0∞)
          s :
        ℝ≥0∞)
⊢ ξ ×ₖ prodMkRight β η ∘ₖ (deterministic f hf ×ₖ κ) = ξ ∘ₖ (deterministic f hf ×ₖ κ) ×ₖ (η ∘ₖ deterministic f hf)

Tactic:
ext ω s hs
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst : IsSFiniteKernel κ
η : Kernel ε β'
inst_1 : IsSFiniteKernel η
ξ : Kernel (ε × β) δ
inst_2 : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
h :
  ∫⁻ (c : β),
      (((ξ ×ₖ prodMkRight β η : (a : ε × β) → Measure (δ × β')) (f ω, c) : Measure (δ × β')) :
          (a : Set (δ × β')) → ℝ≥0∞)
        s ∂(κ : (a : γ) → Measure β) ω =
    ∫⁻ (c : β),
      ∫⁻ (c : δ),
        (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
          (Prod.mk c ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) (f ω, c) ∂(κ : (a : γ) → Measure β) ω
h₁ :
  Measurable (β := ℝ≥0∞) fun (b : ε × β) ↦
    ∫⁻ (c : δ),
      (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) b
h₂ :
  Measurable (β := ℝ≥0∞) fun (b : δ) ↦
    (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞) (Prod.mk b ⁻¹' s)
h₃ :
  Measurable (β := ℝ≥0∞) fun (b : ε × β) ↦
    (((ξ ×ₖ prodMkRight β η : (a : ε × β) → Measure (δ × β')) b : Measure (δ × β')) : (a : Set (δ × β')) → ℝ≥0∞) s
⊢ Eq (α := ℝ≥0∞)
    ((((ξ ×ₖ prodMkRight β η ∘ₖ (deterministic f hf ×ₖ κ) : (a : γ) → Measure (δ × β')) ω : Measure (δ × β')) :
          (a : Set (δ × β')) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((ξ ∘ₖ (deterministic f hf ×ₖ κ) ×ₖ (η ∘ₖ deterministic f hf) : (a : γ) → Measure (δ × β')) ω :
            Measure (δ × β')) :
          (a : Set (δ × β')) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
rw [prod_apply' _ _ _ hs, comp_apply' _ _ _ hs, lintegral_deterministic_prod,
    lintegral_comp, lintegral_deterministic_prod]

Premises used: ProbabilityTheory.Kernel.prod_apply', ProbabilityTheory.Kernel.lintegral_deterministic_prod, ProbabilityTheory.Kernel.lintegral_comp, ProbabilityTheory.Kernel.comp_apply'
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst : IsSFiniteKernel κ
η : Kernel ε β'
inst_1 : IsSFiniteKernel η
ξ : Kernel (ε × β) δ
inst_2 : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
h :
  ∀ (b : β),
    (((ξ ×ₖ prodMkRight β η : (a : ε × β) → Measure (δ × β')) (f ω, b) : Measure (δ × β')) : (a : Set (δ × β')) → ℝ≥0∞)
        s =
      ∫⁻ (c : δ),
        (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
          (Prod.mk c ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) (f ω, b)
⊢ ∫⁻ (c : β),
      (((ξ ×ₖ prodMkRight β η : (a : ε × β) → Measure (δ × β')) (f ω, c) : Measure (δ × β')) :
          (a : Set (δ × β')) → ℝ≥0∞)
        s ∂(κ : (a : γ) → Measure β) ω =
    ∫⁻ (c : β),
      ∫⁻ (c : δ),
        (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
          (Prod.mk c ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) (f ω, c) ∂(κ : (a : γ) → Measure β) ω

Tactic:
congr with b
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst : IsSFiniteKernel κ
η : Kernel ε β'
inst_1 : IsSFiniteKernel η
ξ : Kernel (ε × β) δ
inst_2 : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
b : β
h :
  ∫⁻ (b_1 : δ),
      (((prodMkRight β η : (a : ε × β) → Measure β') (f ω, b) : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk b_1 ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) (f ω, b) =
    ∫⁻ (c : δ),
      (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) (f ω, b)
h₁ :
  ∫⁻ (b_1 : δ),
      (((η : (a : ε) → Measure β') (f ω, b).1 : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk b_1 ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) (f ω, b) =
    ∫⁻ (c : δ),
      (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) (f ω, b)
h₂ :
  ∫⁻ (b_1 : δ),
      (((η : (a : ε) → Measure β') (f ω, b).1 : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk b_1 ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) (f ω, b) =
    ∫⁻ (c : δ),
      (((η.comap f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) (f ω, b)
h₃ h₄ :
  ∫⁻ (b_1 : δ),
      (((η : (a : ε) → Measure β') (f ω, b).1 : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk b_1 ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) (f ω, b) =
    ∫⁻ (c : δ),
      (((η : (a : ε) → Measure β') (f ω) : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) (f ω, b)
⊢ (((ξ ×ₖ prodMkRight β η : (a : ε × β) → Measure (δ × β')) (f ω, b) : Measure (δ × β')) : (a : Set (δ × β')) → ℝ≥0∞)
      s =
    ∫⁻ (c : δ),
      (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) (f ω, b)

Tactic:
rw [prod_apply' _ _ _ hs, prodMkRight_apply, comp_deterministic_eq_comap, comap_apply]

Premises used: ProbabilityTheory.Kernel.prod_apply', ProbabilityTheory.Kernel.prodMkRight_apply, ProbabilityTheory.Kernel.comap_apply, ProbabilityTheory.Kernel.comp_deterministic_eq_comap
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst : IsSFiniteKernel κ
η : Kernel ε β'
inst_1 : IsSFiniteKernel η
ξ : Kernel (ε × β) δ
inst_2 : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : ε × β) ↦
    ∫⁻ (c : δ),
      (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) b

Tactic:
(measurable_measure_prodMk_left hs).lintegral_kernel

Premises used: Measurable.lintegral_kernel, measurable_measure_prodMk_left
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst : IsSFiniteKernel κ
η : Kernel ε β'
inst_1 : IsSFiniteKernel η
ξ : Kernel (ε × β) δ
inst_2 : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : ε × β) ↦
    ∫⁻ (c : δ),
      (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞)
        (Prod.mk c ⁻¹' s) ∂(ξ : (a : ε × β) → Measure δ) b

Tactic:
exact (measurable_measure_prodMk_left hs).lintegral_kernel

Premises used: Measurable.lintegral_kernel, measurable_measure_prodMk_left
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst : IsSFiniteKernel κ
η : Kernel ε β'
inst_1 : IsSFiniteKernel η
ξ : Kernel (ε × β) δ
inst_2 : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : δ) ↦
    (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞) (Prod.mk b ⁻¹' s)

Tactic:
measurable_measure_prodMk_left hs

Premises used: measurable_measure_prodMk_left
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst : IsSFiniteKernel κ
η : Kernel ε β'
inst_1 : IsSFiniteKernel η
ξ : Kernel (ε × β) δ
inst_2 : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : δ) ↦
    (((η ∘ₖ deterministic f hf : (a : γ) → Measure β') ω : Measure β') : (a : Set β') → ℝ≥0∞) (Prod.mk b ⁻¹' s)

Tactic:
exact measurable_measure_prodMk_left hs

Premises used: measurable_measure_prodMk_left
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst : IsSFiniteKernel κ
η : Kernel ε β'
inst_1 : IsSFiniteKernel η
ξ : Kernel (ε × β) δ
inst_2 : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : ε × β) ↦
    (((ξ ×ₖ prodMkRight β η : (a : ε × β) → Measure (δ × β')) b : Measure (δ × β')) : (a : Set (δ × β')) → ℝ≥0∞) s

Tactic:
Kernel.measurable_coe _ hs

Premises used: ProbabilityTheory.Kernel.measurable_coe
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst : IsSFiniteKernel κ
η : Kernel ε β'
inst_1 : IsSFiniteKernel η
ξ : Kernel (ε × β) δ
inst_2 : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : ε × β) ↦
    (((ξ ×ₖ prodMkRight β η : (a : ε × β) → Measure (δ × β')) b : Measure (δ × β')) : (a : Set (δ × β')) → ℝ≥0∞) s

Tactic:
exact Kernel.measurable_coe _ hs

Premises used: ProbabilityTheory.Kernel.measurable_coe
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : SFinite μ
pos :
  ∀ (hκ : IsSFiniteKernel κ),
    μ ⊗ₘ κ =
      bind (α := α × α) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy α) : (a : α) → Measure (α × α)) ∘ₘ μ)
        (⇑(Kernel.id ∥ₖ κ) : (a : α × α) → Measure (α × β))
neg :
  ∀ (hκ : ¬IsSFiniteKernel κ),
    μ ⊗ₘ κ =
      bind (α := α × α) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy α) : (a : α) → Measure (α × α)) ∘ₘ μ)
        (⇑(Kernel.id ∥ₖ κ) : (a : α × α) → Measure (α × β))
⊢ μ ⊗ₘ κ =
    bind (α := α × α) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy α) : (a : α) → Measure (α × α)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ κ) : (a : α × α) → Measure (α × β))

Tactic:
by_cases hκ : IsSFiniteKernel κ

Premises used: ProbabilityTheory.IsSFiniteKernel
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : SFinite μ
hκ : ¬IsSFiniteKernel κ
⊢ μ ⊗ₘ κ =
    bind (α := α × α) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy α) : (a : α) → Measure (α × α)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ κ) : (a : α × α) → Measure (α × β))

Tactic:
simp [hκ]
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : SFinite μ
hκ : IsSFiniteKernel κ
pos :
  Eq (α := Measure (α × β)) ((⇑(Kernel.id ×ₖ κ) : (a : α) → Measure (α × β)) ∘ₘ μ)
    (bind (α := α × α) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy α) : (a : α) → Measure (α × α)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ κ) : (a : α × α) → Measure (α × β)))
pos₁ :
  Eq (α := Measure (α × β)) ((⇑(Kernel.id ∥ₖ κ ∘ₖ Kernel.copy α) : (a : α) → Measure (α × β)) ∘ₘ μ)
    (bind (α := α × α) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy α) : (a : α) → Measure (α × α)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ κ) : (a : α × α) → Measure (α × β)))
pos₂ pos₃ :
  Eq (α := Measure (α × β)) ((⇑(Kernel.id ∥ₖ κ ∘ₖ Kernel.copy α) : (a : α) → Measure (α × β)) ∘ₘ μ)
    ((⇑(Kernel.id ∥ₖ κ ∘ₖ Kernel.copy α) : (a : α) → Measure (α × β)) ∘ₘ μ)
⊢ μ ⊗ₘ κ =
    bind (α := α × α) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy α) : (a : α) → Measure (α × α)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ κ) : (a : α × α) → Measure (α × β))

Tactic:
rw [compProd_eq_comp_prod, ← Kernel.parallelComp_comp_copy, Measure.comp_assoc]

Premises used: ProbabilityTheory.Kernel.parallelComp_comp_copy, MeasureTheory.Measure.compProd_eq_comp_prod, MeasureTheory.Measure.comp_assoc
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst : SFinite ν
κ : Kernel β γ
inst_1 : IsSFiniteKernel κ
h :
  ∀ (s : Set (α × γ)) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((μ.prod ((⇑κ : (a : β) → Measure γ) ∘ₘ ν) : (a : Set (α × γ)) → ℝ≥0∞) s : ℝ≥0∞)
      (((⇑(Kernel.id ∥ₖ κ) : (a : α × β) → Measure (α × γ)) ∘ₘ μ.prod ν : (a : Set (α × γ)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := Measure (α × γ)) (μ.prod ((⇑κ : (a : β) → Measure γ) ∘ₘ ν))
    ((⇑(Kernel.id ∥ₖ κ) : (a : α × β) → Measure (α × γ)) ∘ₘ μ.prod ν)

Tactic:
ext s hs
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst : SFinite ν
κ : Kernel β γ
inst_1 : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
h :
  ∫⁻ (x : α), (((⇑κ : (a : β) → Measure γ) ∘ₘ ν : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂μ =
    ∫⁻ (a : α × β),
      (((Kernel.id ∥ₖ κ : (a : α × β) → Measure (α × γ)) a : Measure (α × γ)) : (a : Set (α × γ)) → ℝ≥0∞) s ∂μ.prod ν
⊢ Eq (α := ℝ≥0∞) ((μ.prod ((⇑κ : (a : β) → Measure γ) ∘ₘ ν) : (a : Set (α × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (((⇑(Kernel.id ∥ₖ κ) : (a : α × β) → Measure (α × γ)) ∘ₘ μ.prod ν : (a : Set (α × γ)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [Measure.prod_apply hs, Measure.bind_apply hs (Kernel.aemeasurable _)]

Premises used: MeasureTheory.Measure.bind_apply, MeasureTheory.Measure.prod_apply, ProbabilityTheory.Kernel.aemeasurable
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst : SFinite ν
κ : Kernel β γ
inst_1 : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
h :
  ∫⁻ (x : α), ∫⁻ (a : β), (((κ : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂ν ∂μ =
    ∫⁻ (a : α × β),
      (((Kernel.id ∥ₖ κ : (a : α × β) → Measure (α × γ)) a : Measure (α × γ)) : (a : Set (α × γ)) → ℝ≥0∞) s ∂μ.prod ν
⊢ ∫⁻ (x : α), (((⇑κ : (a : β) → Measure γ) ∘ₘ ν : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂μ =
    ∫⁻ (a : α × β),
      (((Kernel.id ∥ₖ κ : (a : α × β) → Measure (α × γ)) a : Measure (α × γ)) : (a : Set (α × γ)) → ℝ≥0∞) s ∂μ.prod ν

Tactic:
simp_rw [Measure.bind_apply (measurable_prodMk_left hs) (Kernel.aemeasurable _)]

Premises used: MeasureTheory.Measure.bind_apply, ProbabilityTheory.Kernel.aemeasurable, measurable_prodMk_left
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst : SFinite ν
κ : Kernel β γ
inst_1 : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
h :
  ∫⁻ (x : α), ∫⁻ (a : β), (((κ : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂ν ∂μ =
    ∫⁻ (x : α),
      ∫⁻ (y : β),
        (((Kernel.id ∥ₖ κ : (a : α × β) → Measure (α × γ)) (x, y) : Measure (α × γ)) : (a : Set (α × γ)) → ℝ≥0∞) s ∂ν ∂μ
h₁ :
  AEMeasurable (β := ℝ≥0∞)
    (fun (a : α × β) ↦
      (((Kernel.id ∥ₖ κ : (a : α × β) → Measure (α × γ)) a : Measure (α × γ)) : (a : Set (α × γ)) → ℝ≥0∞) s)
    (μ.prod ν)
⊢ ∫⁻ (x : α), ∫⁻ (a : β), (((κ : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂ν ∂μ =
    ∫⁻ (a : α × β),
      (((Kernel.id ∥ₖ κ : (a : α × β) → Measure (α × γ)) a : Measure (α × γ)) : (a : Set (α × γ)) → ℝ≥0∞) s ∂μ.prod ν

Tactic:
rw [MeasureTheory.lintegral_prod]

Premises used: MeasureTheory.lintegral_prod
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst : SFinite ν
κ : Kernel β γ
inst_1 : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
⊢ AEMeasurable (β := ℝ≥0∞)
    (fun (a : α × β) ↦
      (((Kernel.id ∥ₖ κ : (a : α × β) → Measure (α × γ)) a : Measure (α × γ)) : (a : Set (α × γ)) → ℝ≥0∞) s)
    (μ.prod ν)

Tactic:
(Kernel.measurable_coe _ hs).aemeasurable

Premises used: Measurable.aemeasurable, ProbabilityTheory.Kernel.measurable_coe
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst : SFinite ν
κ : Kernel β γ
inst_1 : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
⊢ AEMeasurable (β := ℝ≥0∞)
    (fun (a : α × β) ↦
      (((Kernel.id ∥ₖ κ : (a : α × β) → Measure (α × γ)) a : Measure (α × γ)) : (a : Set (α × γ)) → ℝ≥0∞) s)
    (μ.prod ν)

Tactic:
exact (Kernel.measurable_coe _ hs).aemeasurable

Premises used: Measurable.aemeasurable, ProbabilityTheory.Kernel.measurable_coe
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst : SFinite ν
κ : Kernel β γ
inst_1 : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
h :
  ∀ (a : α),
    ∫⁻ (a_1 : β), (((κ : (a : β) → Measure γ) a_1 : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂ν =
      ∫⁻ (y : β),
        (((Kernel.id ∥ₖ κ : (a : α × β) → Measure (α × γ)) (a, y) : Measure (α × γ)) : (a : Set (α × γ)) → ℝ≥0∞) s ∂ν
⊢ ∫⁻ (x : α), ∫⁻ (a : β), (((κ : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂ν ∂μ =
    ∫⁻ (x : α),
      ∫⁻ (y : β),
        (((Kernel.id ∥ₖ κ : (a : α × β) → Measure (α × γ)) (x, y) : Measure (α × γ)) : (a : Set (α × γ)) → ℝ≥0∞) s ∂ν ∂μ

Tactic:
congr with a
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst : SFinite ν
κ : Kernel β γ
inst_1 : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
a : α
h :
  ∀ (b : β),
    Eq (α := ℝ≥0∞) ((((κ : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk a ⁻¹' s) : ℝ≥0∞)
      ((((Kernel.id ∥ₖ κ : (a : α × β) → Measure (α × γ)) (a, b) : Measure (α × γ)) : (a : Set (α × γ)) → ℝ≥0∞) s :
        ℝ≥0∞)
⊢ ∫⁻ (a_1 : β), (((κ : (a : β) → Measure γ) a_1 : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂ν =
    ∫⁻ (y : β),
      (((Kernel.id ∥ₖ κ : (a : α × β) → Measure (α × γ)) (a, y) : Measure (α × γ)) : (a : Set (α × γ)) → ℝ≥0∞) s ∂ν

Tactic:
congr with b