awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : NormedAddCommGroup E
a : α
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
inst_3 : NormedSpace ℝ E
g : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a))
this :
  ∀ (i : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a))),
    Measurable (β := ℝ≥0∞) fun (z : β × γ) ↦
      ‖(↑(↑i : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E) z -
          (↑(↑g : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E) z‖ₑ
⊢ Tendsto (fun (i : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a))) ↦ ENNReal.ofReal ‖i - g‖) (𝓝 g)
    (𝓝 (ENNReal.ofReal 0))

Tactic:
(continuous_ofReal.tendsto 0).comp ?_

Premises used: ENNReal.ofNNReal, ENNReal.ofReal, ENNReal.continuous_ofReal, WithTop.some, Continuous.tendsto, Filter.Tendsto.comp, OfNat.ofNat
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : NormedAddCommGroup E
a : α
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
inst_3 : NormedSpace ℝ E
g : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a))
this :
  ∀ (i : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a))),
    Measurable (β := ℝ≥0∞) fun (z : β × γ) ↦
      ‖(↑(↑i : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E) z -
          (↑(↑g : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E) z‖ₑ
refine : Tendsto (β := ℝ) (fun (i : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a))) ↦ ‖i - g‖) (𝓝 g) (𝓝 0)
⊢ Tendsto (fun (i : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a))) ↦ ENNReal.ofReal ‖i - g‖) (𝓝 g)
    (𝓝 (ENNReal.ofReal 0))

Tactic:
refine (continuous_ofReal.tendsto 0).comp ?_

Premises used: ENNReal.continuous_ofReal, Continuous.tendsto, Filter.Tendsto.comp, OfNat.ofNat
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : NormedAddCommGroup E
a : α
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
inst_3 : NormedSpace ℝ E
g : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a))
this :
  ∀ (i : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a))),
    Measurable (β := ℝ≥0∞) fun (z : β × γ) ↦
      ‖(↑(↑i : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E) z -
          (↑(↑g : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E) z‖ₑ
rw : Tendsto (fun (i : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a))) ↦ i) (𝓝 g) (𝓝 g)
⊢ Tendsto (β := ℝ) (fun (i : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a))) ↦ ‖i - g‖) (𝓝 g) (𝓝 0)

Tactic:
rw [← tendsto_iff_norm_sub_tendsto_zero]

Premises used: tendsto_iff_norm_sub_tendsto_zero
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : NormedAddCommGroup E
a : α
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
inst_3 : NormedSpace ℝ E
g : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a))
this :
  ∀ (i : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a))),
    Measurable (β := ℝ≥0∞) fun (z : β × γ) ↦
      ‖(↑(↑i : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E) z -
          (↑(↑g : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E) z‖ₑ
⊢ Tendsto (fun (i : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a))) ↦ i) (𝓝 g) (𝓝 g)

Tactic:
tendsto_id

Premises used: Set.Mem, Filter.tendsto_id, setOf
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : NormedAddCommGroup E
a : α
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
inst_3 : NormedSpace ℝ E
g : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a))
this :
  ∀ (i : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a))),
    Measurable (β := ℝ≥0∞) fun (z : β × γ) ↦
      ‖(↑(↑i : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E) z -
          (↑(↑g : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E) z‖ₑ
⊢ Tendsto (fun (i : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a))) ↦ i) (𝓝 g) (𝓝 g)

Tactic:
exact tendsto_id

Premises used: Filter.tendsto_id
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : NormedAddCommGroup E
a : α
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
inst_3 : NormedSpace ℝ E
pos :
  ∀ {f : β × γ → E} (hE : CompleteSpace E),
    @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) →
      Eq.{u_4 + 1} (α := E)
        (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦ f z)
        (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
          @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
neg :
  ∀ {f : β × γ → E} (hE : ¬CompleteSpace E),
    @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) →
      Eq.{u_4 + 1} (α := E)
        (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦ f z)
        (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
          @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
⊢ ∀ {f : β × γ → E},
    @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) →
      Eq.{u_4 + 1} (α := E)
        (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦ f z)
        (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
          @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))

Tactic:
by_cases hE : CompleteSpace E

Premises used: CompleteSpace
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : NormedAddCommGroup E
a : α
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
inst_3 : NormedSpace ℝ E
f : β × γ → E
hE : ¬CompleteSpace E
⊢ @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) →
    Eq.{u_4 + 1} (α := E)
      (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦ f z)
      (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
        @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))

Tactic:
simp [integral, hE]

