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 β γ
inst_1 : NormedSpace ℝ E
g : ↥(Lp E 1 ((η ∘ₖ κ : (a : α) → Measure γ) a))
refine :
  Tendsto (β := ℝ≥0∞)
    (fun (i : ↥(Lp E 1 ((η ∘ₖ κ : (a : α) → Measure γ) a))) ↦
      ∫⁻ (x : β),
        ‖HSub.hSub (α := E)
            (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦
              (↑(↑i : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) y)
            (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦
              (↑(↑g : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) 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 γ) x) fun (y : γ) ↦
          (↑(↑f : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) y)
    g

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

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

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

Tactic:
tendsto_of_tendsto_of_tendsto_of_le_of_le
    (h := fun i ↦ ∫⁻ x, ∫⁻ y, ‖i y - g y‖ₑ ∂η x ∂κ a)
    tendsto_const_nhds ?_ (fun _ ↦ 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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
g : ↥(Lp E 1 ((η ∘ₖ κ : (a : α) → Measure γ) a))
refine_1 :
  Tendsto (β := ℝ≥0∞)
    (fun (i : ↥(Lp E 1 ((η ∘ₖ κ : (a : α) → Measure γ) a))) ↦
      ∫⁻ (x : β),
        ∫⁻ (y : γ),
          ‖(↑(↑i : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) y -
              (↑(↑g : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E)
                y‖ₑ ∂(η : (a : β) → Measure γ) x ∂(κ : (a : α) → Measure β) a)
    (𝓝 g) (𝓝 0)
refine_2 :
  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 γ) x) fun (y : γ) ↦
            (↑(↑i : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) y -
              (↑(↑g : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) y) ∂(κ : (a : α) → Measure β) a)
    fun (i : ↥(Lp E 1 ((η ∘ₖ κ : (a : α) → Measure γ) a))) ↦
    ∫⁻ (x : β),
      ∫⁻ (y : γ),
        ‖(↑(↑i : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) y -
            (↑(↑g : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E)
              y‖ₑ ∂(η : (a : β) → Measure γ) x ∂(κ : (a : α) → Measure β) a
⊢ Tendsto (β := ℝ≥0∞)
    (fun (i : ↥(Lp E 1 ((η ∘ₖ κ : (a : α) → Measure γ) a))) ↦
      ∫⁻ (x : β),
        enorm.{u_4} (E := E)
          (@integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦
            (↑(↑i : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) y -
              (↑(↑g : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) y) ∂(κ : (a : α) → Measure β) a)
    (𝓝 g) (𝓝 0)

Tactic:
refine tendsto_of_tendsto_of_tendsto_of_le_of_le
    (h := fun i ↦ ∫⁻ x, ∫⁻ y, ‖i y - g y‖ₑ ∂η x ∂κ a)
    tendsto_const_nhds ?_ (fun _ ↦ 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 α β
η : Kernel β γ
inst_1 : 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 γ) x) fun (y : γ) ↦
            (↑(↑i : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) y -
              (↑(↑g : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) y) ∂(κ : (a : α) → Measure β) a)
    fun (i : ↥(Lp E 1 ((η ∘ₖ κ : (a : α) → Measure γ) a))) ↦
    ∫⁻ (x : β),
      ∫⁻ (y : γ),
        ‖(↑(↑i : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) y -
            (↑(↑g : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E)
              y‖ₑ ∂(η : (a : β) → Measure γ) x ∂(κ : (a : α) → Measure β) a

Tactic:
fun _ ↦ lintegral_mono fun _ ↦ enorm_integral_le_lintegral_enorm _

Premises used: MeasureTheory.AEEqFun.cast, HSub.hSub, MeasureTheory.enorm_integral_le_lintegral_enorm, 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 α β
η : Kernel β γ
inst_1 : 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 γ) x) fun (y : γ) ↦
            (↑(↑i : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) y -
              (↑(↑g : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) y) ∂(κ : (a : α) → Measure β) a)
    fun (i : ↥(Lp E 1 ((η ∘ₖ κ : (a : α) → Measure γ) a))) ↦
    ∫⁻ (x : β),
      ∫⁻ (y : γ),
        ‖(↑(↑i : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E) y -
            (↑(↑g : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E)
              y‖ₑ ∂(η : (a : β) → Measure γ) x ∂(κ : (a : α) → Measure β) a

Tactic:
exact fun _ ↦ lintegral_mono fun _ ↦ 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 α β
η : Kernel β γ
inst_1 : 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 (i : γ →₁[(η ∘ₖ κ) a] E) : 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 α β
η : Kernel β γ
inst_1 : 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_1 :
  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) y -
              (↑(↑g : γ →ₘ[(η ∘ₖ κ : (a : α) → Measure γ) a] E) : γ → E)
                y‖ₑ ∂(η : (a : β) → Measure γ) x ∂(κ : (a : α) → Measure β) a)
    (𝓝 g) (𝓝 0)

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

Premises used: ProbabilityTheory.Kernel.lintegral_comp, ENNReal.ofReal_zero, MeasureTheory.L1.ofReal_norm_sub_eq_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 α β
η : Kernel β γ
inst_1 : 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 (tendsto_iff_norm_sub_tendsto_zero.1 tendsto_id)

Premises used: ENNReal.ofNNReal, ENNReal.ofReal, Filter.tendsto_id, ENNReal.continuous_ofReal, WithTop.some, Continuous.tendsto, Iff.mp, Filter.Tendsto.comp, OfNat.ofNat, 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 α β
η : Kernel β γ
inst_1 : 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:
exact (continuous_ofReal.tendsto 0).comp (tendsto_iff_norm_sub_tendsto_zero.1 tendsto_id)

Premises used: Filter.tendsto_id, ENNReal.continuous_ofReal, Continuous.tendsto, Iff.mp, Filter.Tendsto.comp, OfNat.ofNat, 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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
pos :
  ∀ {f : γ → E} (hE : CompleteSpace E),
    @Integrable _ _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a) →
      Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (z : γ) ↦ f z)
        (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
          @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
neg :
  ∀ {f : γ → E} (hE : ¬CompleteSpace E),
    @Integrable _ _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a) →
      Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (z : γ) ↦ f z)
        (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
          @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
⊢ ∀ {f : γ → E},
    @Integrable _ _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a) →
      Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (z : γ) ↦ f z)
        (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
          @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f 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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
f : γ → E
hE : ¬CompleteSpace E
⊢ @Integrable _ _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a) →
    Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (z : γ) ↦ f z)
      (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
        @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f 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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
f : γ → E
hE : CompleteSpace E
c : E
s : Set γ
hs : MeasurableSet s
ms : 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 γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s))
      c
