α : Type u_1
inst✝⁷ : MeasurableSpace α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : BorelSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
μ : Measure α
p✝ : ℝ≥0∞
inst✝² : NormedSpace ℝ E
inst✝¹ : LocallyCompactSpace α
inst✝ : Measure.Regular μ
p : ℝ
hp : 0 < p
f : α → E
hf : Memℒp f (ENNReal.ofReal p)
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
⊢ ∃ g, HasCompactSupport g ∧ (∫ (x : α), ‖f x - g x‖ ^ p ∂μ) ≤ ε ∧ Continuous g ∧ Memℒp g (ENNReal.ofReal p)
α : Type u_1
inst✝⁷ : MeasurableSpace α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : BorelSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
μ : Measure α
p✝ : ℝ≥0∞
inst✝² : NormedSpace ℝ E
inst✝¹ : LocallyCompactSpace α
inst✝ : Measure.Regular μ
p : ℝ
hp : 0 < p
f : α → E
hf : Memℒp f (ENNReal.ofReal p)
ε : ℝ
hε : 0 < ε
⊢ ∃ g, HasCompactSupport g ∧ (∫ (x : α), ‖f x - g x‖ ^ p ∂μ) ≤ ε ∧ Continuous g ∧ Memℒp g (ENNReal.ofReal p)
have I : 0 < ε ^ (1 / p) := Real.rpow_pos_of_pos hε _
α : Type u_1
inst✝⁷ : MeasurableSpace α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : BorelSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
μ : Measure α
p✝ : ℝ≥0∞
inst✝² : NormedSpace ℝ E
inst✝¹ : LocallyCompactSpace α
inst✝ : Measure.Regular μ
p : ℝ
hp : 0 < p
f : α → E
hf : Memℒp f (ENNReal.ofReal p)
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
⊢ ∃ g, HasCompactSupport g ∧ (∫ (x : α), ‖f x - g x‖ ^ p ∂μ) ≤ ε ∧ Continuous g ∧ Memℒp g (ENNReal.ofReal p)
α : Type u_1
inst✝⁷ : MeasurableSpace α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : BorelSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
μ : Measure α
p✝ : ℝ≥0∞
inst✝² : NormedSpace ℝ E
inst✝¹ : LocallyCompactSpace α
inst✝ : Measure.Regular μ
p : ℝ
hp : 0 < p
f : α → E
hf : Memℒp f (ENNReal.ofReal p)
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
⊢ ∃ g, HasCompactSupport g ∧ (∫ (x : α), ‖f x - g x‖ ^ p ∂μ) ≤ ε ∧ Continuous g ∧ Memℒp g (ENNReal.ofReal p)
have A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0 := by
  simp only [Ne.def, ENNReal.ofReal_eq_zero, not_le, I]
α : Type u_1
inst✝⁷ : MeasurableSpace α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : BorelSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
μ : Measure α
p✝ : ℝ≥0∞
inst✝² : NormedSpace ℝ E
inst✝¹ : LocallyCompactSpace α
inst✝ : Measure.Regular μ
p : ℝ
hp : 0 < p
f : α → E
hf : Memℒp f (ENNReal.ofReal p)
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
B : ENNReal.ofReal p ≠ 0
⊢ ∃ g, HasCompactSupport g ∧ (∫ (x : α), ‖f x - g x‖ ^ p ∂μ) ≤ ε ∧ Continuous g ∧ Memℒp g (ENNReal.ofReal p)
α : Type u_1
inst✝⁷ : MeasurableSpace α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : BorelSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
μ : Measure α
p✝ : ℝ≥0∞
inst✝² : NormedSpace ℝ E
inst✝¹ : LocallyCompactSpace α
inst✝ : Measure.Regular μ
p : ℝ
hp : 0 < p
f : α → E
hf : Memℒp f (ENNReal.ofReal p)
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
⊢ ∃ g, HasCompactSupport g ∧ (∫ (x : α), ‖f x - g x‖ ^ p ∂μ) ≤ ε ∧ Continuous g ∧ Memℒp g (ENNReal.ofReal p)
have B : ENNReal.ofReal p ≠ 0 := by simpa only [Ne.def, ENNReal.ofReal_eq_zero, not_le] using hp
case intro.intro.intro.intro
α : Type u_1
inst✝⁷ : MeasurableSpace α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : BorelSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
μ : Measure α
p✝ : ℝ≥0∞
inst✝² : NormedSpace ℝ E
inst✝¹ : LocallyCompactSpace α
inst✝ : Measure.Regular μ
p : ℝ
hp : 0 < p
f : α → E
hf : Memℒp f (ENNReal.ofReal p)
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
B : ENNReal.ofReal p ≠ 0
g : α → E
g_support : HasCompactSupport g
hg : snorm (f - g) (↑(Real.toNNReal p)) μ ≤ ENNReal.ofReal (ε ^ (1 / p))
g_cont : Continuous g
g_mem : Memℒp g ↑(Real.toNNReal p)
⊢ ∃ g, HasCompactSupport g ∧ (∫ (x : α), ‖f x - g x‖ ^ p ∂μ) ≤ ε ∧ Continuous g ∧ Memℒp g (ENNReal.ofReal p)
α : Type u_1
inst✝⁷ : MeasurableSpace α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : BorelSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
μ : Measure α
p✝ : ℝ≥0∞
inst✝² : NormedSpace ℝ E
inst✝¹ : LocallyCompactSpace α
inst✝ : Measure.Regular μ
p : ℝ
hp : 0 < p
f : α → E
hf : Memℒp f (ENNReal.ofReal p)
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
B : ENNReal.ofReal p ≠ 0
⊢ ∃ g, HasCompactSupport g ∧ (∫ (x : α), ‖f x - g x‖ ^ p ∂μ) ≤ ε ∧ Continuous g ∧ Memℒp g (ENNReal.ofReal p)
rcases hf.exists_hasCompactSupport_snorm_sub_le ENNReal.coe_ne_top A with
  ⟨g, g_support, hg, g_cont, g_mem⟩
