α : Type ?u.604444
β : Type u_2
ι : Type ?u.604450
E : Type u_1
F : Type ?u.604456
𝕜 : Type ?u.604459
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : Memℒp f p
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : Memℒp (fun x => y₀) p
n : ℕ
⊢ snorm (↑(approxOn f fmeas s y₀ h₀ n)) p μ < ⊤
α : Type ?u.604444
β : Type u_2
ι : Type ?u.604450
E : Type u_1
F : Type ?u.604456
𝕜 : Type ?u.604459
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : Memℒp f p
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : Memℒp (fun x => y₀) p
n : ℕ
⊢ Memℒp (↑(approxOn f fmeas s y₀ h₀ n)) p
refine' ⟨(approxOn f fmeas s y₀ h₀ n).aestronglyMeasurable, _⟩
α : Type ?u.604444
β : Type u_2
ι : Type ?u.604450
E : Type u_1
F : Type ?u.604456
𝕜 : Type ?u.604459
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : Memℒp f p
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : Memℒp (fun x => y₀) p
n : ℕ
⊢ snorm (fun x => ↑(approxOn f fmeas s y₀ h₀ n) x - y₀) p μ < ⊤
α : Type ?u.604444
β : Type u_2
ι : Type ?u.604450
E : Type u_1
F : Type ?u.604456
𝕜 : Type ?u.604459
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : Memℒp f p
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : Memℒp (fun x => y₀) p
n : ℕ
⊢ snorm (↑(approxOn f fmeas s y₀ h₀ n)) p μ < ⊤
suffices snorm (fun x => approxOn f fmeas s y₀ h₀ n x - y₀) p μ < ⊤ by
  have : Memℒp (fun x => approxOn f fmeas s y₀ h₀ n x - y₀) p μ :=
    ⟨(approxOn f fmeas s y₀ h₀ n - const β y₀).aestronglyMeasurable, this⟩
  convert snorm_add_lt_top this hi₀
  ext x
  simp
α : Type ?u.604444
β : Type u_2
ι : Type ?u.604450
E : Type u_1
F : Type ?u.604456
𝕜 : Type ?u.604459
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : Memℒp f p
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : Memℒp (fun x => y₀) p
n : ℕ
hf' : Memℒp (fun x => ‖f x - y₀‖) p
⊢ snorm (fun x => ↑(approxOn f fmeas s y₀ h₀ n) x - y₀) p μ < ⊤
α : Type ?u.604444
β : Type u_2
ι : Type ?u.604450
E : Type u_1
F : Type ?u.604456
𝕜 : Type ?u.604459
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : Memℒp f p
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : Memℒp (fun x => y₀) p
n : ℕ
⊢ snorm (fun x => ↑(approxOn f fmeas s y₀ h₀ n) x - y₀) p μ < ⊤
have hf' : Memℒp (fun x => ‖f x - y₀‖) p μ := by
  have h_meas : Measurable fun x => ‖f x - y₀‖ := by
    simp only [← dist_eq_norm]
    exact (continuous_id.dist continuous_const).measurable.comp fmeas
  refine' ⟨h_meas.aemeasurable.aestronglyMeasurable, _⟩
  rw [snorm_norm]
  convert snorm_add_lt_top hf hi₀.neg with x
  simp [sub_eq_add_neg]
α : Type ?u.604444
β : Type u_2
ι : Type ?u.604450
E : Type u_1
F : Type ?u.604456
𝕜 : Type ?u.604459
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : Memℒp f p
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : Memℒp (fun x => y₀) p
n : ℕ
hf' : Memℒp (fun x => ‖f x - y₀‖) p
this : ∀ᵐ (x : β) ∂μ, ‖↑(approxOn f fmeas s y₀ h₀ n) x - y₀‖ ≤ ‖‖f x - y₀‖ + ‖f x - y₀‖‖
⊢ snorm (fun x => ↑(approxOn f fmeas s y₀ h₀ n) x - y₀) p μ < ⊤
α : Type ?u.604444
β : Type u_2
ι : Type ?u.604450
E : Type u_1
F : Type ?u.604456
𝕜 : Type ?u.604459
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : Memℒp f p
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : Memℒp (fun x => y₀) p
n : ℕ
hf' : Memℒp (fun x => ‖f x - y₀‖) p
⊢ snorm (fun x => ↑(approxOn f fmeas s y₀ h₀ n) x - y₀) p μ < ⊤
have : ∀ᵐ x ∂μ, ‖approxOn f fmeas s y₀ h₀ n x - y₀‖ ≤ ‖‖f x - y₀‖ + ‖f x - y₀‖‖ := by
  refine' eventually_of_forall _
  intro x
  convert norm_approxOn_y₀_le fmeas h₀ x n using 1
  rw [Real.norm_eq_abs, abs_of_nonneg]
  exact add_nonneg (norm_nonneg _) (norm_nonneg _)
