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
f g : β × γ → E
F : E → ℝ≥0∞
hf : @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
hg : @Integrable _ _ _ _ Prod.instMeasurableSpace g ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
refine :
  (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (x : β) ↦ F (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y) - g (x, y)))
    fun (x : β) ↦
    F
      (HSub.hSub (α := E) (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
        (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ g (x, y)))
⊢ ∫⁻ (x : β),
      F
        (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦
          f (x, y) - g (x, y)) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (x : β),
      F
        (HSub.hSub (α := E) (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
          (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦
            g (x, y))) ∂(κ : (a : α) → Measure β) a

Tactic:
refine lintegral_congr_ae ?_

Premises used: MeasureTheory.lintegral_congr_ae
-- 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 g : β × γ → E
F : E → ℝ≥0∞
hf : @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
hg : @Integrable _ _ _ _ Prod.instMeasurableSpace g ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
h :
  ∀ (a_1 : β)
    (h2f : @Integrable.{u_4, u_3} E _ _ _ mγ (fun (y : γ) ↦ f (a_1, y)) ((η : (a : α × β) → Measure γ) (a, a_1)))
    (h2g : @Integrable.{u_4, u_3} E _ _ _ mγ (fun (y : γ) ↦ g (a_1, y)) ((η : (a : α × β) → Measure γ) (a, a_1))),
    F (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦ f (a_1, y) - g (a_1, y)) =
      F
        (HSub.hSub (α := E) (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦ f (a_1, y))
          (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦ g (a_1, y)))
⊢ (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (x : β) ↦ F (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y) - g (x, y)))
    fun (x : β) ↦
    F
      (HSub.hSub (α := E) (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
        (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ g (x, y)))

Tactic:
filter_upwards [hf.ae_of_compProd, hg.ae_of_compProd] with _ h2f h2g

Premises used: MeasureTheory.Integrable.ae_of_compProd
-- 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 g : β × γ → E
F : E → ℝ≥0∞
hf : @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
hg : @Integrable _ _ _ _ Prod.instMeasurableSpace g ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
a_1 : β
h2f : @Integrable.{u_4, u_3} E _ _ _ mγ (fun (y : γ) ↦ f (a_1, y)) ((η : (a : α × β) → Measure γ) (a, a_1))
h2g : @Integrable.{u_4, u_3} E _ _ _ mγ (fun (y : γ) ↦ g (a_1, y)) ((η : (a : α × β) → Measure γ) (a, a_1))
⊢ F (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦ f (a_1, y) - g (a_1, y)) =
    F
      (HSub.hSub (α := E) (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦ f (a_1, y))
        (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦ g (a_1, y)))

Tactic:
simp [integral_sub h2f h2g]

Premises used: MeasureTheory.integral_sub
-- 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 g : β × γ → E
hf : @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
hg : @Integrable _ _ _ _ Prod.instMeasurableSpace g ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
⊢ (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y) + g (x, y)) =
    HAdd.hAdd (α := E)
      (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
        @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
      (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
        @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ g (x, y))

Tactic:
(Kernel.integral_fn_integral_add id hf hg).trans <|
    integral_add hf.integral_compProd hg.integral_compProd

Premises used: ProbabilityTheory.Kernel.integral_fn_integral_add, id, MeasureTheory.Integrable.integral_compProd, MeasureTheory.integral_add, Eq.trans
-- 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 g : β × γ → E
hf : @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
hg : @Integrable _ _ _ _ Prod.instMeasurableSpace g ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
⊢ (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ (f + g) (x, y)) =
    HAdd.hAdd (α := E)
      (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
        @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
      (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
        @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ g (x, y))

Tactic:
Kernel.integral_integral_add hf hg

Premises used: ProbabilityTheory.Kernel.integral_integral_add
-- 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 g : β × γ → E
hf : @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
hg : @Integrable _ _ _ _ Prod.instMeasurableSpace g ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
⊢ (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y) - g (x, y)) =
    HSub.hSub (α := E)
      (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
        @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
      (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
        @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ g (x, y))

Tactic:
(Kernel.integral_fn_integral_sub id hf hg).trans <|
    integral_sub hf.integral_compProd hg.integral_compProd

Premises used: id, MeasureTheory.integral_sub, MeasureTheory.Integrable.integral_compProd, ProbabilityTheory.Kernel.integral_fn_integral_sub, Eq.trans
-- 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 g : β × γ → E
hf : @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
hg : @Integrable _ _ _ _ Prod.instMeasurableSpace g ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
⊢ (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ (f - g) (x, y)) =
    HSub.hSub (α := E)
      (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
        @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y))
      (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
        @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ g (x, y))

Tactic:
Kernel.integral_integral_sub hf hg

Premises used: ProbabilityTheory.Kernel.integral_integral_sub
-- 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
rw :
  ∀ (x : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a))),
    ContinuousAt (Y := E)
      (fun (f : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a))) ↦
        @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
          @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦
            (↑(↑f : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E) (x, y))
      x
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (f : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a))) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦
        (↑(↑f : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E) (x, y)

Tactic:
rw [continuous_iff_continuousAt]

Premises used: continuous_iff_continuousAt
-- 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))
⊢ ContinuousAt (Y := E)
    (fun (f : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a))) ↦
      @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
        @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦
          (↑(↑f : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E) (x, y))
    g

