case pos
α : Type ?u.20404
β : Type u_2
ι : Type ?u.20410
E : Type u_1
F : Type ?u.20416
𝕜 : Type ?u.20419
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
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 : snorm (fun x => f x - y₀) p μ < ⊤
hp_zero : p = 0
⊢ Tendsto (fun n => snorm (↑(approxOn f hf s y₀ h₀ n) - f) p μ) atTop (𝓝 0)

case neg
α : Type ?u.20404
β : Type u_2
ι : Type ?u.20410
E : Type u_1
F : Type ?u.20416
𝕜 : Type ?u.20419
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
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 : snorm (fun x => f x - y₀) p μ < ⊤
hp_zero : ¬p = 0
⊢ Tendsto (fun n => snorm (↑(approxOn f hf s y₀ h₀ n) - f) p μ) atTop (𝓝 0)
α : Type ?u.20404
β : Type u_2
ι : Type ?u.20410
E : Type u_1
F : Type ?u.20416
𝕜 : Type ?u.20419
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
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 : snorm (fun x => f x - y₀) p μ < ⊤
⊢ Tendsto (fun n => snorm (↑(approxOn f hf s y₀ h₀ n) - f) p μ) atTop (𝓝 0)
by_cases hp_zero : p = 0
case neg
α : Type ?u.20404
β : Type u_2
ι : Type ?u.20410
E : Type u_1
F : Type ?u.20416
𝕜 : Type ?u.20419
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
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 : snorm (fun x => f x - y₀) p μ < ⊤
hp_zero : ¬p = 0
hp : 0 < ENNReal.toReal p
⊢ Tendsto (fun n => snorm (↑(approxOn f hf s y₀ h₀ n) - f) p μ) atTop (𝓝 0)
case neg
α : Type ?u.20404
β : Type u_2
ι : Type ?u.20410
E : Type u_1
F : Type ?u.20416
𝕜 : Type ?u.20419
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
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 : snorm (fun x => f x - y₀) p μ < ⊤
hp_zero : ¬p = 0
⊢ Tendsto (fun n => snorm (↑(approxOn f hf s y₀ h₀ n) - f) p μ) atTop (𝓝 0)
have hp : 0 < p.toReal := toReal_pos hp_zero hp_ne_top
case neg
α : Type ?u.20404
β : Type u_2
ι : Type ?u.20410
E : Type u_1
F : Type ?u.20416
𝕜 : Type ?u.20419
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
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 : snorm (fun x => f x - y₀) p μ < ⊤
hp_zero : ¬p = 0
hp : 0 < ENNReal.toReal p
⊢ Tendsto (fun n => ∫⁻ (x : β), ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p ∂μ) atTop (𝓝 0)
case neg
α : Type ?u.20404
β : Type u_2
ι : Type ?u.20410
E : Type u_1
F : Type ?u.20416
𝕜 : Type ?u.20419
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
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 : snorm (fun x => f x - y₀) p μ < ⊤
hp_zero : ¬p = 0
hp : 0 < ENNReal.toReal p
⊢ Tendsto (fun n => snorm (↑(approxOn f hf s y₀ h₀ n) - f) p μ) atTop (𝓝 0)
suffices
    Tendsto (fun n => ∫⁻ x, (‖approxOn f hf s y₀ h₀ n x - f x‖₊ : ℝ≥0∞) ^ p.toReal ∂μ) atTop
      (𝓝 0) by
  simp only [snorm_eq_lintegral_rpow_nnnorm hp_zero hp_ne_top]
  convert continuous_rpow_const.continuousAt.tendsto.comp this
  simp [zero_rpow_of_pos (_root_.inv_pos.mpr hp)]
