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 γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
f : β × γ → ℝ≥0∞
hf : AEMeasurable (_m := Prod.instMeasurableSpace) f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
A :
  ∫⁻ (z : β × γ), f z ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (z : β × γ), AEMeasurable.mk f hf z ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a
B :
  ∫⁻ (x : β), ∫⁻ (y : γ), f (x, y) ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (x : β),
      ∫⁻ (y : γ), AEMeasurable.mk f hf (x, y) ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a
hf₁ : Measurable (AEMeasurable.mk f hf)
⊢ ∫⁻ (z : β × γ), f z ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (x : β), ∫⁻ (y : γ), f (x, y) ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a

Tactic:
rw [A, B, lintegral_compProd]

Premises used: ProbabilityTheory.Kernel.lintegral_compProd
-- 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 : α
f : β × γ → ℝ≥0∞
hf : AEMeasurable (_m := Prod.instMeasurableSpace) f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
A :
  ∫⁻ (z : β × γ), f z ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (z : β × γ), AEMeasurable.mk f hf z ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a
B :
  ∫⁻ (x : β), ∫⁻ (y : γ), f (x, y) ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (x : β),
      ∫⁻ (y : γ), AEMeasurable.mk f hf (x, y) ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a
⊢ Measurable (AEMeasurable.mk f hf)

Tactic:
hf.measurable_mk

Premises used: AEMeasurable.measurable_mk
-- 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 : α
f : β × γ → ℝ≥0∞
hf : AEMeasurable (_m := Prod.instMeasurableSpace) f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
A :
  ∫⁻ (z : β × γ), f z ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (z : β × γ), AEMeasurable.mk f hf z ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a
B :
  ∫⁻ (x : β), ∫⁻ (y : γ), f (x, y) ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (x : β),
      ∫⁻ (y : γ), AEMeasurable.mk f hf (x, y) ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a
⊢ Measurable (AEMeasurable.mk f hf)

Tactic:
exact hf.measurable_mk

Premises used: AEMeasurable.measurable_mk
-- 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 : α
f : β × γ → ℝ≥0∞
hf : Measurable f
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
simp_rw :
  ∫⁻ (z : β × γ), f z ∂((κ ⊗ₖ η).restrict (s := s ×ˢ t) ⋯ : (a : α) → Measure (β × γ)) a =
    ∫⁻ (x : β) in s, ∫⁻ (y : γ) in t, f (x, y) ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a
simp_rw₁ :
  ∫⁻ (z : β × γ), f z ∂(κ.restrict (s := s) hs ⊗ₖ η.restrict (s := t) ht : (a : α) → Measure (β × γ)) a =
    ∫⁻ (x : β) in s, ∫⁻ (y : γ) in t, f (x, y) ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a
simp_rw₂ :
  ∫⁻ (b : β),
      ∫⁻ (c : γ),
        f
          (b,
            c) ∂(η.restrict (s := t) ht : (a : α × β) → Measure γ)
          (a, b) ∂(κ.restrict (s := s) hs : (a : α) → Measure β) a =
    ∫⁻ (x : β) in s, ∫⁻ (y : γ) in t, f (x, y) ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a
⊢ ∫⁻ (z : β × γ) in s ×ˢ t, f z ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (x : β) in s, ∫⁻ (y : γ) in t, f (x, y) ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a

Tactic:
simp_rw [← Kernel.restrict_apply (κ ⊗ₖ η) (hs.prod ht), ← compProd_restrict hs ht,
    lintegral_compProd _ _ _ hf, Kernel.restrict_apply]

Premises used: ProbabilityTheory.Kernel.restrict_apply, MeasurableSet.prod, ProbabilityTheory.Kernel.compProd_restrict, ProbabilityTheory.Kernel.lintegral_compProd, 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 α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
f : β × γ → ℝ≥0∞
hf : Measurable f
s : Set β
hs : MeasurableSet s
simp_rw :
  ∫⁻ (x : β) in s, ∫⁻ (y : γ) in Set.univ, f (x, y) ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (x : β) in s, ∫⁻ (y : γ), f (x, y) ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a
