-- Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
theorem tendsto_approxOn_Lp_eLpNorm [OpensMeasurableSpace E] {f : β → E} (hf : Measurable f)
    {s : Set E} {y₀ : E} (h₀ : y₀ ∈ s) [SeparableSpace s] (hp_ne_top : p ≠ ∞) {μ : Measure β}
    (hμ : ∀ᵐ x ∂μ, f x ∈ closure s) (hi : eLpNorm (fun x => f x - y₀) p μ < ∞) :
    Tendsto (fun n => eLpNorm (⇑(approxOn f hf s y₀ h₀ n) - f) p μ) atTop (𝓝 0)

Proof state:
case neg
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hp_ne_top : p ≠ ⊤
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure s
hi : eLpNorm (fun x => f x - y₀) p μ < ⊤
hp_zero : ¬p = 0
hp : 0 < p.toReal
hF_meas : ∀ (n : ℕ), Measurable fun x => ‖(approxOn f hf s y₀ h₀ n) x - f x‖ₑ ^ p.toReal
h_bound : ∀ (n : ℕ), (fun x => ‖(approxOn f hf s y₀ h₀ n) x - f x‖ₑ ^ p.toReal) ≤ᶠ[ae μ] fun x => ‖f x - y₀‖ₑ ^ p.toReal
h_fin : ∫⁻ (a : β), ‖f a - y₀‖ₑ ^ p.toReal ∂μ ≠ ⊤
h_lim : ∀ᵐ (a : β) ∂μ, Tendsto (fun x => ‖(approxOn f hf s y₀ h₀ x) a - f a‖ₑ ^ p.toReal) atTop (𝓝 0)
⊢ Tendsto (fun n => ∫⁻ (x : β), ‖(approxOn f hf s y₀ h₀ n) x - f x‖ₑ ^ p.toReal ∂μ) atTop (𝓝 0)

Tactic:
simpa using tendsto_lintegral_of_dominated_convergence _ hF_meas h_bound h_fin h_lim

Result:
no goals

Proof state:
case h.e'_5.h.e'_3
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hp_ne_top : p ≠ ⊤
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure s
hi : eLpNorm (fun x => f x - y₀) p μ < ⊤
hp_zero : ¬p = 0
hp : 0 < p.toReal
hF_meas : ∀ (n : ℕ), Measurable fun x => ‖(approxOn f hf s y₀ h₀ n) x - f x‖ₑ ^ p.toReal
h_bound : ∀ (n : ℕ), (fun x => ‖(approxOn f hf s y₀ h₀ n) x - f x‖ₑ ^ p.toReal) ≤ᶠ[ae μ] fun x => ‖f x - y₀‖ₑ ^ p.toReal
h_fin : ∫⁻ (a : β), ‖f a - y₀‖ₑ ^ p.toReal ∂μ ≠ ⊤
a : β
ha : f a ∈ closure s
this : Tendsto (fun n => (approxOn f hf s y₀ h₀ n) a - f a) atTop (𝓝 (f a - f a))
⊢ 0 = ↑‖f a - f a‖₊ ^ p.toReal

Tactic:
simp [zero_rpow_of_pos hp]

Result:
no goals

Proof state:
case neg
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hp_ne_top : p ≠ ⊤
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure s
hi : eLpNorm (fun x => f x - y₀) p μ < ⊤
hp_zero : ¬p = 0
⊢ Tendsto (fun n => eLpNorm (⇑(approxOn f hf s y₀ h₀ n) - f) p μ) atTop (𝓝 0)

Tactic:
have hp : 0 < p.toReal := toReal_pos hp_zero hp_ne_top

Result:
case neg
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hp_ne_top : p ≠ ⊤
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure s
hi : eLpNorm (fun x => f x - y₀) p μ < ⊤
hp_zero : ¬p = 0
hp : 0 < p.toReal
⊢ Tendsto (fun n => eLpNorm (⇑(approxOn f hf s y₀ h₀ n) - f) p μ) atTop (𝓝 0)

Proof state:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hp_ne_top : p ≠ ⊤
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure s
hi : eLpNorm (fun x => f x - y₀) p μ < ⊤
⊢ Tendsto (fun n => eLpNorm (⇑(approxOn f hf s y₀ h₀ n) - f) p μ) atTop (𝓝 0)