case neg
α : Type ?u.20404
β : Type u_2
ι : Type ?u.20410
E : Type u_1
F : Type ?u.20416
𝕜 : Type ?u.20419
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
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 : snorm (fun x => f x - y₀) p μ < ⊤
hp_zero : ¬p = 0
hp : 0 < ENNReal.toReal p
hF_meas : ∀ (n : ℕ), Measurable fun x => ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p
⊢ Tendsto (fun n => ∫⁻ (x : β), ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p ∂μ) atTop (𝓝 0)
case neg
α : Type ?u.20404
β : Type u_2
ι : Type ?u.20410
E : Type u_1
F : Type ?u.20416
𝕜 : Type ?u.20419
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
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 : snorm (fun x => f x - y₀) p μ < ⊤
hp_zero : ¬p = 0
hp : 0 < ENNReal.toReal p
⊢ Tendsto (fun n => ∫⁻ (x : β), ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p ∂μ) atTop (𝓝 0)
have hF_meas :
  ∀ n, Measurable fun x => (‖approxOn f hf s y₀ h₀ n x - f x‖₊ : ℝ≥0∞) ^ p.toReal := by
  simpa only [← edist_eq_coe_nnnorm_sub] using fun n =>
    (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
case neg
α : Type ?u.20404
β : Type u_2
ι : Type ?u.20410
E : Type u_1
F : Type ?u.20416
𝕜 : Type ?u.20419
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
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 : snorm (fun x => f x - y₀) p μ < ⊤
hp_zero : ¬p = 0
hp : 0 < ENNReal.toReal p
hF_meas : ∀ (n : ℕ), Measurable fun x => ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p
h_bound :
  ∀ (n : ℕ),
    (fun x => ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p) ≤ᵐ[μ] fun x => ↑‖f x - y₀‖₊ ^ ENNReal.toReal p
⊢ Tendsto (fun n => ∫⁻ (x : β), ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p ∂μ) atTop (𝓝 0)
case neg
α : Type ?u.20404
β : Type u_2
ι : Type ?u.20410
E : Type u_1
F : Type ?u.20416
𝕜 : Type ?u.20419
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
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 : snorm (fun x => f x - y₀) p μ < ⊤
hp_zero : ¬p = 0
hp : 0 < ENNReal.toReal p
hF_meas : ∀ (n : ℕ), Measurable fun x => ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p
⊢ Tendsto (fun n => ∫⁻ (x : β), ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p ∂μ) atTop (𝓝 0)
have h_bound :
  ∀ n, (fun x => (‖approxOn f hf s y₀ h₀ n x - f x‖₊ : ℝ≥0∞) ^ p.toReal) ≤ᵐ[μ] fun x =>
      (‖f x - y₀‖₊ : ℝ≥0∞) ^ p.toReal :=
  fun n =>
  eventually_of_forall fun x =>
    rpow_le_rpow (coe_mono (nnnorm_approxOn_le hf h₀ x n)) toReal_nonneg
case neg
α : Type ?u.20404
β : Type u_2
ι : Type ?u.20410
E : Type u_1
F : Type ?u.20416
𝕜 : Type ?u.20419
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
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 : snorm (fun x => f x - y₀) p μ < ⊤
hp_zero : ¬p = 0
hp : 0 < ENNReal.toReal p
hF_meas : ∀ (n : ℕ), Measurable fun x => ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p
h_bound :
  ∀ (n : ℕ),
    (fun x => ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p) ≤ᵐ[μ] fun x => ↑‖f x - y₀‖₊ ^ ENNReal.toReal p
h_fin : (∫⁻ (a : β), ↑‖f a - y₀‖₊ ^ ENNReal.toReal p ∂μ) ≠ ⊤
⊢ Tendsto (fun n => ∫⁻ (x : β), ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p ∂μ) atTop (𝓝 0)
case neg
α : Type ?u.20404
β : Type u_2
ι : Type ?u.20410
E : Type u_1
F : Type ?u.20416
𝕜 : Type ?u.20419
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
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 : snorm (fun x => f x - y₀) p μ < ⊤
hp_zero : ¬p = 0
hp : 0 < ENNReal.toReal p
hF_meas : ∀ (n : ℕ), Measurable fun x => ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p
h_bound :
  ∀ (n : ℕ),
    (fun x => ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p) ≤ᵐ[μ] fun x => ↑‖f x - y₀‖₊ ^ ENNReal.toReal p
⊢ Tendsto (fun n => ∫⁻ (x : β), ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p ∂μ) atTop (𝓝 0)
have h_fin : (∫⁻ a : β, (‖f a - y₀‖₊ : ℝ≥0∞) ^ p.toReal ∂μ) ≠ ⊤ :=
  (lintegral_rpow_nnnorm_lt_top_of_snorm_lt_top hp_zero hp_ne_top hi).ne
case neg
α : Type ?u.20404
β : Type u_2
ι : Type ?u.20410
E : Type u_1
F : Type ?u.20416
𝕜 : Type ?u.20419
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
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 : snorm (fun x => f x - y₀) p μ < ⊤
hp_zero : ¬p = 0
hp : 0 < ENNReal.toReal p
hF_meas : ∀ (n : ℕ), Measurable fun x => ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p
h_bound :
  ∀ (n : ℕ),
    (fun x => ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p) ≤ᵐ[μ] fun x => ↑‖f x - y₀‖₊ ^ ENNReal.toReal p
h_fin : (∫⁻ (a : β), ↑‖f a - y₀‖₊ ^ ENNReal.toReal p ∂μ) ≠ ⊤
h_lim : ∀ᵐ (a : β) ∂μ, Tendsto (fun n => ↑‖↑(approxOn f hf s y₀ h₀ n) a - f a‖₊ ^ ENNReal.toReal p) atTop (𝓝 0)
⊢ Tendsto (fun n => ∫⁻ (x : β), ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p ∂μ) atTop (𝓝 0)
case neg
α : Type ?u.20404
β : Type u_2
ι : Type ?u.20410
E : Type u_1
F : Type ?u.20416
𝕜 : Type ?u.20419
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
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 : snorm (fun x => f x - y₀) p μ < ⊤
hp_zero : ¬p = 0
hp : 0 < ENNReal.toReal p
hF_meas : ∀ (n : ℕ), Measurable fun x => ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p
h_bound :
  ∀ (n : ℕ),
    (fun x => ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p) ≤ᵐ[μ] fun x => ↑‖f x - y₀‖₊ ^ ENNReal.toReal p
h_fin : (∫⁻ (a : β), ↑‖f a - y₀‖₊ ^ ENNReal.toReal p ∂μ) ≠ ⊤
⊢ Tendsto (fun n => ∫⁻ (x : β), ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p ∂μ) atTop (𝓝 0)
have h_lim :
  ∀ᵐ a : β ∂μ,
    Tendsto (fun n => (‖approxOn f hf s y₀ h₀ n a - f a‖₊ : ℝ≥0∞) ^ p.toReal) atTop (𝓝 0) := by
  filter_upwards [hμ] with a ha
  have : Tendsto (fun n => (approxOn f hf s y₀ h₀ n) a - f a) atTop (𝓝 (f a - f a)) :=
    (tendsto_approxOn hf h₀ ha).sub tendsto_const_nhds
  convert continuous_rpow_const.continuousAt.tendsto.comp (tendsto_coe.mpr this.nnnorm)
  simp [zero_rpow_of_pos hp]
no goals
case neg
α : Type ?u.20404
β : Type u_2
ι : Type ?u.20410
E : Type u_1
F : Type ?u.20416
𝕜 : Type ?u.20419
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
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 : snorm (fun x => f x - y₀) p μ < ⊤
hp_zero : ¬p = 0
hp : 0 < ENNReal.toReal p
hF_meas : ∀ (n : ℕ), Measurable fun x => ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p
h_bound :
  ∀ (n : ℕ),
    (fun x => ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p) ≤ᵐ[μ] fun x => ↑‖f x - y₀‖₊ ^ ENNReal.toReal p
h_fin : (∫⁻ (a : β), ↑‖f a - y₀‖₊ ^ ENNReal.toReal p ∂μ) ≠ ⊤
h_lim : ∀ᵐ (a : β) ∂μ, Tendsto (fun n => ↑‖↑(approxOn f hf s y₀ h₀ n) a - f a‖₊ ^ ENNReal.toReal p) atTop (𝓝 0)
⊢ Tendsto (fun n => ∫⁻ (x : β), ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p ∂μ) atTop (𝓝 0)
simpa using tendsto_lintegral_of_dominated_convergence _ hF_meas h_bound h_fin h_lim
no goals
case pos
α : Type ?u.20404
β : Type u_2
ι : Type ?u.20410
E : Type u_1
F : Type ?u.20416
𝕜 : Type ?u.20419
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
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 : snorm (fun x => f x - y₀) p μ < ⊤
hp_zero : p = 0
⊢ Tendsto (fun n => snorm (↑(approxOn f hf s y₀ h₀ n) - f) p μ) atTop (𝓝 0)
simpa only [hp_zero, snorm_exponent_zero] using tendsto_const_nhds
α : Type ?u.20404
β : Type u_2
ι : Type ?u.20410
E : Type u_1
F : Type ?u.20416
𝕜 : Type ?u.20419
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
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 : snorm (fun x => f x - y₀) p μ < ⊤
hp_zero : ¬p = 0
hp : 0 < ENNReal.toReal p
this : Tendsto (fun n => ∫⁻ (x : β), ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p ∂μ) atTop (𝓝 0)
⊢ Tendsto (fun n => (∫⁻ (x : β), ↑‖(↑(approxOn f hf s y₀ h₀ n) - f) x‖₊ ^ ENNReal.toReal p ∂μ) ^ (1 / ENNReal.toReal p))
    atTop (𝓝 0)
α : Type ?u.20404
β : Type u_2
ι : Type ?u.20410
E : Type u_1
F : Type ?u.20416
𝕜 : Type ?u.20419
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
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 : snorm (fun x => f x - y₀) p μ < ⊤
hp_zero : ¬p = 0
hp : 0 < ENNReal.toReal p
this : Tendsto (fun n => ∫⁻ (x : β), ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p ∂μ) atTop (𝓝 0)
⊢ Tendsto (fun n => snorm (↑(approxOn f hf s y₀ h₀ n) - f) p μ) atTop (𝓝 0)
simp only [snorm_eq_lintegral_rpow_nnnorm hp_zero hp_ne_top]
case h.e'_5.h.e'_3
α : Type ?u.20404
β : Type u_2
ι : Type ?u.20410
E : Type u_1
F : Type ?u.20416
𝕜 : Type ?u.20419
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
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 : snorm (fun x => f x - y₀) p μ < ⊤
hp_zero : ¬p = 0
hp : 0 < ENNReal.toReal p
this : Tendsto (fun n => ∫⁻ (x : β), ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p ∂μ) atTop (𝓝 0)
⊢ 0 = 0 ^ (1 / ENNReal.toReal p)
α : Type ?u.20404
β : Type u_2
ι : Type ?u.20410
E : Type u_1
F : Type ?u.20416
𝕜 : Type ?u.20419
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
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 : snorm (fun x => f x - y₀) p μ < ⊤
hp_zero : ¬p = 0
hp : 0 < ENNReal.toReal p
this : Tendsto (fun n => ∫⁻ (x : β), ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p ∂μ) atTop (𝓝 0)
⊢ Tendsto (fun n => (∫⁻ (x : β), ↑‖(↑(approxOn f hf s y₀ h₀ n) - f) x‖₊ ^ ENNReal.toReal p ∂μ) ^ (1 / ENNReal.toReal p))
    atTop (𝓝 0)
convert continuous_rpow_const.continuousAt.tendsto.comp this
no goals
case h.e'_5.h.e'_3
α : Type ?u.20404
β : Type u_2
ι : Type ?u.20410
E : Type u_1
F : Type ?u.20416
𝕜 : Type ?u.20419
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
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 : snorm (fun x => f x - y₀) p μ < ⊤
hp_zero : ¬p = 0
hp : 0 < ENNReal.toReal p
this : Tendsto (fun n => ∫⁻ (x : β), ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p ∂μ) atTop (𝓝 0)
⊢ 0 = 0 ^ (1 / ENNReal.toReal p)
simp [zero_rpow_of_pos (_root_.inv_pos.mpr hp)]
no goals
α : Type ?u.20404
β : Type u_2
ι : Type ?u.20410
E : Type u_1
F : Type ?u.20416
𝕜 : Type ?u.20419
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
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 : snorm (fun x => f x - y₀) p μ < ⊤
hp_zero : ¬p = 0
hp : 0 < ENNReal.toReal p
⊢ ∀ (n : ℕ), Measurable fun x => ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p
simpa only [← edist_eq_coe_nnnorm_sub] using fun n =>
  (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
case h
α : Type ?u.20404
β : Type u_2
ι : Type ?u.20410
E : Type u_1
F : Type ?u.20416
𝕜 : Type ?u.20419
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
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 : snorm (fun x => f x - y₀) p μ < ⊤
hp_zero : ¬p = 0
hp : 0 < ENNReal.toReal p
hF_meas : ∀ (n : ℕ), Measurable fun x => ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p
h_bound :
  ∀ (n : ℕ),
    (fun x => ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p) ≤ᵐ[μ] fun x => ↑‖f x - y₀‖₊ ^ ENNReal.toReal p
h_fin : (∫⁻ (a : β), ↑‖f a - y₀‖₊ ^ ENNReal.toReal p ∂μ) ≠ ⊤
a : β
ha : f a ∈ closure s
⊢ Tendsto (fun n => ↑‖↑(approxOn f hf s y₀ h₀ n) a - f a‖₊ ^ ENNReal.toReal p) atTop (𝓝 0)
α : Type ?u.20404
β : Type u_2
ι : Type ?u.20410
E : Type u_1
F : Type ?u.20416
𝕜 : Type ?u.20419
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
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 : snorm (fun x => f x - y₀) p μ < ⊤
hp_zero : ¬p = 0
hp : 0 < ENNReal.toReal p
hF_meas : ∀ (n : ℕ), Measurable fun x => ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p
h_bound :
  ∀ (n : ℕ),
    (fun x => ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p) ≤ᵐ[μ] fun x => ↑‖f x - y₀‖₊ ^ ENNReal.toReal p
h_fin : (∫⁻ (a : β), ↑‖f a - y₀‖₊ ^ ENNReal.toReal p ∂μ) ≠ ⊤
⊢ ∀ᵐ (a : β) ∂μ, Tendsto (fun n => ↑‖↑(approxOn f hf s y₀ h₀ n) a - f a‖₊ ^ ENNReal.toReal p) atTop (𝓝 0)
filter_upwards [hμ] with a ha
case h
α : Type ?u.20404
β : Type u_2
ι : Type ?u.20410
E : Type u_1
F : Type ?u.20416
𝕜 : Type ?u.20419
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
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 : snorm (fun x => f x - y₀) p μ < ⊤
hp_zero : ¬p = 0
hp : 0 < ENNReal.toReal p
hF_meas : ∀ (n : ℕ), Measurable fun x => ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p
h_bound :
  ∀ (n : ℕ),
    (fun x => ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p) ≤ᵐ[μ] fun x => ↑‖f x - y₀‖₊ ^ ENNReal.toReal p
h_fin : (∫⁻ (a : β), ↑‖f a - y₀‖₊ ^ ENNReal.toReal p ∂μ) ≠ ⊤
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))
⊢ Tendsto (fun n => ↑‖↑(approxOn f hf s y₀ h₀ n) a - f a‖₊ ^ ENNReal.toReal p) atTop (𝓝 0)
case h
α : Type ?u.20404
β : Type u_2
ι : Type ?u.20410
E : Type u_1
F : Type ?u.20416
𝕜 : Type ?u.20419
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
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 : snorm (fun x => f x - y₀) p μ < ⊤
hp_zero : ¬p = 0
hp : 0 < ENNReal.toReal p
hF_meas : ∀ (n : ℕ), Measurable fun x => ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p
h_bound :
  ∀ (n : ℕ),
    (fun x => ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p) ≤ᵐ[μ] fun x => ↑‖f x - y₀‖₊ ^ ENNReal.toReal p