no goals
α : Type ?u.604444
β : Type u_2
ι : Type ?u.604450
E : Type u_1
F : Type ?u.604456
𝕜 : Type ?u.604459
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : Memℒp f p
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : Memℒp (fun x => y₀) p
n : ℕ
hf' : Memℒp (fun x => ‖f x - y₀‖) p
this : ∀ᵐ (x : β) ∂μ, ‖↑(approxOn f fmeas s y₀ h₀ n) x - y₀‖ ≤ ‖‖f x - y₀‖ + ‖f x - y₀‖‖
⊢ snorm (fun x => ↑(approxOn f fmeas s y₀ h₀ n) x - y₀) p μ < ⊤
calc
  snorm (fun x => approxOn f fmeas s y₀ h₀ n x - y₀) p μ ≤
      snorm (fun x => ‖f x - y₀‖ + ‖f x - y₀‖) p μ :=
    snorm_mono_ae this
  _ < ⊤ := snorm_add_lt_top hf' hf'
α : Type ?u.604444
β : Type u_2
ι : Type ?u.604450
E : Type u_1
F : Type ?u.604456
𝕜 : Type ?u.604459
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : Memℒp f p
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : Memℒp (fun x => y₀) p
n : ℕ
this✝ : snorm (fun x => ↑(approxOn f fmeas s y₀ h₀ n) x - y₀) p μ < ⊤
this : Memℒp (fun x => ↑(approxOn f fmeas s y₀ h₀ n) x - y₀) p
⊢ snorm (↑(approxOn f fmeas s y₀ h₀ n)) p μ < ⊤
α : Type ?u.604444
β : Type u_2
ι : Type ?u.604450
E : Type u_1
F : Type ?u.604456
𝕜 : Type ?u.604459
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : Memℒp f p
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : Memℒp (fun x => y₀) p
n : ℕ
this : snorm (fun x => ↑(approxOn f fmeas s y₀ h₀ n) x - y₀) p μ < ⊤
⊢ snorm (↑(approxOn f fmeas s y₀ h₀ n)) p μ < ⊤
have : Memℒp (fun x => approxOn f fmeas s y₀ h₀ n x - y₀) p μ :=
  ⟨(approxOn f fmeas s y₀ h₀ n - const β y₀).aestronglyMeasurable, this⟩
