awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ_1 : Kernel α β
η_1 : Kernel γ δ
x : α × γ
κ : Kernel α β
η : Kernel γ δ
h : IsSFiniteKernel κ ∧ IsSFiniteKernel η
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set (β × δ)
hs : MeasurableSet s
refine :
  Measurable (β := ℝ≥0∞) fun (y : (α × γ) × β) ↦
    (((prodMkLeft α η : (a : α × γ) → Measure δ) y.1 : Measure δ) : (a : Set δ) → ℝ≥0∞) (Prod.mk y.2 ⁻¹' s)
⊢ Measurable (β := ℝ≥0∞) fun (b : α × γ) ↦
    ∫⁻ (x : β),
      (((η : (a : γ) → Measure δ) b.2 : Measure δ) : (a : Set δ) → ℝ≥0∞)
        (Prod.mk x ⁻¹' s) ∂(κ : (a : α) → Measure β) b.1

Tactic:
refine Measurable.lintegral_kernel_prod_right'
        (f := fun y ↦ prodMkLeft α η y.1 (Prod.mk y.2 ⁻¹' s)) (κ := prodMkRight γ κ) ?_

Premises used: Measurable.lintegral_kernel_prod_right'
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ_1 : Kernel α β
η_1 : Kernel γ δ
x : α × γ
κ : Kernel α β
η : Kernel γ δ
h : IsSFiniteKernel κ ∧ IsSFiniteKernel η
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set (β × δ)
hs : MeasurableSet s
⊢ Eq (α := (y : (α × γ) × β) → ℝ≥0∞)
    (fun (y : (α × γ) × β) ↦
      (((prodMkLeft α η : (a : α × γ) → Measure δ) y.1 : Measure δ) : (a : Set δ) → ℝ≥0∞) (Prod.mk y.2 ⁻¹' s))
    fun (y : (α × γ) × β) ↦
    (((prodMkRight β (prodMkLeft α η) : (a : (α × γ) × β) → Measure δ) y : Measure δ) : (a : Set δ) → ℝ≥0∞)
      (Prod.mk y.2 ⁻¹' s)

Tactic:
have : (fun y ↦ prodMkLeft α η y.1 (Prod.mk y.2 ⁻¹' s))
          = fun y ↦ prodMkRight β (prodMkLeft α η) y (Prod.mk y.2 ⁻¹' s) := rfl
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ_1 : Kernel α β
η_1 : Kernel γ δ
x : α × γ
κ : Kernel α β
η : Kernel γ δ
h : IsSFiniteKernel κ ∧ IsSFiniteKernel η
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set (β × δ)
hs : MeasurableSet s
this :
  Eq (α := (y : (α × γ) × β) → ℝ≥0∞)
    (fun (y : (α × γ) × β) ↦
      (((prodMkLeft α η : (a : α × γ) → Measure δ) y.1 : Measure δ) : (a : Set δ) → ℝ≥0∞) (Prod.mk y.2 ⁻¹' s))
    fun (y : (α × γ) × β) ↦
    (((prodMkRight β (prodMkLeft α η) : (a : (α × γ) × β) → Measure δ) y : Measure δ) : (a : Set δ) → ℝ≥0∞)
      (Prod.mk y.2 ⁻¹' s)
rw :
  Measurable (β := ℝ≥0∞) fun (y : (α × γ) × β) ↦
    (((prodMkRight β (prodMkLeft α η) : (a : (α × γ) × β) → Measure δ) y : Measure δ) : (a : Set δ) → ℝ≥0∞)
      (Prod.mk y.2 ⁻¹' s)
⊢ Measurable (β := ℝ≥0∞) fun (y : (α × γ) × β) ↦
    (((prodMkLeft α η : (a : α × γ) → Measure δ) y.1 : Measure δ) : (a : Set δ) → ℝ≥0∞) (Prod.mk y.2 ⁻¹' s)

Tactic:
rw [this]
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ_1 : Kernel α β
η_1 : Kernel γ δ
x : α × γ
κ : Kernel α β
η : Kernel γ δ
h : IsSFiniteKernel κ ∧ IsSFiniteKernel η
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set (β × δ)
hs : MeasurableSet s
this :
  Eq (α := (y : (α × γ) × β) → ℝ≥0∞)
    (fun (y : (α × γ) × β) ↦
      (((prodMkLeft α η : (a : α × γ) → Measure δ) y.1 : Measure δ) : (a : Set δ) → ℝ≥0∞) (Prod.mk y.2 ⁻¹' s))
    fun (y : (α × γ) × β) ↦
    (((prodMkRight β (prodMkLeft α η) : (a : (α × γ) × β) → Measure δ) y : Measure δ) : (a : Set δ) → ℝ≥0∞)
      (Prod.mk y.2 ⁻¹' s)
⊢ Measurable (β := ℝ≥0∞) fun (y : (α × γ) × β) ↦
    (((prodMkRight β (prodMkLeft α η) : (a : (α × γ) × β) → Measure δ) y : Measure δ) : (a : Set δ) → ℝ≥0∞)
      (Prod.mk y.2 ⁻¹' s)

Tactic:
measurable_kernel_prodMk_left (measurable_fst.snd.prodMk measurable_snd hs)

Premises used: Set.Mem, setOf, Measurable.prodMk, Set.preimage, measurable_snd, ProbabilityTheory.Kernel.measurable_kernel_prodMk_left, measurable_fst, Measurable.snd
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ_1 : Kernel α β
η_1 : Kernel γ δ
x : α × γ
κ : Kernel α β
η : Kernel γ δ
h : IsSFiniteKernel κ ∧ IsSFiniteKernel η
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set (β × δ)
hs : MeasurableSet s
this :
  Eq (α := (y : (α × γ) × β) → ℝ≥0∞)
    (fun (y : (α × γ) × β) ↦
      (((prodMkLeft α η : (a : α × γ) → Measure δ) y.1 : Measure δ) : (a : Set δ) → ℝ≥0∞) (Prod.mk y.2 ⁻¹' s))
    fun (y : (α × γ) × β) ↦
    (((prodMkRight β (prodMkLeft α η) : (a : (α × γ) × β) → Measure δ) y : Measure δ) : (a : Set δ) → ℝ≥0∞)
      (Prod.mk y.2 ⁻¹' s)
⊢ Measurable (β := ℝ≥0∞) fun (y : (α × γ) × β) ↦
    (((prodMkRight β (prodMkLeft α η) : (a : (α × γ) × β) → Measure δ) y : Measure δ) : (a : Set δ) → ℝ≥0∞)
      (Prod.mk y.2 ⁻¹' s)

Tactic:
exact measurable_kernel_prodMk_left (measurable_fst.snd.prodMk measurable_snd hs)

Premises used: Measurable.prodMk, measurable_snd, ProbabilityTheory.Kernel.measurable_kernel_prodMk_left, measurable_fst, Measurable.snd
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
h : ¬IsSFiniteKernel κ
rw :
  Eq (α := Kernel (α × γ) (β × δ))
    (if h : IsSFiniteKernel κ ∧ IsSFiniteKernel η then
      { toFun := fun (x : α × γ) ↦ Measure.prod ((κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2),
        measurable' := ⋯ }
    else 0)
    0
rw₁ rw₂ : Eq (α := Kernel (α × γ) (β × δ)) 0 0
⊢ κ ∥ₖ η = 0

Tactic:
rw [parallelComp, dif_neg (not_and_of_not_left _ h)]

Premises used: not_and_of_not_left, dif_neg, ProbabilityTheory.Kernel.parallelComp
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
η : Kernel γ δ
κ : Kernel α β
h : ¬IsSFiniteKernel η
rw :
  Eq (α := Kernel (α × γ) (β × δ))
    (if h : IsSFiniteKernel κ ∧ IsSFiniteKernel η then
      { toFun := fun (x : α × γ) ↦ Measure.prod ((κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2),
        measurable' := ⋯ }
    else 0)
    0
rw₁ rw₂ : Eq (α := Kernel (α × γ) (β × δ)) 0 0
⊢ κ ∥ₖ η = 0

Tactic:
rw [parallelComp, dif_neg (not_and_of_not_right _ h)]

Premises used: dif_neg, not_and_of_not_right, ProbabilityTheory.Kernel.parallelComp
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel γ δ
inst_1 : IsSFiniteKernel η
x : α × γ
rw :
  Eq (α := Measure (β × δ))
    ((if h : IsSFiniteKernel κ ∧ IsSFiniteKernel η then
            { toFun := fun (x : α × γ) ↦ Measure.prod ((κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2),
              measurable' := ⋯ }
          else 0 :
          (a : α × γ) → Measure (β × δ))
        x :
      Measure (β × δ))
    (Measure.prod ((κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2) : Measure (β × δ))
rw₁ :
  Eq (α := Measure (β × δ))
    (({ toFun := fun (x : α × γ) ↦ Measure.prod ((κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2),
            measurable' := ⋯ : Kernel (α × γ) (β × δ) } :
          (a : α × γ) → Measure (β × δ))
        x :
      Measure (β × δ))
    (Measure.prod ((κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2) : Measure (β × δ))
rw₂ rw₃ :
  Eq (α := Measure (β × δ)) (Measure.prod ((κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2))
    (Measure.prod ((κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2))
⊢ Eq (α := Measure (β × δ)) ((κ ∥ₖ η : (a : α × γ) → Measure (β × δ)) x : Measure (β × δ))
    (Measure.prod ((κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2) : Measure (β × δ))

Tactic:
rw [parallelComp, dif_pos ⟨inferInstance, inferInstance⟩, coe_mk]

Premises used: dif_pos, ProbabilityTheory.Kernel.coe_mk, ProbabilityTheory.Kernel.parallelComp
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
x : α × γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
s : Set (β × δ)
hs : MeasurableSet s
rw :
  (Measure.prod ((κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2) : (a : Set (β × δ)) → ℝ≥0∞) s =
    ∫⁻ (b : β),
      (((η : (a : γ) → Measure δ) x.2 : Measure δ) : (a : Set δ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) x.1
rw₁ rw₂ :
  ∫⁻ (x_1 : β),
      (((η : (a : γ) → Measure δ) x.2 : Measure δ) : (a : Set δ) → ℝ≥0∞)
        (Prod.mk x_1 ⁻¹' s) ∂(κ : (a : α) → Measure β) x.1 =
    ∫⁻ (b : β),
      (((η : (a : γ) → Measure δ) x.2 : Measure δ) : (a : Set δ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) x.1
⊢ (((κ ∥ₖ η : (a : α × γ) → Measure (β × δ)) x : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) s =
    ∫⁻ (b : β),
      (((η : (a : γ) → Measure δ) x.2 : Measure δ) : (a : Set δ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) x.1

Tactic:
rw [parallelComp_apply, Measure.prod_apply hs]

Premises used: MeasureTheory.Measure.prod_apply, ProbabilityTheory.Kernel.parallelComp_apply
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
x : α × γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
s : Set β
t : Set δ
rw :
  (Measure.prod ((κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2) : (a : Set (β × δ)) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure β) x.1 : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((((η : (a : γ) → Measure δ) x.2 : Measure δ) : (a : Set δ) → ℝ≥0∞) t : ℝ≥0∞)
rw₁ rw₂ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure β) x.1 : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((((η : (a : γ) → Measure δ) x.2 : Measure δ) : (a : Set δ) → ℝ≥0∞) t : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure β) x.1 : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((((η : (a : γ) → Measure δ) x.2 : Measure δ) : (a : Set δ) → ℝ≥0∞) t : ℝ≥0∞)
⊢ (((κ ∥ₖ η : (a : α × γ) → Measure (β × δ)) x : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure β) x.1 : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((((η : (a : γ) → Measure δ) x.2 : Measure δ) : (a : Set δ) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rw [parallelComp_apply, Measure.prod_prod]

Premises used: MeasureTheory.Measure.prod_prod, ProbabilityTheory.Kernel.parallelComp_apply
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
x : α × γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
rw :
  ∫⁻ (x_1 : β),
      (((η : (a : γ) → Measure δ) x.2 : Measure δ) : (a : Set δ) → ℝ≥0∞)
        (Prod.mk x_1 ⁻¹' Set.univ) ∂(κ : (a : α) → Measure β) x.1 =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((η : (a : γ) → Measure δ) x.2 : Measure δ) : (a : Set δ) → ℝ≥0∞) Set.univ : ℝ≥0∞)
      ((((κ : (a : α) → Measure β) x.1 : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞)
⊢ (((κ ∥ₖ η : (a : α × γ) → Measure (β × δ)) x : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) Set.univ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : α) → Measure β) x.1 : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞)
      ((((η : (a : γ) → Measure δ) x.2 : Measure δ) : (a : Set δ) → ℝ≥0∞) Set.univ : ℝ≥0∞)

Tactic:
rw [parallelComp_apply, Measure.prod_apply .univ, mul_comm]

Premises used: MeasureTheory.Measure.prod_apply, mul_comm, ProbabilityTheory.Kernel.parallelComp_apply, MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
x : α × γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
⊢ ∫⁻ (x_1 : β),
      (((η : (a : γ) → Measure δ) x.2 : Measure δ) : (a : Set δ) → ℝ≥0∞)
        (Prod.mk x_1 ⁻¹' Set.univ) ∂(κ : (a : α) → Measure β) x.1 =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((η : (a : γ) → Measure δ) x.2 : Measure δ) : (a : Set δ) → ℝ≥0∞) Set.univ : ℝ≥0∞)
      ((((κ : (a : α) → Measure β) x.1 : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
η : Kernel γ δ
pos : ∀ (h : IsSFiniteKernel η), Eq (α := Kernel (α × γ) (β × δ)) (0 ∥ₖ η) 0
neg : ∀ (h : ¬IsSFiniteKernel η), Eq (α := Kernel (α × γ) (β × δ)) (0 ∥ₖ η) 0
⊢ Eq (α := Kernel (α × γ) (β × δ)) (0 ∥ₖ η) 0

Tactic:
by_cases h : IsSFiniteKernel η

Premises used: ProbabilityTheory.IsSFiniteKernel
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
η : Kernel γ δ
h : IsSFiniteKernel η
pos :
  ∀ (a : α × γ) (s : Set (β × δ)),
    MeasurableSet s →
      Eq (α := ℝ≥0∞)
        ((((0 ∥ₖ η : (a : α × γ) → Measure (β × δ)) a : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) s : ℝ≥0∞)
        ((((0 : (a : α × γ) → Measure (β × δ)) a : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := Kernel (α × γ) (β × δ)) (0 ∥ₖ η) 0

Tactic:
ext
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
η : Kernel γ δ
h : IsSFiniteKernel η
a : α × γ
s : Set (β × δ)
h_1 : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((0 ∥ₖ η : (a : α × γ) → Measure (β × δ)) a : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((0 : (a : α × γ) → Measure (β × δ)) a : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [parallelComp_apply]

Premises used: ProbabilityTheory.Kernel.parallelComp_apply
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
η : Kernel γ δ
h : ¬IsSFiniteKernel η
⊢ Eq (α := Kernel (α × γ) (β × δ)) (0 ∥ₖ η) 0

Tactic:
parallelComp_of_not_isSFiniteKernel_right _ h

Premises used: ProbabilityTheory.Kernel.parallelComp_of_not_isSFiniteKernel_right
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
η : Kernel γ δ
h : ¬IsSFiniteKernel η
⊢ Eq (α := Kernel (α × γ) (β × δ)) (0 ∥ₖ η) 0

Tactic:
exact parallelComp_of_not_isSFiniteKernel_right _ h

Premises used: ProbabilityTheory.Kernel.parallelComp_of_not_isSFiniteKernel_right
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
pos : ∀ (h : IsSFiniteKernel κ), Eq (α := Kernel (α × γ) (β × δ)) (κ ∥ₖ 0) 0
neg : ∀ (h : ¬IsSFiniteKernel κ), Eq (α := Kernel (α × γ) (β × δ)) (κ ∥ₖ 0) 0
⊢ Eq (α := Kernel (α × γ) (β × δ)) (κ ∥ₖ 0) 0

Tactic:
by_cases h : IsSFiniteKernel κ

Premises used: ProbabilityTheory.IsSFiniteKernel
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
h : IsSFiniteKernel κ
pos :
  ∀ (a : α × γ) (s : Set (β × δ)),
    MeasurableSet s →
      Eq (α := ℝ≥0∞)
        ((((κ ∥ₖ 0 : (a : α × γ) → Measure (β × δ)) a : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) s : ℝ≥0∞)
        ((((0 : (a : α × γ) → Measure (β × δ)) a : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := Kernel (α × γ) (β × δ)) (κ ∥ₖ 0) 0

Tactic:
ext
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
h : IsSFiniteKernel κ
a : α × γ
s : Set (β × δ)
h_1 : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((κ ∥ₖ 0 : (a : α × γ) → Measure (β × δ)) a : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((0 : (a : α × γ) → Measure (β × δ)) a : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [parallelComp_apply]

Premises used: ProbabilityTheory.Kernel.parallelComp_apply
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
h : ¬IsSFiniteKernel κ
⊢ Eq (α := Kernel (α × γ) (β × δ)) (κ ∥ₖ 0) 0

Tactic:
parallelComp_of_not_isSFiniteKernel_left _ h

Premises used: ProbabilityTheory.Kernel.parallelComp_of_not_isSFiniteKernel_left
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
h : ¬IsSFiniteKernel κ
⊢ Eq (α := Kernel (α × γ) (β × δ)) (κ ∥ₖ 0) 0

Tactic:
exact parallelComp_of_not_isSFiniteKernel_left _ h

Premises used: ProbabilityTheory.Kernel.parallelComp_of_not_isSFiniteKernel_left
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
h :
  ∀ (a : α × β),
    Eq (α := Measure (α × β)) ((Kernel.id ∥ₖ Kernel.id : (a : α × β) → Measure (α × β)) a : Measure (α × β))
      ((Kernel.id : (a : α × β) → Measure (α × β)) a : Measure (α × β))
⊢ Eq (α := Kernel (α × β) (α × β)) (Kernel.id ∥ₖ Kernel.id) Kernel.id

Tactic:
ext : 1
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
a : α × β
⊢ Eq (α := Measure (α × β)) ((Kernel.id ∥ₖ Kernel.id : (a : α × β) → Measure (α × β)) a : Measure (α × β))
    ((Kernel.id : (a : α × β) → Measure (α × β)) a : Measure (α × β))

Tactic:
simp [parallelComp_apply, id_apply, Measure.dirac_prod_dirac]

Premises used: MeasureTheory.Measure.dirac_prod_dirac, ProbabilityTheory.Kernel.id_apply, ProbabilityTheory.Kernel.parallelComp_apply
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → γ
g : β → δ
hf : Measurable f
hg : Measurable g
h :
  ∀ (x : α × β),
    Eq (α := Measure (γ × δ))
      ((deterministic f hf ∥ₖ deterministic g hg : (a : α × β) → Measure (γ × δ)) x : Measure (γ × δ))
      ((deterministic (Prod.map f g) ⋯ : (a : α × β) → Measure (γ × δ)) x : Measure (γ × δ))
⊢ deterministic f hf ∥ₖ deterministic g hg = deterministic (Prod.map f g) ⋯

Tactic:
ext x : 1
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → γ
g : β → δ
hf : Measurable f
hg : Measurable g
x : α × β
h :
  Eq (α := Measure (γ × δ))
    (Measure.prod ((deterministic f hf : (a : α) → Measure γ) x.1) ((deterministic g hg : (a : β) → Measure δ) x.2))
    ((deterministic (Prod.map f g) ⋯ : (a : α × β) → Measure (γ × δ)) x)
h₁ :
  Eq (α := Measure (γ × δ)) (Measure.prod (Measure.dirac (f x.1)) (Measure.dirac (g x.2)))
    (Measure.dirac (Prod.map f g x))
h₂ :
  Eq (α := Measure (γ × δ)) (Measure.prod (Measure.dirac (f x.1)) (Measure.dirac (g x.2)))
    (Measure.dirac (f x.1, g x.2))
⊢ Eq (α := Measure (γ × δ))
    ((deterministic f hf ∥ₖ deterministic g hg : (a : α × β) → Measure (γ × δ)) x : Measure (γ × δ))
    ((deterministic (Prod.map f g) ⋯ : (a : α × β) → Measure (γ × δ)) x : Measure (γ × δ))

Tactic:
simp_rw [parallelComp_apply, deterministic_apply, Prod.map, Measure.dirac_prod_dirac]

Premises used: ProbabilityTheory.Kernel.deterministic_apply, Prod.map, MeasureTheory.Measure.dirac_prod_dirac, ProbabilityTheory.Kernel.parallelComp_apply
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
ac : α × γ
g : β × δ → ℝ≥0∞
hg : Measurable g
rw :
  ∫⁻ (bd : β × δ), g bd ∂Measure.prod ((κ : (a : α) → Measure β) ac.1) ((η : (a : γ) → Measure δ) ac.2) =
    ∫⁻ (b : β), ∫⁻ (d : δ), g (b, d) ∂(η : (a : γ) → Measure δ) ac.2 ∂(κ : (a : α) → Measure β) ac.1
rw₁ rw₂ :
  ∫⁻ (x : β), ∫⁻ (y : δ), g (x, y) ∂(η : (a : γ) → Measure δ) ac.2 ∂(κ : (a : α) → Measure β) ac.1 =
    ∫⁻ (b : β), ∫⁻ (d : δ), g (b, d) ∂(η : (a : γ) → Measure δ) ac.2 ∂(κ : (a : α) → Measure β) ac.1
⊢ ∫⁻ (bd : β × δ), g bd ∂(κ ∥ₖ η : (a : α × γ) → Measure (β × δ)) ac =
    ∫⁻ (b : β), ∫⁻ (d : δ), g (b, d) ∂(η : (a : γ) → Measure δ) ac.2 ∂(κ : (a : α) → Measure β) ac.1

Tactic:
rw [parallelComp_apply, MeasureTheory.lintegral_prod _ hg.aemeasurable]

Premises used: Measurable.aemeasurable, MeasureTheory.lintegral_prod, ProbabilityTheory.Kernel.parallelComp_apply
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
ac : α × γ
g : β × δ → ℝ≥0∞
hg : Measurable g
rw :
  ∫⁻ (bd : β × δ), g bd ∂Measure.prod ((κ : (a : α) → Measure β) ac.1) ((η : (a : γ) → Measure δ) ac.2) =
    ∫⁻ (d : δ), ∫⁻ (b : β), g (b, d) ∂(κ : (a : α) → Measure β) ac.1 ∂(η : (a : γ) → Measure δ) ac.2
rw₁ rw₂ :
  ∫⁻ (y : δ), ∫⁻ (x : β), g (x, y) ∂(κ : (a : α) → Measure β) ac.1 ∂(η : (a : γ) → Measure δ) ac.2 =
    ∫⁻ (d : δ), ∫⁻ (b : β), g (b, d) ∂(κ : (a : α) → Measure β) ac.1 ∂(η : (a : γ) → Measure δ) ac.2
⊢ ∫⁻ (bd : β × δ), g bd ∂(κ ∥ₖ η : (a : α × γ) → Measure (β × δ)) ac =
    ∫⁻ (d : δ), ∫⁻ (b : β), g (b, d) ∂(κ : (a : α) → Measure β) ac.1 ∂(η : (a : γ) → Measure δ) ac.2

Tactic:
rw [parallelComp_apply, MeasureTheory.lintegral_prod_symm _ hg.aemeasurable]

Premises used: Measurable.aemeasurable, MeasureTheory.lintegral_prod_symm, ProbabilityTheory.Kernel.parallelComp_apply
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
ι : Type u_5
inst : Countable ι
κ : ι → Kernel α β
inst_1 : ∀ (i : ι), IsSFiniteKernel (κ i)
η : Kernel γ δ
pos : ∀ (h : IsSFiniteKernel η), Kernel.sum κ ∥ₖ η = Kernel.sum fun (i : ι) ↦ κ i ∥ₖ η
neg : ∀ (h : ¬IsSFiniteKernel η), Kernel.sum κ ∥ₖ η = Kernel.sum fun (i : ι) ↦ κ i ∥ₖ η
⊢ Kernel.sum κ ∥ₖ η = Kernel.sum fun (i : ι) ↦ κ i ∥ₖ η

Tactic:
by_cases h : IsSFiniteKernel η

Premises used: ProbabilityTheory.IsSFiniteKernel