h_fin : (∫⁻ (a : β), ↑‖f a - y₀‖₊ ^ ENNReal.toReal p ∂μ) ≠ ⊤
a : β
ha : f a ∈ closure s
⊢ Tendsto (fun n => ↑‖↑(approxOn f hf s y₀ h₀ n) a - f a‖₊ ^ ENNReal.toReal p) atTop (𝓝 0)
have : Tendsto (fun n => (approxOn f hf s y₀ h₀ n) a - f a) atTop (𝓝 (f a - f a)) :=
  (tendsto_approxOn hf h₀ ha).sub tendsto_const_nhds
case h.e'_5.h.e'_3
α : Type ?u.20404
β : Type u_2
ι : Type ?u.20410
E : Type u_1
F : Type ?u.20416
𝕜 : Type ?u.20419
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
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 : snorm (fun x => f x - y₀) p μ < ⊤
hp_zero : ¬p = 0
hp : 0 < ENNReal.toReal p
hF_meas : ∀ (n : ℕ), Measurable fun x => ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p
h_bound :
  ∀ (n : ℕ),
    (fun x => ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p) ≤ᵐ[μ] fun x => ↑‖f x - y₀‖₊ ^ ENNReal.toReal p
h_fin : (∫⁻ (a : β), ↑‖f a - y₀‖₊ ^ ENNReal.toReal p ∂μ) ≠ ⊤
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‖₊ ^ ENNReal.toReal p
case h
α : Type ?u.20404
β : Type u_2
ι : Type ?u.20410
E : Type u_1
F : Type ?u.20416
𝕜 : Type ?u.20419
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
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 : snorm (fun x => f x - y₀) p μ < ⊤
hp_zero : ¬p = 0
hp : 0 < ENNReal.toReal p
hF_meas : ∀ (n : ℕ), Measurable fun x => ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p
h_bound :
  ∀ (n : ℕ),
    (fun x => ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p) ≤ᵐ[μ] fun x => ↑‖f x - y₀‖₊ ^ ENNReal.toReal p
