-- Mathlib/Probability/Kernel/Composition/IntegralCompProd.lean
theorem Kernel.continuous_integral_integral :
    -- Continuous fun f : α × β →₁[(κ ⊗ₖ η) a] E => ∫ x, ∫ y, f (x, y) ∂η (a, x) ∂κ a

Proof state:
α : 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✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
g : ↥(Lp E 1 ((κ ⊗ₖ η) a))
this : ∀ (i : ↥(Lp E 1 ((κ ⊗ₖ η) a))), Measurable fun z => ‖↑↑i z - ↑↑g z‖ₑ
⊢ Tendsto (fun i => ∫⁻ (x : β), ∫⁻ (y : γ), ‖↑↑i (x, y) - ↑↑g (x, y)‖ₑ ∂η (a, x) ∂κ a) (𝓝 g) (𝓝 0)

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

Result:
α : 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✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
g : ↥(Lp E 1 ((κ ⊗ₖ η) a))
this : ∀ (i : ↥(Lp E 1 ((κ ⊗ₖ η) a))), Measurable fun z => ‖↑↑i z - ↑↑g z‖ₑ
⊢ Tendsto (fun i => ENNReal.ofReal ‖i - g‖) (𝓝 g) (𝓝 (ENNReal.ofReal 0))

Proof state:
α : 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✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
g : ↥(Lp E 1 ((κ ⊗ₖ η) a))
⊢ ↥(Lp E 1 ((κ ⊗ₖ η) a)) → ℝ≥0∞

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

Result:
no goals

Proof state:
α : 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✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
g : ↥(Lp E 1 ((κ ⊗ₖ η) a))
⊢ (fun i => ∫⁻ (x : β), ‖∫ (y : γ), ↑↑i (x, y) - ↑↑g (x, y) ∂η (a, x)‖ₑ ∂κ a) ≤ fun i =>
    ∫⁻ (x : β), ∫⁻ (y : γ), ‖↑↑i (x, y) - ↑↑g (x, y)‖ₑ ∂η (a, x) ∂κ a

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

Result:
no goals

Proof state:
α : 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✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
g : ↥(Lp E 1 ((κ ⊗ₖ η) a))
⊢ Tendsto (fun i => ∫⁻ (x : β), ‖∫ (y : γ), ↑↑i (x, y) - ↑↑g (x, y) ∂η (a, x)‖ₑ ∂κ a) (𝓝 g) (𝓝 0)

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

Result:
α : 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✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
g : ↥(Lp E 1 ((κ ⊗ₖ η) a))
⊢ ↥(Lp E 1 ((κ ⊗ₖ η) a)) → ℝ≥0∞

α : 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✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
g : ↥(Lp E 1 ((κ ⊗ₖ η) a))
⊢ Tendsto ?m.52391 (𝓝 g) (𝓝 0)

α : 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✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
g : ↥(Lp E 1 ((κ ⊗ₖ η) a))
⊢ (fun i => ∫⁻ (x : β), ‖∫ (y : γ), ↑↑i (x, y) - ↑↑g (x, y) ∂η (a, x)‖ₑ ∂κ a) ≤ ?m.52391

Proof state:
α : 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✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
g : ↥(Lp E 1 ((κ ⊗ₖ η) a))
this : ∀ (i : ↥(Lp E 1 ((κ ⊗ₖ η) a))), Measurable fun z => ‖↑↑i z - ↑↑g z‖ₑ
⊢ Tendsto (fun i => ENNReal.ofReal ‖i - g‖) (𝓝 g) (𝓝 (ENNReal.ofReal 0))

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

Result:
α : 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✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
g : ↥(Lp E 1 ((κ ⊗ₖ η) a))
this : ∀ (i : ↥(Lp E 1 ((κ ⊗ₖ η) a))), Measurable fun z => ‖↑↑i z - ↑↑g z‖ₑ
⊢ Tendsto (fun i => ‖i - g‖) (𝓝 g) (𝓝 0)

Proof state:
α : 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✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
g : ↥(Lp E 1 ((κ ⊗ₖ η) a))
this : ∀ (i : ↥(Lp E 1 ((κ ⊗ₖ η) a))), Measurable fun z => ‖↑↑i z - ↑↑g z‖ₑ
⊢ Tendsto (fun i => i) (𝓝 g) (𝓝 g)

Tactic:
exact tendsto_id

Result:
no goals

Proof state:
α : 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✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
g : ↥(Lp E 1 ((κ ⊗ₖ η) a))
this : ∀ (i : ↥(Lp E 1 ((κ ⊗ₖ η) a))), Measurable fun z => ‖↑↑i z - ↑↑g z‖ₑ
⊢ Tendsto (fun i => ‖i - g‖) (𝓝 g) (𝓝 0)

Tactic:
rw [← tendsto_iff_norm_sub_tendsto_zero]

Result:
α : 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✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
g : ↥(Lp E 1 ((κ ⊗ₖ η) a))
this : ∀ (i : ↥(Lp E 1 ((κ ⊗ₖ η) a))), Measurable fun z => ‖↑↑i z - ↑↑g z‖ₑ
⊢ Tendsto (fun i => i) (𝓝 g) (𝓝 g)

Proof state:
α : 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✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
g : ↥(Lp E 1 ((κ ⊗ₖ η) a))
⊢ Tendsto (fun i => ∫⁻ (x : β), ∫⁻ (y : γ), ‖↑↑i (x, y) - ↑↑g (x, y)‖ₑ ∂η (a, x) ∂κ a) (𝓝 g) (𝓝 0)

Tactic:
have this (i : Lp (α := β × γ) E 1 (((κ ⊗ₖ η) a) : Measure (β × γ))) :
    Measurable fun z => ‖i z - g z‖ₑ :=
  ((Lp.stronglyMeasurable i).sub (Lp.stronglyMeasurable g)).enorm

Result:
α : 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✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
g : ↥(Lp E 1 ((κ ⊗ₖ η) a))
this : ∀ (i : ↥(Lp E 1 ((κ ⊗ₖ η) a))), Measurable fun z => ‖↑↑i z - ↑↑g z‖ₑ
⊢ Tendsto (fun i => ∫⁻ (x : β), ∫⁻ (y : γ), ‖↑↑i (x, y) - ↑↑g (x, y)‖ₑ ∂η (a, x) ∂κ a) (𝓝 g) (𝓝 0)

Proof state:
α : 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✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
⊢ Continuous fun f => ∫ (x : β), ∫ (y : γ), ↑↑f (x, y) ∂η (a, x) ∂κ a

Tactic:
rw [continuous_iff_continuousAt]

Result:
α : 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✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
⊢ ∀ (x : ↥(Lp E 1 ((κ ⊗ₖ η) a))), ContinuousAt (fun f => ∫ (x : β), ∫ (y : γ), ↑↑f (x, y) ∂η (a, x) ∂κ a) x