case h.e'_3.h.e'_5
α : Type ?u.604444
β : Type u_2
ι : Type ?u.604450
E : Type u_1
F : Type ?u.604456
𝕜 : Type ?u.604459
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : Memℒp f p
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : Memℒp (fun x => y₀) p
n : ℕ
this✝ : snorm (fun x => ↑(approxOn f fmeas s y₀ h₀ n) x - y₀) p μ < ⊤
this : Memℒp (fun x => ↑(approxOn f fmeas s y₀ h₀ n) x - y₀) p
⊢ ↑(approxOn f fmeas s y₀ h₀ n) = (fun x => ↑(approxOn f fmeas s y₀ h₀ n) x - y₀) + fun x => y₀
α : Type ?u.604444
β : Type u_2
ι : Type ?u.604450
E : Type u_1
F : Type ?u.604456
𝕜 : Type ?u.604459
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : Memℒp f p
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : Memℒp (fun x => y₀) p
n : ℕ
this✝ : snorm (fun x => ↑(approxOn f fmeas s y₀ h₀ n) x - y₀) p μ < ⊤
this : Memℒp (fun x => ↑(approxOn f fmeas s y₀ h₀ n) x - y₀) p
⊢ snorm (↑(approxOn f fmeas s y₀ h₀ n)) p μ < ⊤
convert snorm_add_lt_top this hi₀
case h.e'_3.h.e'_5.h
α : Type ?u.604444
β : Type u_2
ι : Type ?u.604450
E : Type u_1
F : Type ?u.604456
𝕜 : Type ?u.604459
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : Memℒp f p
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : Memℒp (fun x => y₀) p
n : ℕ
this✝ : snorm (fun x => ↑(approxOn f fmeas s y₀ h₀ n) x - y₀) p μ < ⊤
this : Memℒp (fun x => ↑(approxOn f fmeas s y₀ h₀ n) x - y₀) p
x : β
⊢ ↑(approxOn f fmeas s y₀ h₀ n) x = ((fun x => ↑(approxOn f fmeas s y₀ h₀ n) x - y₀) + fun x => y₀) x
case h.e'_3.h.e'_5
α : Type ?u.604444
β : Type u_2
ι : Type ?u.604450
E : Type u_1
F : Type ?u.604456
𝕜 : Type ?u.604459
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : Memℒp f p
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : Memℒp (fun x => y₀) p
n : ℕ
this✝ : snorm (fun x => ↑(approxOn f fmeas s y₀ h₀ n) x - y₀) p μ < ⊤
this : Memℒp (fun x => ↑(approxOn f fmeas s y₀ h₀ n) x - y₀) p
⊢ ↑(approxOn f fmeas s y₀ h₀ n) = (fun x => ↑(approxOn f fmeas s y₀ h₀ n) x - y₀) + fun x => y₀
ext x
no goals
case h.e'_3.h.e'_5.h
α : Type ?u.604444
β : Type u_2
ι : Type ?u.604450
E : Type u_1
F : Type ?u.604456
𝕜 : Type ?u.604459
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : Memℒp f p
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : Memℒp (fun x => y₀) p
n : ℕ
this✝ : snorm (fun x => ↑(approxOn f fmeas s y₀ h₀ n) x - y₀) p μ < ⊤
this : Memℒp (fun x => ↑(approxOn f fmeas s y₀ h₀ n) x - y₀) p
x : β
⊢ ↑(approxOn f fmeas s y₀ h₀ n) x = ((fun x => ↑(approxOn f fmeas s y₀ h₀ n) x - y₀) + fun x => y₀) x
simp
α : Type ?u.604444
β : Type u_2
ι : Type ?u.604450
E : Type u_1
F : Type ?u.604456
𝕜 : Type ?u.604459
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : Memℒp f p
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : Memℒp (fun x => y₀) p
n : ℕ
h_meas : Measurable fun x => ‖f x - y₀‖
⊢ Memℒp (fun x => ‖f x - y₀‖) p
α : Type ?u.604444
β : Type u_2
ι : Type ?u.604450
E : Type u_1
F : Type ?u.604456
𝕜 : Type ?u.604459
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : Memℒp f p
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : Memℒp (fun x => y₀) p
n : ℕ
⊢ Memℒp (fun x => ‖f x - y₀‖) p
have h_meas : Measurable fun x => ‖f x - y₀‖ := by
  simp only [← dist_eq_norm]
  exact (continuous_id.dist continuous_const).measurable.comp fmeas