h_fin : (∫⁻ (a : β), ↑‖f a - y₀‖₊ ^ ENNReal.toReal p ∂μ) ≠ ⊤
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))
⊢ Tendsto (fun n => ↑‖↑(approxOn f hf s y₀ h₀ n) a - f a‖₊ ^ ENNReal.toReal p) atTop (𝓝 0)
convert continuous_rpow_const.continuousAt.tendsto.comp (tendsto_coe.mpr this.nnnorm)
no goals
case h.e'_5.h.e'_3
α : Type ?u.20404
β : Type u_2
ι : Type ?u.20410
E : Type u_1
F : Type ?u.20416
𝕜 : Type ?u.20419
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
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 : snorm (fun x => f x - y₀) p μ < ⊤
hp_zero : ¬p = 0
hp : 0 < ENNReal.toReal p
hF_meas : ∀ (n : ℕ), Measurable fun x => ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p
h_bound :
  ∀ (n : ℕ),
    (fun x => ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ ENNReal.toReal p) ≤ᵐ[μ] fun x => ↑‖f x - y₀‖₊ ^ ENNReal.toReal p
h_fin : (∫⁻ (a : β), ↑‖f a - y₀‖₊ ^ ENNReal.toReal p ∂μ) ≠ ⊤
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‖₊ ^ ENNReal.toReal p
simp [zero_rpow_of_pos hp]