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 α β
η : Kernel β γ
f : γ → E
hf : @Integrable _ _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a)
⊢ @Integrable ℝ _ _ _ mβ (fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ ‖f y‖)
    ((κ : (a : α) → Measure β) a)

Tactic:
((integrable_comp_iff hf.1).1 hf).2

Premises used: And.right, And.left, Iff.mp, ProbabilityTheory.integrable_comp_iff
-- 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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
f : γ → E
hf : @Integrable _ _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a)
⊢ @Integrable.{u_4, u_2} E _ _ _ mβ (fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
    ((κ : (a : α) → Measure β) a)

Tactic:
Integrable.mono hf.integral_norm_comp hf.1.integral_kernel_comp <|
    ae_of_all _ fun _ ↦ (norm_integral_le_integral_norm _).trans_eq
    (norm_of_nonneg <| integral_nonneg_of_ae <| ae_of_all _ fun _ ↦ norm_nonneg _).symm

Premises used: LE.le.trans_eq, MeasureTheory.Integrable.mono, MeasureTheory.Integrable.integral_norm_comp, MeasureTheory.norm_integral_le_integral_norm, MeasureTheory.integral_nonneg_of_ae, And.left, MeasureTheory.ae_of_all, MeasureTheory.AEStronglyMeasurable.integral_kernel_comp, Eq.symm, DFunLike.coe, norm_nonneg, Real.norm_of_nonneg
-- 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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
E' : Type u_5
inst_2 : NormedAddCommGroup E'
inst_3 : NormedSpace ℝ E'
f g : γ → E
F : E → E'
hf : @Integrable _ _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a)
hg : @Integrable _ _ _ _ mγ g ((η ∘ₖ κ : (a : α) → Measure γ) a)
⊢ Eq.{u_5 + 1} (α := E')
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      F (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y + g y))
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      F
        (HAdd.hAdd (α := E) (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
          (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ g y)))

Tactic:
integral_congr_ae ?_

Premises used: MeasureTheory.integral_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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
E' : Type u_5
inst_2 : NormedAddCommGroup E'
inst_3 : NormedSpace ℝ E'
f g : γ → E
F : E → E'
hf : @Integrable _ _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a)
hg : @Integrable _ _ _ _ mγ g ((η ∘ₖ κ : (a : α) → Measure γ) a)
refine :
  EventuallyEq.{u_2, u_5} (β := E') (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β))
    (fun (x : β) ↦ F (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y + g y)) fun (x : β) ↦
    F
      (HAdd.hAdd (α := E) (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
        (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ g y))
⊢ Eq.{u_5 + 1} (α := E')
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      F (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y + g y))
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      F
        (HAdd.hAdd (α := E) (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
          (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ g y)))

Tactic:
refine integral_congr_ae ?_

Premises used: MeasureTheory.integral_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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
E' : Type u_5
inst_2 : NormedAddCommGroup E'
inst_3 : NormedSpace ℝ E'
f g : γ → E
F : E → E'
hf : @Integrable _ _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a)
hg : @Integrable _ _ _ _ mγ g ((η ∘ₖ κ : (a : α) → Measure γ) a)
h :
  ∀ (a : β) (h2f : @Integrable _ _ _ _ mγ f ((η : (a : β) → Measure γ) a))
    (h2g : @Integrable _ _ _ _ mγ g ((η : (a : β) → Measure γ) a)),
    F (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a) fun (y : γ) ↦ f y + g y) =
      F
        (HAdd.hAdd (α := E) (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a) fun (y : γ) ↦ f y)
          (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a) fun (y : γ) ↦ g y))
⊢ EventuallyEq.{u_2, u_5} (β := E') (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β))
    (fun (x : β) ↦ F (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y + g y)) fun (x : β) ↦
    F
      (HAdd.hAdd (α := E) (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
        (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ g y))

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

Premises used: MeasureTheory.Integrable.ae_of_comp
-- 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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
E' : Type u_5
inst_2 : NormedAddCommGroup E'
inst_3 : NormedSpace ℝ E'
f g : γ → E
F : E → E'
hf : @Integrable _ _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a)
hg : @Integrable _ _ _ _ mγ g ((η ∘ₖ κ : (a : α) → Measure γ) a)
a_1 : β
h2f : @Integrable _ _ _ _ mγ f ((η : (a : β) → Measure γ) a_1)
h2g : @Integrable _ _ _ _ mγ g ((η : (a : β) → Measure γ) a_1)
⊢ F (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a_1) fun (y : γ) ↦ f y + g y) =
    F
      (HAdd.hAdd (α := E) (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a_1) fun (y : γ) ↦ f y)
        (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a_1) fun (y : γ) ↦ g y))