Tactic:
tendsto_integral_of_L1 _ (L1.integrable_coeFn g).integral_compProd.aestronglyMeasurable
      (Eventually.of_forall fun h => (L1.integrable_coeFn h).integral_compProd) ?_

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, MeasureTheory.tendsto_integral_of_L1, ContinuousAt, MeasureTheory.L1.integrable_coeFn, Filter.Eventually.of_forall, MeasureTheory.Integrable.integral_compProd
-- 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))
tendsto_integral_of_L1 :
  Tendsto (β := ℝ≥0∞)
    (fun (i : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a))) ↦
      ∫⁻ (x : β),
        ‖HSub.hSub (α := E)
            (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦
              (↑(↑i : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E) (x, y))
            (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦
              (↑(↑g : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E)
                (x, y))‖ₑ ∂(κ : (a : α) → Measure β) a)
    (𝓝 g) (𝓝 0)
⊢ ContinuousAt (Y := E)
    (fun (f : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a))) ↦
      @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
        @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦
          (↑(↑f : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E) (x, y))
    g

Tactic:
refine
    tendsto_integral_of_L1 _ (L1.integrable_coeFn g).integral_compProd.aestronglyMeasurable
      (Eventually.of_forall fun h => (L1.integrable_coeFn h).integral_compProd) ?_

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, MeasureTheory.tendsto_integral_of_L1, MeasureTheory.L1.integrable_coeFn, Filter.Eventually.of_forall, MeasureTheory.Integrable.integral_compProd
-- 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))
simp_rw :
  Tendsto (β := ℝ≥0∞)
    (fun (i : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a))) ↦
      ∫⁻ (x : β),
        enorm.{u_4} (E := E)
          (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦
            (↑(↑i : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E) (x, y) -
              (↑(↑g : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E)
                (x, y)) ∂(κ : (a : α) → Measure β) a)
    (𝓝 g) (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (i : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a))) ↦
      ∫⁻ (x : β),
        ‖HSub.hSub (α := E)
            (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦
              (↑(↑i : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E) (x, y))
            (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦
              (↑(↑g : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E)
                (x, y))‖ₑ ∂(κ : (a : α) → Measure β) a)
    (𝓝 g) (𝓝 0)

Tactic:
simp_rw [← lintegral_fn_integral_sub (‖·‖ₑ) (L1.integrable_coeFn _) (L1.integrable_coeFn g)]

Premises used: MeasureTheory.L1.integrable_coeFn, ENorm.enorm, ProbabilityTheory.Kernel.lintegral_fn_integral_sub
-- 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))
apply : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)) → ℝ≥0∞
apply₁ :
  Tendsto (β := ℝ≥0∞)
    (fun (i : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a))) ↦
      ∫⁻ (x : β),
        ∫⁻ (y : γ),
          ‖(↑(↑i : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E) (x, y) -
              (↑(↑g : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E)
                (x, y)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a)
    (𝓝 g) (𝓝 0)
apply₂ :
  LE.le (α := ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)) → ℝ≥0∞)
    (fun (i : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a))) ↦
      ∫⁻ (x : β),
        enorm.{u_4} (E := E)
          (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦
            (↑(↑i : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E) (x, y) -
              (↑(↑g : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E)
                (x, y)) ∂(κ : (a : α) → Measure β) a)
    fun (i : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a))) ↦
    ∫⁻ (x : β),
      ∫⁻ (y : γ),
        ‖(↑(↑i : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E) (x, y) -
            (↑(↑g : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E)
              (x, y)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a
⊢ Tendsto (β := ℝ≥0∞)
    (fun (i : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a))) ↦
      ∫⁻ (x : β),
        enorm.{u_4} (E := E)
          (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦
            (↑(↑i : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E) (x, y) -
              (↑(↑g : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E)
                (x, y)) ∂(κ : (a : α) → Measure β) a)
    (𝓝 g) (𝓝 0)

Tactic:
apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds _ (fun i => zero_le) _

Premises used: zero_le, tendsto_of_tendsto_of_tendsto_of_le_of_le, tendsto_const_nhds
-- 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))
⊢ ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)) → ℝ≥0∞