⊢ Eq.{u_4 + 1} (α := E)
    (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (z : γ) ↦ s.indicator (fun (x : γ) ↦ c) z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ s.indicator (fun (x : γ) ↦ c) y)

Tactic:
simp_rw [integral_indicator hs, MeasureTheory.setIntegral_const, integral_smul_const,
      measureReal_def]

Premises used: MeasureTheory.integral_indicator, integral_smul_const, MeasureTheory.measureReal_def, 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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
f : γ → E
hE : CompleteSpace E
c : E
s : Set γ
hs : MeasurableSet s
ms : 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 γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) 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 γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s))
      c

Tactic:
congr
-- 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
hE : CompleteSpace E
c : E
s : Set γ
hs : MeasurableSet s
ms : LT.lt (α := ℝ≥0∞) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
pos :
  AEMeasurable (β := ℝ≥0∞) (_m := mβ) (fun (x : β) ↦ (((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s)
    ((κ : (a : α) → Measure β) a)
pos₁ :
  ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    LT.lt (α := ℝ≥0∞) ((((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ENNReal.toReal ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s) =
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      ENNReal.toReal ((((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s)

Tactic:
rw [integral_toReal, Kernel.comp_apply' _ _ _ hs]

Premises used: ProbabilityTheory.Kernel.comp_apply', 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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
f : γ → E
hE : CompleteSpace E
c : E
s : Set γ
hs : MeasurableSet s
ms : LT.lt (α := ℝ≥0∞) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ AEMeasurable (β := ℝ≥0∞) (_m := mβ) (fun (x : β) ↦ (((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s)
    ((κ : (a : α) → Measure β) a)

Tactic:
(Kernel.measurable_coe _ hs).aemeasurable

Premises used: Measurable.aemeasurable, ProbabilityTheory.Kernel.measurable_coe
-- 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
hE : CompleteSpace E
c : E
s : Set γ
hs : MeasurableSet s
ms : LT.lt (α := ℝ≥0∞) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ AEMeasurable (β := ℝ≥0∞) (_m := mβ) (fun (x : β) ↦ (((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s)
    ((κ : (a : α) → Measure β) a)

Tactic:
exact (Kernel.measurable_coe _ hs).aemeasurable

Premises used: Measurable.aemeasurable, ProbabilityTheory.Kernel.measurable_coe
-- 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
hE : CompleteSpace E
c : E
s : Set γ
hs : MeasurableSet s
ms : LT.lt (α := ℝ≥0∞) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    LT.lt (α := ℝ≥0∞) ((((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
ae_lt_top_of_comp_ne_top a ms.ne

Premises used: ProbabilityTheory.Kernel.ae_lt_top_of_comp_ne_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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
f : γ → E
hE : CompleteSpace E
c : E
s : Set γ
hs : MeasurableSet s
ms : LT.lt (α := ℝ≥0∞) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    LT.lt (α := ℝ≥0∞) ((((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact ae_lt_top_of_comp_ne_top a ms.ne

Premises used: ProbabilityTheory.Kernel.ae_lt_top_of_comp_ne_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 α β
η : Kernel β γ
inst_1 : NormedSpace ℝ E
f_1 : γ → E
hE : CompleteSpace E
f g : γ → E
i_f : @Integrable _ _ _ _ mγ f ((η ∘ₖ κ : (a : α) → Measure γ) a)
i_g : @Integrable _ _ _ _ mγ g ((η ∘ₖ κ : (a : α) → Measure γ) a)
hf :
  Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (z : γ) ↦ f z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ f y)
hg :
  Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (z : γ) ↦ g z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ g y)
pos :
  HAdd.hAdd (α := E) (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (a : γ) ↦ f a)
      (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (a : γ) ↦ g a) =
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (z : γ) ↦ (f + g) z
pos₁ :
  HAdd.hAdd (α := E) (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (a : γ) ↦ f a)
      (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (a : γ) ↦ g a) =
    HAdd.hAdd (α := E)
      (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
        @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (a : γ) ↦ f a)
      (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
        @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (a : γ) ↦ g a)
pos₂ :
  HAdd.hAdd (α := E)
      (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
        @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (a : γ) ↦ f a)
      (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (a : γ) ↦ g a) =
    HAdd.hAdd (α := E)
      (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
        @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (a : γ) ↦ f a)
      (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
        @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (a : γ) ↦ g a)
⊢ Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η ∘ₖ κ : (a : α) → Measure γ) a) fun (z : γ) ↦ (f + g) z)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (x : β) ↦
      @integral _ _ _ _ mγ ((η : (a : β) → Measure γ) x) fun (y : γ) ↦ (f + g) y)

Tactic:
simp_rw [integral_add' i_f i_g, integral_integral_add'_comp i_f i_g, hf, hg]

Premises used: MeasureTheory.integral_add', ProbabilityTheory.Kernel.integral_integral_add'_comp