awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
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
E' : Type u_5
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace ℝ E'
f g : β × γ → E
F : E → E'
hf : @Integrable _ _ _ _ Prod.instMeasurableSpace f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
hg : @Integrable _ _ _ _ Prod.instMeasurableSpace g ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
⊢ EventuallyEq.{u_2, u_5} (β := E') (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β))
    (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)))
have 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)))
Tactic: filter_upwards [hf.ae_of_compProd, hg.ae_of_compProd] with _ h2f h2g
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
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)
⊢ ∫⁻ (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
have 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)))
Tactic: refine lintegral_congr_ae ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
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)
⊢ (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)))
have 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)))
Tactic: filter_upwards [hf.ae_of_compProd, hg.ae_of_compProd] with _ h2f h2g
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
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
⊢ 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)
have 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
Tactic: rw [continuous_iff_continuousAt]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
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
have 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)
Tactic: refine
    tendsto_integral_of_L1 _ (L1.integrable_coeFn g).integral_compProd.aestronglyMeasurable
      (Eventually.of_forall fun h => (L1.integrable_coeFn h).integral_compProd) ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
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 (β := ℝ≥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)
have 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)
Tactic: simp_rw [← lintegral_fn_integral_sub (‖·‖ₑ) (L1.integrable_coeFn _) (L1.integrable_coeFn g)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
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 (β := ℝ≥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)
have apply : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)) → ℝ≥0∞
Tactic: apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds _ (fun i => zero_le) _
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
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∞
⊢ 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)
have 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)
Tactic: apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds _ (fun i => zero_le) _
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
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)
⊢ 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)
have 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
Tactic: apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds _ (fun i => zero_le) _
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (hypothesis)
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 (β := ℝ≥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)
have 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‖ₑ
Tactic: have this (i : Lp (α := β × γ) E 1 (((κ ⊗ₖ η) a) : Measure (β × γ))) :
      Measurable fun z => ‖i z - g z‖ₑ :=
    ((Lp.stronglyMeasurable i).sub (Lp.stronglyMeasurable g)).enorm
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
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 (β := ℝ≥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)
have simp_rw : Tendsto (fun (i : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a))) ↦ ENNReal.ofReal ‖i - g‖) (𝓝 g)
  (𝓝 (ENNReal.ofReal 0))
Tactic: simp_rw [← lintegral_compProd _ _ _ (this _), ← L1.ofReal_norm_sub_eq_lintegral, ← ofReal_zero]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
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))
have refine : Tendsto (β := ℝ) (fun (i : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a))) ↦ ‖i - g‖) (𝓝 g) (𝓝 0)
Tactic: refine (continuous_ofReal.tendsto 0).comp ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
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) (𝓝 0)
have rw : Tendsto (fun (i : ↥(Lp E 1 ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a))) ↦ i) (𝓝 g) (𝓝 g)
Tactic: rw [← tendsto_iff_norm_sub_tendsto_zero]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
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},
    @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))
have 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))
Tactic: by_cases hE : CompleteSpace E
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
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))
⊢ ∀ {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))
have 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))
Tactic: by_cases hE : CompleteSpace E
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
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))
have pos : ∀ (c : E) ⦃s : Set (β × γ)⦄,
  MeasurableSet s →
    LT.lt (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
        (∞ : ℝ≥0∞) →
      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: apply Integrable.induction