Tactic:
exact fun i => ∫⁻ x, ∫⁻ y, ‖i (x, y) - g (x, y)‖ₑ ∂η (a, x) ∂κ a

Premises used: MeasureTheory.AEEqFun.cast, HSub.hSub, Prod.mk, ENorm.enorm, Subtype.val, DFunLike.coe, MeasureTheory.lintegral
-- 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))
⊢ LE.le (α := ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)) → ℝ≥0∞)
    (fun (i : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a))) ↦
      ∫⁻ (x : β),
        enorm.{u_4} (E := E)
          (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦
            (↑(↑i : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E) (x, y) -
              (↑(↑g : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E)
                (x, y)) ∂(κ : (a : α) → Measure β) a)
    fun (i : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a))) ↦
    ∫⁻ (x : β),
      ∫⁻ (y : γ),
        ‖(↑(↑i : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E) (x, y) -
            (↑(↑g : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E)
              (x, y)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a

Tactic:
fun i => lintegral_mono fun x => enorm_integral_le_lintegral_enorm _

Premises used: MeasureTheory.AEEqFun.cast, HSub.hSub, MeasureTheory.enorm_integral_le_lintegral_enorm, Prod.mk, MeasureTheory.lintegral_mono, Subtype.val
-- 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))
⊢ LE.le (α := ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)) → ℝ≥0∞)
    (fun (i : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a))) ↦
      ∫⁻ (x : β),
        enorm.{u_4} (E := E)
          (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦
            (↑(↑i : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E) (x, y) -
              (↑(↑g : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E)
                (x, y)) ∂(κ : (a : α) → Measure β) a)
    fun (i : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a))) ↦
    ∫⁻ (x : β),
      ∫⁻ (y : γ),
        ‖(↑(↑i : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E) (x, y) -
            (↑(↑g : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E)
              (x, y)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a

Tactic:
exact fun i => lintegral_mono fun x => enorm_integral_le_lintegral_enorm _

Premises used: MeasureTheory.enorm_integral_le_lintegral_enorm, MeasureTheory.lintegral_mono
-- 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))
⊢ ∀ (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‖ₑ

Tactic:
have this (i : Lp (α := β × γ) E 1 (((κ ⊗ₖ η) a) : Measure (β × γ))) :
      Measurable fun z => ‖i z - g z‖ₑ :=
    ((Lp.stronglyMeasurable i).sub (Lp.stronglyMeasurable g)).enorm
-- 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‖ₑ
simp_rw :
  Tendsto (fun (i : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a))) ↦ ENNReal.ofReal ‖i - g‖) (𝓝 g)
    (𝓝 (ENNReal.ofReal 0))
⊢ Tendsto (β := ℝ≥0∞)
    (fun (i : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a))) ↦
      ∫⁻ (x : β),
        ∫⁻ (y : γ),
          ‖(↑(↑i : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E) (x, y) -
              (↑(↑g : β × γ →ₘ[(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a] E) : β × γ → E)
                (x, y)‖ₑ ∂(η : (a : α × β) → Measure γ) (a, x) ∂(κ : (a : α) → Measure β) a)
    (𝓝 g) (𝓝 0)

Tactic:
simp_rw [← lintegral_compProd _ _ _ (this _), ← L1.ofReal_norm_sub_eq_lintegral, ← ofReal_zero]

Premises used: ENNReal.ofReal_zero, MeasureTheory.L1.ofReal_norm_sub_eq_lintegral, ProbabilityTheory.Kernel.lintegral_compProd