Tactic:
simp [integral_add h2f h2g]

Premises used: MeasureTheory.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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
E' : Type u_5
inst_2 : NormedAddCommGroup E'
inst_3 : NormedSpace ℝ E'
f g : γ → E
F : E → E'
hf : @Integrable _ _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a)
hg : @Integrable _ _ _ _ mγ g ((η ∘ₖ κ : (a : α) → Measure γ) a)
⊢ Eq.{u_5 + 1} (α := E')
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      F (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y - g y))
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      F
        (HSub.hSub (α := E) (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
          (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ g y)))

Tactic:
integral_congr_ae ?_

Premises used: MeasureTheory.integral_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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
E' : Type u_5
inst_2 : NormedAddCommGroup E'
inst_3 : NormedSpace ℝ E'
f g : γ → E
F : E → E'
hf : @Integrable _ _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a)
hg : @Integrable _ _ _ _ mγ g ((η ∘ₖ κ : (a : α) → Measure γ) a)
refine :
  EventuallyEq.{u_2, u_5} (β := E') (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β))
    (fun (x : β) ↦ F (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y - g y)) fun (x : β) ↦
    F
      (HSub.hSub (α := E) (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
        (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ g y))
⊢ Eq.{u_5 + 1} (α := E')
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      F (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y - g y))
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      F
        (HSub.hSub (α := E) (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
          (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ g y)))

Tactic:
refine integral_congr_ae ?_

Premises used: MeasureTheory.integral_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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
E' : Type u_5
inst_2 : NormedAddCommGroup E'
inst_3 : NormedSpace ℝ E'
f g : γ → E
F : E → E'
hf : @Integrable _ _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a)
hg : @Integrable _ _ _ _ mγ g ((η ∘ₖ κ : (a : α) → Measure γ) a)
h :
  ∀ (a : β) (h2f : @Integrable _ _ _ _ mγ f ((η : (a : β) → Measure γ) a))
    (h2g : @Integrable _ _ _ _ mγ g ((η : (a : β) → Measure γ) a)),
    F (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a) fun (y : γ) ↦ f y - g y) =
      F
        (HSub.hSub (α := E) (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a) fun (y : γ) ↦ f y)
          (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a) fun (y : γ) ↦ g y))
⊢ EventuallyEq.{u_2, u_5} (β := E') (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β))
    (fun (x : β) ↦ F (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y - g y)) fun (x : β) ↦
    F
      (HSub.hSub (α := E) (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
        (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ g y))

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

Premises used: MeasureTheory.Integrable.ae_of_comp
-- 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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
E' : Type u_5
inst_2 : NormedAddCommGroup E'
inst_3 : NormedSpace ℝ E'
f g : γ → E
F : E → E'
hf : @Integrable _ _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a)
hg : @Integrable _ _ _ _ mγ g ((η ∘ₖ κ : (a : α) → Measure γ) a)
a_1 : β
h2f : @Integrable _ _ _ _ mγ f ((η : (a : β) → Measure γ) a_1)
h2g : @Integrable _ _ _ _ mγ g ((η : (a : β) → Measure γ) a_1)
⊢ F (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a_1) fun (y : γ) ↦ f y - g y) =
    F
      (HSub.hSub (α := E) (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a_1) fun (y : γ) ↦ f y)
        (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a_1) fun (y : γ) ↦ g 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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
f g : γ → E
F : E → ℝ≥0∞
hf : @Integrable _ _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a)
hg : @Integrable _ _ _ _ mγ g ((η ∘ₖ κ : (a : α) → Measure γ) a)
⊢ ∫⁻ (x : β),
      F (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y - g y) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (x : β),
      F
        (HSub.hSub (α := E) (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
          (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ g y)) ∂(κ : (a : α) → Measure β) a

Tactic:
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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
f g : γ → E
F : E → ℝ≥0∞
hf : @Integrable _ _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a)
hg : @Integrable _ _ _ _ mγ g ((η ∘ₖ κ : (a : α) → Measure γ) a)
refine :
  (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (x : β) ↦ F (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y - g y)) fun (x : β) ↦
    F
      (HSub.hSub (α := E) (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
        (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ g y))
⊢ ∫⁻ (x : β),
      F (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y - g y) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (x : β),
      F
        (HSub.hSub (α := E) (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
          (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ g 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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
f g : γ → E
F : E → ℝ≥0∞
hf : @Integrable _ _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a)
hg : @Integrable _ _ _ _ mγ g ((η ∘ₖ κ : (a : α) → Measure γ) a)
h :
  ∀ (a : β) (h2f : @Integrable _ _ _ _ mγ f ((η : (a : β) → Measure γ) a))
    (h2g : @Integrable _ _ _ _ mγ g ((η : (a : β) → Measure γ) a)),
    F (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a) fun (y : γ) ↦ f y - g y) =
      F
        (HSub.hSub (α := E) (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a) fun (y : γ) ↦ f y)
          (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a) fun (y : γ) ↦ g y))