case intro.intro.intro.intro
α : Type u_1
inst✝⁷ : MeasurableSpace α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : BorelSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
μ : Measure α
p✝ : ℝ≥0∞
inst✝² : NormedSpace ℝ E
inst✝¹ : LocallyCompactSpace α
inst✝ : Measure.Regular μ
p : ℝ
hp : 0 < p
f : α → E
hf : Memℒp f (ENNReal.ofReal p)
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
B : ENNReal.ofReal p ≠ 0
g : α → E
g_support : HasCompactSupport g
g_cont : Continuous g
g_mem : Memℒp g ↑(Real.toNNReal p)
hg : snorm (f - g) (ENNReal.ofReal p) μ ≤ ENNReal.ofReal (ε ^ (1 / p))
⊢ ∃ g, HasCompactSupport g ∧ (∫ (x : α), ‖f x - g x‖ ^ p ∂μ) ≤ ε ∧ Continuous g ∧ Memℒp g (ENNReal.ofReal p)
case intro.intro.intro.intro
α : Type u_1
inst✝⁷ : MeasurableSpace α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : BorelSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
μ : Measure α
p✝ : ℝ≥0∞
inst✝² : NormedSpace ℝ E
inst✝¹ : LocallyCompactSpace α
inst✝ : Measure.Regular μ
p : ℝ
hp : 0 < p
f : α → E
hf : Memℒp f (ENNReal.ofReal p)
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
B : ENNReal.ofReal p ≠ 0
g : α → E
g_support : HasCompactSupport g
hg : snorm (f - g) (↑(Real.toNNReal p)) μ ≤ ENNReal.ofReal (ε ^ (1 / p))
g_cont : Continuous g
g_mem : Memℒp g ↑(Real.toNNReal p)
⊢ ∃ g, HasCompactSupport g ∧ (∫ (x : α), ‖f x - g x‖ ^ p ∂μ) ≤ ε ∧ Continuous g ∧ Memℒp g (ENNReal.ofReal p)
change snorm _ (ENNReal.ofReal p) _ ≤ _ at hg
case intro.intro.intro.intro
α : Type u_1
inst✝⁷ : MeasurableSpace α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : BorelSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
μ : Measure α
p✝ : ℝ≥0∞
inst✝² : NormedSpace ℝ E
inst✝¹ : LocallyCompactSpace α
inst✝ : Measure.Regular μ
p : ℝ
hp : 0 < p
f : α → E
hf : Memℒp f (ENNReal.ofReal p)
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
B : ENNReal.ofReal p ≠ 0
g : α → E
g_support : HasCompactSupport g
g_cont : Continuous g
g_mem : Memℒp g ↑(Real.toNNReal p)
hg : snorm (f - g) (ENNReal.ofReal p) μ ≤ ENNReal.ofReal (ε ^ (1 / p))
⊢ (∫ (x : α), ‖f x - g x‖ ^ p ∂μ) ≤ ε
case intro.intro.intro.intro
α : Type u_1
inst✝⁷ : MeasurableSpace α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : BorelSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
μ : Measure α
p✝ : ℝ≥0∞
inst✝² : NormedSpace ℝ E
inst✝¹ : LocallyCompactSpace α
inst✝ : Measure.Regular μ
p : ℝ
hp : 0 < p
f : α → E
hf : Memℒp f (ENNReal.ofReal p)
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
B : ENNReal.ofReal p ≠ 0
g : α → E
g_support : HasCompactSupport g
g_cont : Continuous g
g_mem : Memℒp g ↑(Real.toNNReal p)
hg : snorm (f - g) (ENNReal.ofReal p) μ ≤ ENNReal.ofReal (ε ^ (1 / p))
⊢ ∃ g, HasCompactSupport g ∧ (∫ (x : α), ‖f x - g x‖ ^ p ∂μ) ≤ ε ∧ Continuous g ∧ Memℒp g (ENNReal.ofReal p)
refine' ⟨g, g_support, _, g_cont, g_mem⟩
α : Type u_1
inst✝⁷ : MeasurableSpace α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : BorelSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
μ : Measure α
p✝ : ℝ≥0∞
inst✝² : NormedSpace ℝ E
inst✝¹ : LocallyCompactSpace α
inst✝ : Measure.Regular μ
p : ℝ
hp : 0 < p
f : α → E
hf : Memℒp f (ENNReal.ofReal p)
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
B : ENNReal.ofReal p ≠ 0
g : α → E
g_support : HasCompactSupport g
g_cont : Continuous g
g_mem : Memℒp g ↑(Real.toNNReal p)
hg : (∫ (a : α), ‖(f - g) a‖ ^ p ∂μ) ^ p⁻¹ ≤ ε ^ p⁻¹
⊢ 0 ≤ ∫ (a : α), ‖(f - g) a‖ ^ p ∂μ
case intro.intro.intro.intro
α : Type u_1
inst✝⁷ : MeasurableSpace α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : BorelSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
μ : Measure α
p✝ : ℝ≥0∞
inst✝² : NormedSpace ℝ E
inst✝¹ : LocallyCompactSpace α
inst✝ : Measure.Regular μ
p : ℝ
hp : 0 < p
f : α → E
hf : Memℒp f (ENNReal.ofReal p)
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
B : ENNReal.ofReal p ≠ 0
g : α → E
g_support : HasCompactSupport g
g_cont : Continuous g
g_mem : Memℒp g ↑(Real.toNNReal p)
hg : snorm (f - g) (ENNReal.ofReal p) μ ≤ ENNReal.ofReal (ε ^ (1 / p))
⊢ (∫ (x : α), ‖f x - g x‖ ^ p ∂μ) ≤ ε
rwa [(hf.sub g_mem).snorm_eq_integral_rpow_norm B ENNReal.coe_ne_top,
  ENNReal.ofReal_le_ofReal_iff I.le, one_div, ENNReal.toReal_ofReal hp.le,
  Real.rpow_le_rpow_iff _ hε.le (inv_pos.2 hp)] at hg
