awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : 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_1 : IsSFiniteKernel η
a : α
⊢ AEMeasurable (α := α × β) (β := Measure (β × γ)) (_m := Prod.instMeasurableSpace)
    (⇑(swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
            deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
          (Kernel.id ∥ₖ copy β)) :
      (a : α × β) → Measure (β × γ))
    (Measure.prod (Measure.dirac (a, a).1) ((κ : (a : α) → Measure β) (a, a).2))

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : 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_1 : IsSFiniteKernel η
a : α
rw :
  ∫⁻ (y : β),
      (((swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
                    deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β)
                      ⋯ ∘ₖ
                  (Kernel.id ∥ₖ copy β) :
                (a : α × β) → Measure (β × γ))
              ((a, a).1, y) :
            Measure (β × γ)) :
          (a : Set (β × γ)) → ℝ≥0∞)
        s ∂(κ : (a : α) → Measure β) (a, a).2 =
    ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a
hf :
  Measurable (β := ℝ≥0∞) fun (x : α) ↦
    ∫⁻ (y : β),
      (((swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
                    deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β)
                      ⋯ ∘ₖ
                  (Kernel.id ∥ₖ copy β) :
                (a : α × β) → Measure (β × γ))
              (x, y) :
            Measure (β × γ)) :
          (a : Set (β × γ)) → ℝ≥0∞)
        s ∂(κ : (a : α) → Measure β) (a, a).2
⊢ (((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s =
    ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a

Tactic:
rw [compProd, comp_apply, copy_apply, Measure.dirac_bind (by fun_prop), comp_apply,
    parallelComp_apply, Kernel.id_apply, Measure.bind_apply hs (by fun_prop),
    lintegral_prod _ (Kernel.measurable_coe _ hs).aemeasurable, lintegral_dirac']

Premises used: MeasureTheory.Measure.bind_apply, MeasureTheory.Measure.dirac_bind, Measurable.aemeasurable, MeasureTheory.lintegral_dirac', ProbabilityTheory.Kernel.copy_apply, ProbabilityTheory.Kernel.comp_apply, MeasureTheory.lintegral_prod, ProbabilityTheory.Kernel.id_apply, ProbabilityTheory.Kernel.measurable_coe, ProbabilityTheory.Kernel.parallelComp_apply, ProbabilityTheory.Kernel.compProd
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : 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_1 : IsSFiniteKernel η
a : α
this :
  Measurable (β := ℝ≥0∞) fun (p : α × β) ↦
    (((swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
                  deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
                (Kernel.id ∥ₖ copy β) :
              (a : α × β) → Measure (β × γ))
            p :
          Measure (β × γ)) :
        (a : Set (β × γ)) → ℝ≥0∞)
      s
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦
    ∫⁻ (y : β),
      (((swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
                    deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β)
                      ⋯ ∘ₖ
                  (Kernel.id ∥ₖ copy β) :
                (a : α × β) → Measure (β × γ))
              (x, y) :
            Measure (β × γ)) :
          (a : Set (β × γ)) → ℝ≥0∞)
        s ∂(κ : (a : α) → Measure β) (a, a).2

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : 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_1 : IsSFiniteKernel η
a : α
hf :
  Measurable (β := ℝ≥0∞) fun (p : α × β) ↦
    (((swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
                  deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
                (Kernel.id ∥ₖ copy β) :
              (a : α × β) → Measure (β × γ))
            p :
          Measure (β × γ)) :
        (a : Set (β × γ)) → ℝ≥0∞)
      s
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦
    ∫⁻ (y : β),
      (((swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
                    deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β)
                      ⋯ ∘ₖ
                  (Kernel.id ∥ₖ copy β) :
                (a : α × β) → Measure (β × γ))
              (x, y) :
            Measure (β × γ)) :
          (a : Set (β × γ)) → ℝ≥0∞)
        s ∂(κ : (a : α) → Measure β) (a, a).2

Tactic:
suffices Measurable fun p : α × β ↦
      (swap γ β ∘ₖ (η ∥ₖ Kernel.id)
        ∘ₖ deterministic MeasurableEquiv.prodAssoc.symm (MeasurableEquiv.measurable _)
        ∘ₖ (Kernel.id ∥ₖ copy β)) p s by fun_prop
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : 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_1 : IsSFiniteKernel η
a : α
⊢ Measurable (β := ℝ≥0∞) fun (p : α × β) ↦
    (((swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
                  deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
                (Kernel.id ∥ₖ copy β) :
              (a : α × β) → Measure (β × γ))
            p :
          Measure (β × γ)) :
        (a : Set (β × γ)) → ℝ≥0∞)
      s

Tactic:
Kernel.measurable_coe _ hs

Premises used: ProbabilityTheory.Kernel.measurable_coe
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : 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_1 : IsSFiniteKernel η
a : α
⊢ Measurable (β := ℝ≥0∞) fun (p : α × β) ↦
    (((swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
                  deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
                (Kernel.id ∥ₖ copy β) :
              (a : α × β) → Measure (β × γ))
            p :
          Measure (β × γ)) :
        (a : Set (β × γ)) → ℝ≥0∞)
      s

Tactic:
exact Kernel.measurable_coe _ hs

Premises used: ProbabilityTheory.Kernel.measurable_coe
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : 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_1 : IsSFiniteKernel η
a : α
e_f :
  ∀ (b : β),
    Eq (α := ℝ≥0∞)
      ((((swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
                      deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β)
                        ⋯ ∘ₖ
                    (Kernel.id ∥ₖ copy β) :
                  (a : α × β) → Measure (β × γ))
                ((a, a).1, b) :
              Measure (β × γ)) :
            (a : Set (β × γ)) → ℝ≥0∞)
          s :
        ℝ≥0∞)
      ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) : ℝ≥0∞)