⊢ ∫⁻ (z : β × γ) in SProd.sprod (β := Set γ) s Set.univ, f z ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (x : β) in s, ∫⁻ (y : γ), f (x, y) ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a

Tactic:
simp_rw [setLIntegral_compProd κ η a hf hs MeasurableSet.univ, Measure.restrict_univ]

Premises used: ProbabilityTheory.Kernel.setLIntegral_compProd, MeasurableSet.univ, MeasureTheory.Measure.restrict_univ
-- 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 : α
f : β × γ → ℝ≥0∞
hf : Measurable f
t : Set γ
ht : MeasurableSet t
simp_rw :
  ∫⁻ (x : β) in Set.univ, ∫⁻ (y : γ) in t, f (x, y) ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (x : β), ∫⁻ (y : γ) in t, f (x, y) ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a
⊢ ∫⁻ (z : β × γ) in SProd.sprod (α := Set β) Set.univ t, f z ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (x : β), ∫⁻ (y : γ) in t, f (x, y) ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a

Tactic:
simp_rw [setLIntegral_compProd κ η a hf MeasurableSet.univ ht, Measure.restrict_univ]

Premises used: ProbabilityTheory.Kernel.setLIntegral_compProd, MeasurableSet.univ, MeasureTheory.Measure.restrict_univ
-- 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 (α × β) γ
simp_rw :
  swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
            deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
          (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ) ∘ₖ
      copy α =
    Kernel.sum fun (n : ℕ) ↦
      swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
              deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
            (Kernel.id ∥ₖ copy β) ∘ₖ
          (Kernel.id ∥ₖ κ.seq n) ∘ₖ
        copy α
⊢ κ ⊗ₖ η = Kernel.sum fun (n : ℕ) ↦ κ.seq n ⊗ₖ η

Tactic:
simp_rw [compProd_def]

Premises used: ProbabilityTheory.Kernel.compProd_def
-- 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 (α × β) γ
rw :
  swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
            deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
          (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ) ∘ₖ
      copy α =
    (Kernel.sum fun (n : ℕ) ↦
        swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
              deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
            (Kernel.id ∥ₖ copy β) ∘ₖ
          (Kernel.id ∥ₖ κ.seq n)) ∘ₖ
      copy α
rw₁ :
  swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
            deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
          (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ) ∘ₖ
      copy α =
    (swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
            deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
          (Kernel.id ∥ₖ copy β) ∘ₖ
        Kernel.sum fun (n : ℕ) ↦ Kernel.id ∥ₖ κ.seq n) ∘ₖ
      copy α
rw₂ :
  swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
            deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
          (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ) ∘ₖ
      copy α =
    swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
            deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
          (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ Kernel.sum κ.seq) ∘ₖ
      copy α
rw₃ rw₄ :
  swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
            deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
          (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ) ∘ₖ
      copy α =
    swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
            deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
          (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ) ∘ₖ
      copy α
⊢ swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
            deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
          (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ) ∘ₖ
      copy α =
    Kernel.sum fun (n : ℕ) ↦
      swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
              deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
            (Kernel.id ∥ₖ copy β) ∘ₖ
          (Kernel.id ∥ₖ κ.seq n) ∘ₖ
        copy α

Tactic:
rw [← comp_sum_left, ← comp_sum_right, ← parallelComp_sum_right, kernel_sum_seq]

Premises used: ProbabilityTheory.Kernel.comp_sum_left, ProbabilityTheory.Kernel.parallelComp_sum_right, ProbabilityTheory.Kernel.kernel_sum_seq, ProbabilityTheory.Kernel.comp_sum_right
-- 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 η
simp_rw :
  swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
            deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
          (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ) ∘ₖ
      copy α =
    Kernel.sum fun (n : ℕ) ↦
      swap γ β ∘ₖ (η.seq n ∥ₖ Kernel.id) ∘ₖ
              deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
            (Kernel.id ∥ₖ copy β) ∘ₖ
          (Kernel.id ∥ₖ κ) ∘ₖ
        copy α