no goals
α : Type u_1
inst✝⁷ : MeasurableSpace α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : BorelSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
μ : Measure α
p✝ : ℝ≥0∞
inst✝² : NormedSpace ℝ E
inst✝¹ : LocallyCompactSpace α
inst✝ : Measure.Regular μ
p : ℝ
hp : 0 < p
f : α → E
hf : Memℒp f (ENNReal.ofReal p)
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
B : ENNReal.ofReal p ≠ 0
g : α → E
g_support : HasCompactSupport g
g_cont : Continuous g
g_mem : Memℒp g ↑(Real.toNNReal p)
hg : (∫ (a : α), ‖(f - g) a‖ ^ p ∂μ) ^ p⁻¹ ≤ ε ^ p⁻¹
⊢ 0 ≤ ∫ (a : α), ‖(f - g) a‖ ^ p ∂μ
exact integral_nonneg fun x => Real.rpow_nonneg_of_nonneg (norm_nonneg _) _
no goals
α : Type u_1
inst✝⁷ : MeasurableSpace α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : BorelSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
μ : Measure α
p✝ : ℝ≥0∞
inst✝² : NormedSpace ℝ E
inst✝¹ : LocallyCompactSpace α
inst✝ : Measure.Regular μ
p : ℝ
hp : 0 < p
f : α → E
hf : Memℒp f (ENNReal.ofReal p)
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
⊢ ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
simp only [Ne.def, ENNReal.ofReal_eq_zero, not_le, I]
no goals
α : Type u_1
inst✝⁷ : MeasurableSpace α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : BorelSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
μ : Measure α
p✝ : ℝ≥0∞
inst✝² : NormedSpace ℝ E
inst✝¹ : LocallyCompactSpace α
inst✝ : Measure.Regular μ
p : ℝ
hp : 0 < p
f : α → E
hf : Memℒp f (ENNReal.ofReal p)
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
⊢ ENNReal.ofReal p ≠ 0
simpa only [Ne.def, ENNReal.ofReal_eq_zero, not_le] using hp