-- Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
theorem memLp_approxOn [BorelSpace E] {f : β → E} {μ : Measure β} (fmeas : Measurable f)
    (hf : MemLp f p μ) {s : Set E} {y₀ : E} (h₀ : y₀ ∈ s) [SeparableSpace s]
    (hi₀ : MemLp (fun _ => y₀) p μ) (n : ℕ) : MemLp (approxOn f fmeas s y₀ h₀ n) p μ

Proof state:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x => y₀) p μ
n : ℕ
⊢ eLpNorm (fun x => (approxOn f fmeas s y₀ h₀ n) x - y₀) p μ < ⊤

Tactic:
have hf' : MemLp (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 [eLpNorm_norm]
  convert eLpNorm_add_lt_top hf hi₀.neg with x
  simp [sub_eq_add_neg]

Result:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x => y₀) p μ
n : ℕ
hf' : MemLp (fun x => ‖f x - y₀‖) p μ
⊢ eLpNorm (fun x => (approxOn f fmeas s y₀ h₀ n) x - y₀) p μ < ⊤

Proof state:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x => y₀) p μ
n : ℕ
⊢ MemLp (⇑(approxOn f fmeas s y₀ h₀ n)) p μ

Tactic:
refine ⟨(approxOn f fmeas s y₀ h₀ n).aestronglyMeasurable, ?_⟩

Result:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x => y₀) p μ
n : ℕ
⊢ eLpNorm (⇑(approxOn f fmeas s y₀ h₀ n)) p μ < ⊤

Proof state:
case h.e'_4
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x => y₀) p μ
n : ℕ
hf' : MemLp (fun x => ‖f x - y₀‖) p μ
x : β
⊢ ‖‖f x - y₀‖ + ‖f x - y₀‖‖ = ‖f x - y₀‖ + ‖f x - y₀‖

Tactic:
rw [Real.norm_eq_abs, abs_of_nonneg]

Result:
case h.e'_4
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x => y₀) p μ
n : ℕ
hf' : MemLp (fun x => ‖f x - y₀‖) p μ
x : β
⊢ 0 ≤ ‖f x - y₀‖ + ‖f x - y₀‖

Proof state:
case h
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x => y₀) p μ
n : ℕ
hf' : MemLp (fun x => ‖f x - y₀‖) p μ
x : β
⊢ ‖(approxOn f fmeas s y₀ h₀ n) x - y₀‖ ≤ ‖‖f x - y₀‖ + ‖f x - y₀‖‖

Tactic:
convert norm_approxOn_y₀_le fmeas h₀ x n using 1

Result:
case h.e'_4
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x => y₀) p μ
n : ℕ
hf' : MemLp (fun x => ‖f x - y₀‖) p μ
x : β
⊢ ‖‖f x - y₀‖ + ‖f x - y₀‖‖ = ‖f x - y₀‖ + ‖f x - y₀‖

Proof state:
case h.e'_4
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x => y₀) p μ
n : ℕ
hf' : MemLp (fun x => ‖f x - y₀‖) p μ
x : β
⊢ 0 ≤ ‖f x - y₀‖ + ‖f x - y₀‖

Tactic:
positivity

Result:
no goals

Proof state:
case h.e'_3.h.e'_5.h
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x => y₀) p μ
n : ℕ
this✝ : eLpNorm (fun x => (approxOn f fmeas s y₀ h₀ n) x - y₀) p μ < ⊤
this : MemLp (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

Tactic:
simp

Result:
no goals

Proof state:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x => y₀) p μ
n : ℕ
⊢ Measurable fun x => dist (f x) y₀

Tactic:
exact (continuous_id.dist continuous_const).measurable.comp fmeas

Result:
no goals

Proof state:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x => y₀) p μ
n : ℕ
this : eLpNorm (fun x => (approxOn f fmeas s y₀ h₀ n) x - y₀) p μ < ⊤
⊢ eLpNorm (⇑(approxOn f fmeas s y₀ h₀ n)) p μ < ⊤

Tactic:
have : MemLp (fun x => approxOn f fmeas s y₀ h₀ n x - y₀) p μ :=
  ⟨(approxOn f fmeas s y₀ h₀ n - const β y₀).aestronglyMeasurable, this⟩

Result:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x => y₀) p μ
n : ℕ
this✝ : eLpNorm (fun x => (approxOn f fmeas s y₀ h₀ n) x - y₀) p μ < ⊤
this : MemLp (fun x => (approxOn f fmeas s y₀ h₀ n) x - y₀) p μ
⊢ eLpNorm (⇑(approxOn f fmeas s y₀ h₀ n)) p μ < ⊤

Proof state:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x => y₀) p μ
n : ℕ
h_meas : Measurable fun x => ‖f x - y₀‖
⊢ eLpNorm (fun x => ‖f x - y₀‖) p μ < ⊤

Tactic:
rw [eLpNorm_norm]

Result:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x => y₀) p μ
n : ℕ
h_meas : Measurable fun x => ‖f x - y₀‖
⊢ eLpNorm (fun x => f x - y₀) p μ < ⊤