⊢ κ ⊗ₖ η = Kernel.sum fun (n : ℕ) ↦ κ ⊗ₖ η.seq n

Tactic:
simp_rw [compProd_def]

Premises used: ProbabilityTheory.Kernel.compProd_def
-- 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 η
simp_rw : κ ⊗ₖ η = Kernel.sum fun (n : ℕ) ↦ κ.seq n ⊗ₖ η
⊢ κ ⊗ₖ η = Kernel.sum fun (n : ℕ) ↦ Kernel.sum fun (m : ℕ) ↦ κ.seq n ⊗ₖ η.seq m

Tactic:
simp_rw [← compProd_eq_sum_compProd_right, ← compProd_eq_sum_compProd_left]

Premises used: ProbabilityTheory.Kernel.compProd_eq_sum_compProd_left, ProbabilityTheory.Kernel.compProd_eq_sum_compProd_right
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
hs : MeasurableSet s
rw :
  Eq (α := ℝ≥0∞)
    ((((Kernel.sum fun (n : ℕ) ↦ Kernel.sum fun (m : ℕ) ↦ κ.seq n ⊗ₖ η.seq m : (a : α) → Measure (β × γ)) a :
            Measure (β × γ)) :
          (a : Set (β × γ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    (∑' (n : ℕ) (m : ℕ),
        (((κ.seq n ⊗ₖ η.seq m : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (n : ℕ) (m : ℕ),
        (((κ.seq n ⊗ₖ η.seq m : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s :
      ℝ≥0∞)

Tactic:
rw [compProd_eq_sum_compProd]

Premises used: ProbabilityTheory.Kernel.compProd_eq_sum_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 (β × γ)
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    ((((Kernel.sum fun (n : ℕ) ↦ Kernel.sum fun (m : ℕ) ↦ κ.seq n ⊗ₖ η.seq m : (a : α) → Measure (β × γ)) a :
            Measure (β × γ)) :
          (a : Set (β × γ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    (∑' (n : ℕ) (m : ℕ),
        (((κ.seq n ⊗ₖ η.seq m : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s :
      ℝ≥0∞)

Tactic:
simp_rw [sum_apply' _ _ hs]

Premises used: ProbabilityTheory.Kernel.sum_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 (β × γ)
κ : Kernel α β
inst : IsMarkovKernel κ
η : Kernel (α × β) γ
inst_1 : IsMarkovKernel η
a : α
⊢ Eq (α := ℝ≥0∞)
    ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
simp [compProd_apply]

Premises used: ProbabilityTheory.Kernel.compProd_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 (β × γ)
κ : Kernel α β
inst : IsZeroOrMarkovKernel κ
η : Kernel (α × β) γ
inst_1 : IsZeroOrMarkovKernel η
rw :
  IsZeroOrMarkovKernel
    (swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
            deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
          (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ) ∘ₖ
      copy α)
⊢ IsZeroOrMarkovKernel (κ ⊗ₖ η)

Tactic:
rw [compProd_def]

Premises used: ProbabilityTheory.Kernel.compProd_def
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst : IsZeroOrMarkovKernel κ
η : Kernel (α × β) γ
inst_1 : IsZeroOrMarkovKernel η
⊢ IsZeroOrMarkovKernel
    (swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
            deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
          (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ) ∘ₖ
      copy α)

Tactic:
infer_instance
-- 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 : IsFiniteKernel η
a : α
pos :
  ∀ (hκ : IsSFiniteKernel κ),
    (((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) Set.univ ≤
      HMul.hMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) η.bound
neg :
  ∀ (hκ : ¬IsSFiniteKernel κ),
    (((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) Set.univ ≤
      HMul.hMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) η.bound
⊢ (((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) Set.univ ≤
    HMul.hMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) η.bound

Tactic:
by_cases hκ : IsSFiniteKernel κ

Premises used: ProbabilityTheory.IsSFiniteKernel
-- 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 : IsFiniteKernel η
a : α
hκ : ¬IsSFiniteKernel κ
neg :
  (((0 : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) Set.univ ≤
    HMul.hMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) η.bound
⊢ (((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) Set.univ ≤
    HMul.hMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) η.bound

Tactic:
rw [compProd_of_not_isSFiniteKernel_left _ _ hκ]

Premises used: ProbabilityTheory.Kernel.compProd_of_not_isSFiniteKernel_left
-- 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 : IsFiniteKernel η
a : α
hκ : ¬IsSFiniteKernel κ
⊢ (((0 : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) Set.univ ≤
    HMul.hMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) η.bound

Tactic:
simp
-- 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 : IsFiniteKernel η
a : α
hκ : IsSFiniteKernel κ
pos :
  ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' Set.univ) ∂(κ : (a : α) → Measure β) a ≤
    HMul.hMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) η.bound
⊢ (((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) Set.univ ≤
    HMul.hMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) η.bound

Tactic:
rw [compProd_apply .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 : IsFiniteKernel η
a : α
hκ : IsSFiniteKernel κ
Cη : ℝ≥0∞ := η.bound
⊢ ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ ∂(κ : (a : α) → Measure β) a ≤
    ∫⁻ (x : β), Cη ∂(κ : (a : α) → Measure β) a

Tactic:
lintegral_mono fun b => measure_le_bound η (a, b) Set.univ

Premises used: Set.univ, Prod.mk, MeasureTheory.lintegral_mono, ProbabilityTheory.Kernel.measure_le_bound
-- 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 : IsFiniteKernel η
a : α
hκ : IsSFiniteKernel κ
Cη : ℝ≥0∞ := η.bound
⊢ ∫⁻ (x : β), Cη ∂(κ : (a : α) → Measure β) a =
    HMul.hMul (β := ℝ≥0∞) Cη ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞)

Tactic:
MeasureTheory.lintegral_const Cη

Premises used: MeasureTheory.lintegral_const
-- 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 : IsFiniteKernel η
a : α
hκ : IsSFiniteKernel κ
Cη : ℝ≥0∞ := η.bound
⊢ HMul.hMul (β := ℝ≥0∞) Cη ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) Cη

Tactic:
mul_comm _ _

Premises used: mul_comm
-- 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 : IsFiniteKernel η
a : α
hκ : IsSFiniteKernel κ
Cη : ℝ≥0∞ := η.bound
⊢ ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' Set.univ) ∂(κ : (a : α) → Measure β) a ≤
    HMul.hMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) η.bound

Tactic:
calc
    ∫⁻ b, η (a, b) Set.univ ∂κ a ≤ ∫⁻ _, Cη ∂κ a :=
      lintegral_mono fun b => measure_le_bound η (a, b) Set.univ
    _ = Cη * κ a Set.univ := MeasureTheory.lintegral_const Cη
    _ = κ a Set.univ * Cη := mul_comm _ _

Premises used: MeasureTheory.lintegral_const, Set.univ, Prod.mk, MeasureTheory.lintegral_mono, ProbabilityTheory.Kernel.measure_le_bound, mul_comm, DFunLike.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 (β × γ)
κ : Kernel α β
inst : IsFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsFiniteKernel η
rw :
  IsFiniteKernel
    (swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
            deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
          (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ) ∘ₖ
      copy α)
⊢ IsFiniteKernel (κ ⊗ₖ η)

Tactic:
rw [compProd_def]

Premises used: ProbabilityTheory.Kernel.compProd_def
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst : IsFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsFiniteKernel η
⊢ IsFiniteKernel
    (swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
            deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
          (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ) ∘ₖ
      copy α)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
η : Kernel (α × β) γ
rw :
  IsSFiniteKernel
    (swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
            deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
          (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ) ∘ₖ
      copy α)
⊢ IsSFiniteKernel (κ ⊗ₖ η)

Tactic:
rw [compProd_def]

Premises used: ProbabilityTheory.Kernel.compProd_def
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
η : Kernel (α × β) γ
⊢ IsSFiniteKernel
    (swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
            deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
          (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ) ∘ₖ
      copy α)

Tactic:
infer_instance