Tactic:
by_cases hp_zero : p = 0

Result:
case pos
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hp_ne_top : p ≠ ⊤
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure s
hi : eLpNorm (fun x => f x - y₀) p μ < ⊤
hp_zero : p = 0
⊢ Tendsto (fun n => eLpNorm (⇑(approxOn f hf s y₀ h₀ n) - f) p μ) atTop (𝓝 0)

case neg
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hp_ne_top : p ≠ ⊤
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure s
hi : eLpNorm (fun x => f x - y₀) p μ < ⊤
hp_zero : ¬p = 0
⊢ Tendsto (fun n => eLpNorm (⇑(approxOn f hf s y₀ h₀ n) - f) p μ) atTop (𝓝 0)

Proof state:
case neg
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hp_ne_top : p ≠ ⊤
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure s
hi : eLpNorm (fun x => f x - y₀) p μ < ⊤
hp_zero : ¬p = 0
hp : 0 < p.toReal
⊢ Tendsto (fun n => ∫⁻ (x : β), ‖(approxOn f hf s y₀ h₀ n) x - f x‖ₑ ^ p.toReal ∂μ) atTop (𝓝 0)

Tactic:
have hF_meas n : Measurable fun x => ‖approxOn f hf s y₀ h₀ n x - f x‖ₑ ^ p.toReal := by
  simpa only [← edist_eq_enorm_sub] using
    (approxOn f hf s y₀ h₀ n).measurable_bind (fun y x => edist y (f x) ^ p.toReal) fun y =>
      (measurable_edist_right.comp hf).pow_const p.toReal

Result:
case neg
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hp_ne_top : p ≠ ⊤
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure s
hi : eLpNorm (fun x => f x - y₀) p μ < ⊤
hp_zero : ¬p = 0
hp : 0 < p.toReal
hF_meas : ∀ (n : ℕ), Measurable fun x => ‖(approxOn f hf s y₀ h₀ n) x - f x‖ₑ ^ p.toReal
⊢ Tendsto (fun n => ∫⁻ (x : β), ‖(approxOn f hf s y₀ h₀ n) x - f x‖ₑ ^ p.toReal ∂μ) atTop (𝓝 0)

Proof state:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hp_ne_top : p ≠ ⊤
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure s
hi : eLpNorm (fun x => f x - y₀) p μ < ⊤
hp_zero : ¬p = 0
hp : 0 < p.toReal
n : ℕ
⊢ Measurable fun x => ‖(approxOn f hf s y₀ h₀ n) x - f x‖ₑ ^ p.toReal

Tactic:
simpa only [← edist_eq_enorm_sub] using
  (approxOn f hf s y₀ h₀ n).measurable_bind (fun y x => edist y (f x) ^ p.toReal) fun y =>
    (measurable_edist_right.comp hf).pow_const p.toReal

Result:
no goals

Proof state:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hp_ne_top : p ≠ ⊤
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure s
hi : eLpNorm (fun x => f x - y₀) p μ < ⊤
hp_zero : ¬p = 0
hp : 0 < p.toReal
this : Tendsto (fun n => ∫⁻ (x : β), ‖(approxOn f hf s y₀ h₀ n) x - f x‖ₑ ^ p.toReal ∂μ) atTop (𝓝 0)
⊢ Tendsto (fun n => (∫⁻ (x : β), ‖(⇑(approxOn f hf s y₀ h₀ n) - f) x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)) atTop (𝓝 0)

Tactic:
convert continuous_rpow_const.continuousAt.tendsto.comp this

Result:
case h.e'_5.h.e'_3
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hp_ne_top : p ≠ ⊤
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure s
hi : eLpNorm (fun x => f x - y₀) p μ < ⊤
hp_zero : ¬p = 0
hp : 0 < p.toReal
this : Tendsto (fun n => ∫⁻ (x : β), ‖(approxOn f hf s y₀ h₀ n) x - f x‖ₑ ^ p.toReal ∂μ) atTop (𝓝 0)
⊢ 0 = 0 ^ (1 / p.toReal)