α : Type ?u.604444
β : Type u_2
ι : Type ?u.604450
E : Type u_1
F : Type ?u.604456
𝕜 : Type ?u.604459
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : Memℒp f p
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : Memℒp (fun x => y₀) p
n : ℕ
h_meas : Measurable fun x => ‖f x - y₀‖
⊢ snorm (fun x => ‖f x - y₀‖) p μ < ⊤
α : Type ?u.604444
β : Type u_2
ι : Type ?u.604450
E : Type u_1
F : Type ?u.604456
𝕜 : Type ?u.604459
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : Memℒp f p
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : Memℒp (fun x => y₀) p
n : ℕ
h_meas : Measurable fun x => ‖f x - y₀‖
⊢ Memℒp (fun x => ‖f x - y₀‖) p
refine' ⟨h_meas.aemeasurable.aestronglyMeasurable, _⟩
α : Type ?u.604444
β : Type u_2
ι : Type ?u.604450
E : Type u_1
F : Type ?u.604456
𝕜 : Type ?u.604459
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : Memℒp f p
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : Memℒp (fun x => y₀) p
n : ℕ
h_meas : Measurable fun x => ‖f x - y₀‖
⊢ snorm (fun x => f x - y₀) p μ < ⊤
α : Type ?u.604444
β : Type u_2
ι : Type ?u.604450
E : Type u_1
F : Type ?u.604456
𝕜 : Type ?u.604459
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : Memℒp f p
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : Memℒp (fun x => y₀) p
n : ℕ
h_meas : Measurable fun x => ‖f x - y₀‖
⊢ snorm (fun x => ‖f x - y₀‖) p μ < ⊤
rw [snorm_norm]
case h.e'_3.h.e'_5.h
α : Type ?u.604444
β : Type u_2
ι : Type ?u.604450
E : Type u_1
F : Type ?u.604456
𝕜 : Type ?u.604459
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : Memℒp f p
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : Memℒp (fun x => y₀) p
n : ℕ
h_meas : Measurable fun x => ‖f x - y₀‖
x : β
⊢ f x - y₀ = (f + -fun x => y₀) x
α : Type ?u.604444
β : Type u_2
ι : Type ?u.604450
E : Type u_1
F : Type ?u.604456
𝕜 : Type ?u.604459
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : Memℒp f p
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : Memℒp (fun x => y₀) p
n : ℕ
h_meas : Measurable fun x => ‖f x - y₀‖
⊢ snorm (fun x => f x - y₀) p μ < ⊤
convert snorm_add_lt_top hf hi₀.neg with x
no goals
case h.e'_3.h.e'_5.h
α : Type ?u.604444
β : Type u_2
ι : Type ?u.604450
E : Type u_1
F : Type ?u.604456
𝕜 : Type ?u.604459
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : Memℒp f p
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : Memℒp (fun x => y₀) p
n : ℕ
h_meas : Measurable fun x => ‖f x - y₀‖
x : β
⊢ f x - y₀ = (f + -fun x => y₀) x
simp [sub_eq_add_neg]
α : Type ?u.604444
β : Type u_2
ι : Type ?u.604450
E : Type u_1
F : Type ?u.604456
𝕜 : Type ?u.604459
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : Memℒp f p
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : Memℒp (fun x => y₀) p
n : ℕ
⊢ Measurable fun x => dist (f x) y₀
α : Type ?u.604444
β : Type u_2
ι : Type ?u.604450
E : Type u_1
F : Type ?u.604456
𝕜 : Type ?u.604459
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : Memℒp f p
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : Memℒp (fun x => y₀) p
n : ℕ
⊢ Measurable fun x => ‖f x - y₀‖
simp only [← dist_eq_norm]
no goals
α : Type ?u.604444
β : Type u_2
ι : Type ?u.604450
E : Type u_1
F : Type ?u.604456
𝕜 : Type ?u.604459
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : Memℒp f p
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : Memℒp (fun x => y₀) p
n : ℕ
⊢ Measurable fun x => dist (f x) y₀
exact (continuous_id.dist continuous_const).measurable.comp fmeas
α : Type ?u.604444
β : Type u_2
ι : Type ?u.604450
E : Type u_1
F : Type ?u.604456
𝕜 : Type ?u.604459
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : Memℒp f p
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : Memℒp (fun x => y₀) p
n : ℕ
hf' : Memℒp (fun x => ‖f x - y₀‖) p
⊢ ∀ (x : β), ‖↑(approxOn f fmeas s y₀ h₀ n) x - y₀‖ ≤ ‖‖f x - y₀‖ + ‖f x - y₀‖‖
α : Type ?u.604444
β : Type u_2
ι : Type ?u.604450
E : Type u_1
F : Type ?u.604456
𝕜 : Type ?u.604459
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : Memℒp f p
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : Memℒp (fun x => y₀) p
n : ℕ
hf' : Memℒp (fun x => ‖f x - y₀‖) p
⊢ ∀ᵐ (x : β) ∂μ, ‖↑(approxOn f fmeas s y₀ h₀ n) x - y₀‖ ≤ ‖‖f x - y₀‖ + ‖f x - y₀‖‖
refine' eventually_of_forall _
α : Type ?u.604444
β : Type u_2
ι : Type ?u.604450
E : Type u_1
F : Type ?u.604456
𝕜 : Type ?u.604459
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : Memℒp f p
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : Memℒp (fun x => y₀) p
n : ℕ
hf' : Memℒp (fun x => ‖f x - y₀‖) p
x : β
⊢ ‖↑(approxOn f fmeas s y₀ h₀ n) x - y₀‖ ≤ ‖‖f x - y₀‖ + ‖f x - y₀‖‖
α : Type ?u.604444
β : Type u_2
ι : Type ?u.604450
E : Type u_1
F : Type ?u.604456
𝕜 : Type ?u.604459
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : Memℒp f p
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : Memℒp (fun x => y₀) p
n : ℕ
hf' : Memℒp (fun x => ‖f x - y₀‖) p
⊢ ∀ (x : β), ‖↑(approxOn f fmeas s y₀ h₀ n) x - y₀‖ ≤ ‖‖f x - y₀‖ + ‖f x - y₀‖‖
intro x
case h.e'_4
α : Type ?u.604444
β : Type u_2
ι : Type ?u.604450
E : Type u_1
F : Type ?u.604456
𝕜 : Type ?u.604459
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : Memℒp f p
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : Memℒp (fun x => y₀) p
n : ℕ
hf' : Memℒp (fun x => ‖f x - y₀‖) p
x : β
⊢ ‖‖f x - y₀‖ + ‖f x - y₀‖‖ = ‖f x - y₀‖ + ‖f x - y₀‖
α : Type ?u.604444
β : Type u_2
ι : Type ?u.604450
E : Type u_1
F : Type ?u.604456
𝕜 : Type ?u.604459
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : Memℒp f p
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : Memℒp (fun x => y₀) p
n : ℕ
hf' : Memℒp (fun x => ‖f x - y₀‖) p
x : β
⊢ ‖↑(approxOn f fmeas s y₀ h₀ n) x - y₀‖ ≤ ‖‖f x - y₀‖ + ‖f x - y₀‖‖
convert norm_approxOn_y₀_le fmeas h₀ x n using 1
case h.e'_4
α : Type ?u.604444
β : Type u_2
ι : Type ?u.604450
E : Type u_1
F : Type ?u.604456
𝕜 : Type ?u.604459
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : Memℒp f p
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : Memℒp (fun x => y₀) p
n : ℕ
hf' : Memℒp (fun x => ‖f x - y₀‖) p
x : β
⊢ 0 ≤ ‖f x - y₀‖ + ‖f x - y₀‖
case h.e'_4
α : Type ?u.604444
β : Type u_2
ι : Type ?u.604450
E : Type u_1
F : Type ?u.604456
𝕜 : Type ?u.604459
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : Memℒp f p
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : Memℒp (fun x => y₀) p
n : ℕ
hf' : Memℒp (fun x => ‖f x - y₀‖) p
x : β
⊢ ‖‖f x - y₀‖ + ‖f x - y₀‖‖ = ‖f x - y₀‖ + ‖f x - y₀‖
rw [Real.norm_eq_abs, abs_of_nonneg]
no goals
case h.e'_4
α : Type ?u.604444
β : Type u_2
ι : Type ?u.604450
E : Type u_1
F : Type ?u.604456
𝕜 : Type ?u.604459
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : Memℒp f p
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : Memℒp (fun x => y₀) p
n : ℕ
hf' : Memℒp (fun x => ‖f x - y₀‖) p
x : β
⊢ 0 ≤ ‖f x - y₀‖ + ‖f x - y₀‖
exact add_nonneg (norm_nonneg _) (norm_nonneg _)