⊢ (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (x : β) ↦ F (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y - g y)) fun (x : β) ↦
    F
      (HSub.hSub (α := E) (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
        (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ g y))

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

Premises used: MeasureTheory.Integrable.ae_of_comp
-- 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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
f g : γ → E
F : E → ℝ≥0∞
hf : @Integrable _ _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a)
hg : @Integrable _ _ _ _ mγ g ((η ∘ₖ κ : (a : α) → Measure γ) a)
a_1 : β
h2f : @Integrable _ _ _ _ mγ f ((η : (a : β) → Measure γ) a_1)
h2g : @Integrable _ _ _ _ mγ g ((η : (a : β) → Measure γ) a_1)
⊢ F (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a_1) fun (y : γ) ↦ f y - g y) =
    F
      (HSub.hSub (α := E) (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a_1) fun (y : γ) ↦ f y)
        (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) a_1) fun (y : γ) ↦ g 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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
f g : γ → E
hf : @Integrable _ _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a)
hg : @Integrable _ _ _ _ mγ g ((η ∘ₖ κ : (a : α) → Measure γ) a)
⊢ (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y + g y) =
    HAdd.hAdd (α := E)
      (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
        @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
      (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
        @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ g y)

Tactic:
(integral_fn_integral_add_comp id hf hg).trans <| integral_add hf.integral_comp hg.integral_comp

Premises used: MeasureTheory.Integrable.integral_comp, ProbabilityTheory.Kernel.integral_fn_integral_add_comp, id, 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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
f g : γ → E
hf : @Integrable _ _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a)
hg : @Integrable _ _ _ _ mγ g ((η ∘ₖ κ : (a : α) → Measure γ) a)
⊢ (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ (f + g) y) =
    HAdd.hAdd (α := E)
      (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
        @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
      (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
        @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ g y)

Tactic:
integral_integral_add_comp hf hg

Premises used: ProbabilityTheory.Kernel.integral_integral_add_comp
-- 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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
f g : γ → E
hf : @Integrable _ _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a)
hg : @Integrable _ _ _ _ mγ g ((η ∘ₖ κ : (a : α) → Measure γ) a)
⊢ (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y - g y) =
    HSub.hSub (α := E)
      (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
        @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
      (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
        @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ g y)

Tactic:
(integral_fn_integral_sub_comp id hf hg).trans <| integral_sub hf.integral_comp hg.integral_comp

Premises used: MeasureTheory.Integrable.integral_comp, id, MeasureTheory.integral_sub, ProbabilityTheory.Kernel.integral_fn_integral_sub_comp, 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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
f g : γ → E
hf : @Integrable _ _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a)
hg : @Integrable _ _ _ _ mγ g ((η ∘ₖ κ : (a : α) → Measure γ) a)
⊢ (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ (f - g) y) =
    HSub.hSub (α := E)
      (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
        @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
      (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
        @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ g y)

Tactic:
integral_integral_sub_comp hf hg

Premises used: ProbabilityTheory.Kernel.integral_integral_sub_comp
-- 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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (f : ↥(Lp E 1 ((η ∘ₖ κ : (a : α) → Measure γ) a))) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦
        (↑(↑f : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) y

Tactic:
continuous_iff_continuousAt.2 fun g ↦ ?_

Premises used: Iff.mpr, 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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
refine :
  ∀ (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 γ) x) fun (y : γ) ↦
            (↑(↑f : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) y)
      g
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (f : ↥(Lp E 1 ((η ∘ₖ κ : (a : α) → Measure γ) a))) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦
        (↑(↑f : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) y

Tactic:
refine continuous_iff_continuousAt.2 fun g ↦ ?_

Premises used: Iff.mpr, 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 α β
η : Kernel β γ
inst_1 : 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 γ) x) fun (y : γ) ↦
          (↑(↑f : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) y)
    g

Tactic:
tendsto_integral_of_L1 _ (L1.integrable_coeFn g).integral_comp.aestronglyMeasurable
      (Eventually.of_forall fun h ↦ (L1.integrable_coeFn h).integral_comp) ?_

Premises used: MeasureTheory.Integrable.integral_comp, MeasureTheory.Integrable.aestronglyMeasurable, MeasureTheory.tendsto_integral_of_L1, ContinuousAt, MeasureTheory.L1.integrable_coeFn, Filter.Eventually.of_forall