Premises used: MeasureTheory.integral
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : NormedAddCommGroup E
a : α
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
inst_3 : NormedSpace ℝ E
f : β × γ → E
hE : CompleteSpace E
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s :
  LT.lt (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
pos :
  ENNReal.toReal ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s) • c =
    HSMul.hSMul (α := ℝ)
      (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
        ENNReal.toReal ((((η : (a : α × β) → Measure γ) (a, x) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk x ⁻¹' s)))
      c
⊢ Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦
      s.indicator (fun (x : β × γ) ↦ c) z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦
        s.indicator (fun (x : β × γ) ↦ c) (x, y))

Tactic:
simp_rw [integral_indicator hs, ← indicator_comp_right, Function.comp_def,
      integral_indicator (measurable_prodMk_left hs), MeasureTheory.setIntegral_const,
      integral_smul_const, measureReal_def]

Premises used: MeasureTheory.integral_indicator, integral_smul_const, Set.indicator_comp_right, Function.comp_def, MeasureTheory.measureReal_def, measurable_prodMk_left, MeasureTheory.setIntegral_const
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : NormedAddCommGroup E
a : α
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
inst_3 : NormedSpace ℝ E
f : β × γ → E
hE : CompleteSpace E
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s :
  LT.lt (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
pos :
  ENNReal.toReal ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s) =
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      ENNReal.toReal ((((η : (a : α × β) → Measure γ) (a, x) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk x ⁻¹' s))
⊢ ENNReal.toReal ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s) • c =
    HSMul.hSMul (α := ℝ)
      (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
        ENNReal.toReal ((((η : (a : α × β) → Measure γ) (a, x) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk x ⁻¹' s)))
      c

Tactic:
congr 1
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : NormedAddCommGroup E
a : α
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
inst_3 : NormedSpace ℝ E
f : β × γ → E
hE : CompleteSpace E
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s :
  LT.lt (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
pos :
  ENNReal.toReal ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s) =
    (∫⁻ (a_1 : β),
        (((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (Prod.mk a_1 ⁻¹' s) ∂(κ : (a : α) → Measure β) a).toReal
pos₁ :
  AEMeasurable (β := ℝ≥0∞) (_m := mβ)
    (fun (x : β) ↦ (((η : (a : α × β) → Measure γ) (a, x) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk x ⁻¹' s))
    ((κ : (a : α) → Measure β) a)
pos₂ :
  ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    LT.lt (α := ℝ≥0∞)
      ((((η : (a : α × β) → Measure γ) (a, x) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk x ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ENNReal.toReal ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s) =
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      ENNReal.toReal ((((η : (a : α × β) → Measure γ) (a, x) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk x ⁻¹' s))

Tactic:
rw [integral_toReal]

Premises used: MeasureTheory.integral_toReal
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : NormedAddCommGroup E
a : α
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
inst_3 : NormedSpace ℝ E
f : β × γ → E
hE : CompleteSpace E
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s :
  LT.lt (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ AEMeasurable (β := ℝ≥0∞) (_m := mβ)
    (fun (x : β) ↦ (((η : (a : α × β) → Measure γ) (a, x) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk x ⁻¹' s))
    ((κ : (a : α) → Measure β) a)

Tactic:
(Kernel.measurable_kernel_prodMk_left' hs _).aemeasurable

Premises used: Measurable.aemeasurable, ProbabilityTheory.Kernel.measurable_kernel_prodMk_left'
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : NormedAddCommGroup E
a : α
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
inst_3 : NormedSpace ℝ E
f : β × γ → E
hE : CompleteSpace E
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s :
  LT.lt (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ AEMeasurable (β := ℝ≥0∞) (_m := mβ)
    (fun (x : β) ↦ (((η : (a : α × β) → Measure γ) (a, x) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk x ⁻¹' s))
    ((κ : (a : α) → Measure β) a)

Tactic:
exact (Kernel.measurable_kernel_prodMk_left' hs _).aemeasurable

Premises used: Measurable.aemeasurable, ProbabilityTheory.Kernel.measurable_kernel_prodMk_left'
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : NormedAddCommGroup E
a : α
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
inst_3 : NormedSpace ℝ E
f : β × γ → E
hE : CompleteSpace E
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s :
  LT.lt (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    LT.lt (α := ℝ≥0∞)
      ((((η : (a : α × β) → Measure γ) (a, x) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk x ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
ae_kernel_lt_top a h2s.ne

Premises used: ProbabilityTheory.Kernel.ae_kernel_lt_top, LT.lt.ne
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : NormedAddCommGroup E
a : α
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
inst_3 : NormedSpace ℝ E
f : β × γ → E
hE : CompleteSpace E
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s :
  LT.lt (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    LT.lt (α := ℝ≥0∞)
      ((((η : (a : α × β) → Measure γ) (a, x) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk x ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact ae_kernel_lt_top a h2s.ne

Premises used: ProbabilityTheory.Kernel.ae_kernel_lt_top, LT.lt.ne
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : NormedAddCommGroup E
a : α
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
inst_3 : NormedSpace ℝ E
f : β × γ → E
hE : CompleteSpace E
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s :
  LT.lt (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
pos pos₁ :
  (∫⁻ (b : β),
        (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a).toReal =
    (∫⁻ (a_1 : β),
        (((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (Prod.mk a_1 ⁻¹' s) ∂(κ : (a : α) → Measure β) a).toReal
⊢ ENNReal.toReal ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s) =
    (∫⁻ (a_1 : β),
        (((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (Prod.mk a_1 ⁻¹' s) ∂(κ : (a : α) → Measure β) a).toReal

Tactic:
rw [Kernel.compProd_apply hs]

Premises used: ProbabilityTheory.Kernel.compProd_apply
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : NormedAddCommGroup E
a : α
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
inst_3 : NormedSpace ℝ E
f_1 : β × γ → E
hE : CompleteSpace E
f g : β × γ → E
pos :
  Disjoint (support f) (support g) →
    @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) →
      @Integrable _ _ _ _ Prod.instMeasurableSpace g ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) →
        Eq.{u_4 + 1} (α := E)
            (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦ f z)
            (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
              @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y)) →
          Eq.{u_4 + 1} (α := E)
              (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦
                g z)
              (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
                @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ g (x, y)) →
            Eq.{u_4 + 1} (α := E)
              (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦
                (f + g) z)
              (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
                @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ (f + g) (x, y))
⊢ Disjoint (support f) (support g) →
    @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) →
      @Integrable _ _ _ _ Prod.instMeasurableSpace g ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) →
        Eq.{u_4 + 1} (α := E)
            (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦ f z)
            (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
              @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y)) →
          Eq.{u_4 + 1} (α := E)
              (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦
                g z)
              (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
                @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ g (x, y)) →
            Eq.{u_4 + 1} (α := E)
              (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦
                (f + g) z)
              (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
                @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ (f + g) (x, y))

Tactic:
_
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : NormedAddCommGroup E
a : α
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
inst_3 : NormedSpace ℝ E
f : β × γ → E
hE : CompleteSpace E
⊢ IsClosed (X := ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)))
    {f : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)) |
      Eq.{u_4 + 1} (α := E)
        (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦
          (↑(↑f : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E) z)
        (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
          @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦
            (↑(↑f : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E) (x, y))}

Tactic:
isClosed_eq continuous_integral Kernel.continuous_integral_integral

Premises used: ProbabilityTheory.Kernel.continuous_integral_integral, isClosed_eq, MeasureTheory.continuous_integral
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : NormedAddCommGroup E
a : α
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
inst_3 : NormedSpace ℝ E
f : β × γ → E
hE : CompleteSpace E
⊢ IsClosed (X := ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)))
    {f : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)) |
      Eq.{u_4 + 1} (α := E)
        (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦
          (↑(↑f : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E) z)
        (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
          @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦
            (↑(↑f : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E) (x, y))}

Tactic:
exact isClosed_eq continuous_integral Kernel.continuous_integral_integral

Premises used: ProbabilityTheory.Kernel.continuous_integral_integral, isClosed_eq, MeasureTheory.continuous_integral
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : NormedAddCommGroup E
a : α
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
inst_3 : NormedSpace ℝ E
f_1 : β × γ → E
hE : CompleteSpace E
f g : β × γ → E
hfg : f =ᶠ[ae (F := Measure (β × γ)) ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ))] g
pos :
  @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) →
    Eq.{u_4 + 1} (α := E)
        (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦ f z)
        (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
          @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y)) →
      Eq.{u_4 + 1} (α := E)
        (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦ g z)
        (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
          @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ g (x, y))
⊢ @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) →
    Eq.{u_4 + 1} (α := E)
        (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦ f z)
        (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
          @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y)) →
      Eq.{u_4 + 1} (α := E)
        (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) fun (z : β × γ) ↦ g z)
        (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
          @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ g (x, y))

Tactic:
_