⊢ ∫⁻ (y : β),
      (((swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
                    deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β)
                      ⋯ ∘ₖ
                  (Kernel.id ∥ₖ copy β) :
                (a : α × β) → Measure (β × γ))
              ((a, a).1, y) :
            Measure (β × γ)) :
          (a : Set (β × γ)) → ℝ≥0∞)
        s ∂(κ : (a : α) → Measure β) (a, a).2 =
    ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a

Tactic:
congr with b
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : 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_1 : IsSFiniteKernel η
a : α
b : β
⊢ Measurable (α := Prod.{u_1, u_2} α (β × β)) (β := Measure (β × γ))
    (⇑(swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
          deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯) :
      (a : α × β × β) → Measure (β × γ))

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : 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_1 : IsSFiniteKernel η
a : α
b : β
⊢ Measurable (α := Prod.{u_1, u_2} α (β × β)) (β := (α × β) × β)
    (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : 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_1 : IsSFiniteKernel η
a : α
b : β
⊢ Measurable (α := (α × β) × β) (β := Measure (β × γ))
    (⇑(swap γ β ∘ₖ (η ∥ₖ Kernel.id)) : (a : (α × β) × β) → Measure (β × γ))

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : 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_1 : IsSFiniteKernel η
a : α
b : β
e_f :
  Eq (α := ℝ≥0∞)
    ((Measure.bind (α := γ × β) (mα := Prod.instMeasurableSpace)
            ((η ∥ₖ Kernel.id : (a : (α × β) × β) → Measure (γ × β))
              ((MeasurableEquiv.symm MeasurableEquiv.prodAssoc : (a : α × β × β) → (α × β) × β)
                (((a, a).1, b).1, ((a, a).1, b).2, ((a, a).1, b).2)))
            (⇑(swap γ β) : (a : γ × β) → Measure (β × γ)) :
          (a : Set (β × γ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
                    deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β)
                      ⋯ ∘ₖ
                  (Kernel.id ∥ₖ copy β) :
                (a : α × β) → Measure (β × γ))
              ((a, a).1, b) :
            Measure (β × γ)) :
          (a : Set (β × γ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) : ℝ≥0∞)

Tactic:
rw [comp_apply, parallelComp_apply, Kernel.id_apply, copy_apply, Measure.dirac_prod_dirac,
    Measure.dirac_bind (by fun_prop), comp_apply, deterministic_apply (by fun_prop),
    Measure.dirac_bind (by fun_prop), comp_apply]

Premises used: MeasureTheory.Measure.dirac_bind, ProbabilityTheory.Kernel.deterministic_apply, ProbabilityTheory.Kernel.copy_apply, ProbabilityTheory.Kernel.comp_apply, MeasureTheory.Measure.dirac_prod_dirac, ProbabilityTheory.Kernel.id_apply, ProbabilityTheory.Kernel.parallelComp_apply
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : 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_1 : IsSFiniteKernel η
a : α
b : β
e_f :
  Eq (α := ℝ≥0∞)
    ((Measure.bind (α := γ × β) (mα := Prod.instMeasurableSpace)
            ((η ∥ₖ Kernel.id : (a : (α × β) × β) → Measure (γ × β)) ((a, b), b))
            (⇑(swap γ β) : (a : γ × β) → Measure (β × γ)) :
          (a : Set (β × γ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((Measure.bind (α := γ × β) (mα := Prod.instMeasurableSpace)
            ((η ∥ₖ Kernel.id : (a : (α × β) × β) → Measure (γ × β))
              ((MeasurableEquiv.symm MeasurableEquiv.prodAssoc : (a : α × β × β) → (α × β) × β)
                (((a, a).1, b).1, ((a, a).1, b).2, ((a, a).1, b).2)))
            (⇑(swap γ β) : (a : γ × β) → Measure (β × γ)) :
          (a : Set (β × γ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) : ℝ≥0∞)

Tactic:
simp only [MeasurableEquiv.prodAssoc, MeasurableEquiv.symm_mk, MeasurableEquiv.coe_mk,
    Equiv.prodAssoc_symm_apply]

Premises used: MeasurableEquiv.coe_mk, MeasurableEquiv.prodAssoc, Equiv.prodAssoc_symm_apply, MeasurableEquiv.symm_mk
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : 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_1 : IsSFiniteKernel η
a : α
b : β
⊢ AEMeasurable (α := γ × β) (β := Measure (β × γ)) (_m := Prod.instMeasurableSpace)
    (⇑(swap γ β) : (a : γ × β) → Measure (β × γ))
    (Measure.prod ((η : (a : α × β) → Measure γ) ((a, b), b).1) (Measure.dirac ((a, b), b).2))

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : 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_1 : IsSFiniteKernel η
a : α
b : β
e_f :
  ∫⁻ (x : γ),
      ∫⁻ (y : β),
        (((swap γ β : (a : γ × β) → Measure (β × γ)) (x, y) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
          s ∂Measure.dirac ((a, b), b).2 ∂(η : (a : α × β) → Measure γ) ((a, b), b).1 =
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)
⊢ Eq (α := ℝ≥0∞)
    ((Measure.bind (α := γ × β) (mα := Prod.instMeasurableSpace)
            ((η ∥ₖ Kernel.id : (a : (α × β) × β) → Measure (γ × β)) ((a, b), b))
            (⇑(swap γ β) : (a : γ × β) → Measure (β × γ)) :
          (a : Set (β × γ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) : ℝ≥0∞)

Tactic:
rw [parallelComp_apply, Kernel.id_apply, Measure.bind_apply hs (by fun_prop),
    lintegral_prod _ (Kernel.measurable_coe _ hs).aemeasurable]

Premises used: MeasureTheory.Measure.bind_apply, Measurable.aemeasurable, MeasureTheory.lintegral_prod, ProbabilityTheory.Kernel.id_apply, ProbabilityTheory.Kernel.measurable_coe, ProbabilityTheory.Kernel.parallelComp_apply
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : 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_1 : IsSFiniteKernel η
a : α
b : β
x : γ
rw :
  Eq (α := ℝ≥0∞)
    ((((swap γ β : (a : γ × β) → Measure (β × γ)) (x, b) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((Prod.mk b ⁻¹' s).indicator 1 x : ℝ≥0∞)
hf :
  Measurable (β := ℝ≥0∞) fun (y : β) ↦
    (((swap γ β : (a : γ × β) → Measure (β × γ)) (x, y) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s
⊢ ∫⁻ (y : β),
      (((swap γ β : (a : γ × β) → Measure (β × γ)) (x, y) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
        s ∂Measure.dirac b =
    (Prod.mk b ⁻¹' s).indicator 1 x

Tactic:
rw [lintegral_dirac']

Premises used: MeasureTheory.lintegral_dirac'
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : 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_1 : IsSFiniteKernel η
a : α
b : β
x : γ
⊢ Eq (α := ℝ≥0∞)
    ((((swap γ β : (a : γ × β) → Measure (β × γ)) (x, b) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((Prod.mk b ⁻¹' s).indicator 1 x : ℝ≥0∞)

Tactic:
simp [swap_apply' _ hs, Set.indicator_apply]

Premises used: Set.indicator_apply, ProbabilityTheory.Kernel.swap_apply'
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : 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_1 : IsSFiniteKernel η
a : α
b : β
x : γ
⊢ Measurable (β := ℝ≥0∞) fun (y : β) ↦
    (((swap γ β : (a : γ × β) → Measure (β × γ)) (x, y) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s

Tactic:
simpa [swap_apply' _ hs, Prod.swap_prod_mk] using
        measurable_const.indicator (measurable_prodMk_right hs)

Premises used: Measurable.indicator, measurable_prodMk_right, Prod.swap_prod_mk, measurable_const, ProbabilityTheory.Kernel.swap_apply'
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : 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_1 : IsSFiniteKernel η
a : α
b : β
⊢ ∀ (x : γ),
    ∫⁻ (y : β),
        (((swap γ β : (a : γ × β) → Measure (β × γ)) (x, y) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
          s ∂Measure.dirac b =
      (Prod.mk b ⁻¹' s).indicator 1 x

Tactic:
have h_int x : ∫⁻ y, swap γ β (x, y) s ∂Measure.dirac b = (Prod.mk b ⁻¹' s).indicator 1 x := by
    rw [lintegral_dirac']
    · simp [swap_apply' _ hs, Set.indicator_apply]
    · simpa [swap_apply' _ hs, Prod.swap_prod_mk] using
        measurable_const.indicator (measurable_prodMk_right hs)
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : 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_1 : IsSFiniteKernel η
a : α
b : β
h_int :
  ∀ (x : γ),
    ∫⁻ (y : β),
        (((swap γ β : (a : γ × β) → Measure (β × γ)) (x, y) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
          s ∂Measure.dirac b =
      (Prod.mk b ⁻¹' s).indicator 1 x
e_f :
  ∫⁻ (x : γ), (Prod.mk b ⁻¹' s).indicator 1 x ∂(η : (a : α × β) → Measure γ) (a, b) =
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)
⊢ ∫⁻ (x : γ),
      ∫⁻ (y : β),
        (((swap γ β : (a : γ × β) → Measure (β × γ)) (x, y) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
          s ∂Measure.dirac ((a, b), b).2 ∂(η : (a : α × β) → Measure γ) ((a, b), b).1 =
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)

Tactic:
simp_rw [h_int]
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : 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_1 : IsSFiniteKernel η
a : α
b : β
h_int :
  ∀ (x : γ),
    ∫⁻ (y : β),
        (((swap γ β : (a : γ × β) → Measure (β × γ)) (x, y) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
          s ∂Measure.dirac b =
      (Prod.mk b ⁻¹' s).indicator 1 x
e_f : MeasurableSet (Prod.mk b ⁻¹' s)
⊢ ∫⁻ (x : γ), (Prod.mk b ⁻¹' s).indicator 1 x ∂(η : (a : α × β) → Measure γ) (a, b) =
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)

Tactic:
rw [lintegral_indicator_one]

Premises used: MeasureTheory.lintegral_indicator_one
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : 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_1 : IsSFiniteKernel η
a : α
b : β
h_int :
  ∀ (x : γ),
    ∫⁻ (y : β),
        (((swap γ β : (a : γ × β) → Measure (β × γ)) (x, y) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
          s ∂Measure.dirac b =
      (Prod.mk b ⁻¹' s).indicator 1 x
⊢ MeasurableSet (Prod.mk b ⁻¹' s)

Tactic:
measurable_prodMk_left hs

Premises used: measurable_prodMk_left
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : 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_1 : IsSFiniteKernel η
a : α
b : β
h_int :
  ∀ (x : γ),
    ∫⁻ (y : β),
        (((swap γ β : (a : γ × β) → Measure (β × γ)) (x, y) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
          s ∂Measure.dirac b =
      (Prod.mk b ⁻¹' s).indicator 1 x
⊢ MeasurableSet (Prod.mk b ⁻¹' s)

Tactic:
exact measurable_prodMk_left hs

Premises used: measurable_prodMk_left
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
s : Set (β × γ)
⊢ ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        {c : γ | (b, c) ∈ s} ∂(κ : (a : α) → Measure β) a ≤
    (((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s

Tactic:
calc
    ∫⁻ b, η (a, b) {c | (b, c) ∈ s} ∂κ a ≤
        ∫⁻ b, η (a, b) {c | (b, c) ∈ toMeasurable ((κ ⊗ₖ η) a) s} ∂κ a :=
      lintegral_mono fun _ => measure_mono fun _ h_mem => subset_toMeasurable _ _ h_mem
    _ = (κ ⊗ₖ η) a (toMeasurable ((κ ⊗ₖ η) a) s) :=
      (compProd_apply (measurableSet_toMeasurable _ _) κ η a).symm
    _ = (κ ⊗ₖ η) a s := measure_toMeasurable s

Premises used: Trans.trans, MeasureTheory.subset_toMeasurable, MeasureTheory.measure_toMeasurable, MeasureTheory.measurableSet_toMeasurable, MeasureTheory.lintegral_mono, MeasureTheory.measure_mono, ProbabilityTheory.Kernel.compProd_apply, Eq.symm, DFunLike.coe, ProbabilityTheory.Kernel.compProd
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsMarkovKernel η
a : α
rw :
  ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' Set.univ) ∂(κ : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ
⊢ Eq (α := ℝ≥0∞)
    ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞)

Tactic:
rw [compProd_apply MeasurableSet.univ]

Premises used: ProbabilityTheory.Kernel.compProd_apply, MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsMarkovKernel η
a : α
⊢ ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' Set.univ) ∂(κ : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ

Tactic:
simp