[GOAL]
α : 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✝ : Measure.OuterRegular μ
hp : p ≠ ⊤
s u : Set α
s_closed : IsClosed s
u_open : IsOpen u
hsu : s ⊆ u
hs : ↑↑μ s ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ f,
    Continuous f ∧
      snorm (fun x => f x - indicator s (fun _y => c) x) p μ ≤ ε ∧
        (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ Memℒp f p
[PROOFSTEP]
obtain ⟨η, η_pos, hη⟩ : ∃ η : ℝ≥0, 0 < η ∧ ∀ s : Set α, μ s ≤ η → snorm (s.indicator fun _x => c) p μ ≤ ε
[GOAL]
α : 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✝ : Measure.OuterRegular μ
hp : p ≠ ⊤
s u : Set α
s_closed : IsClosed s
u_open : IsOpen u
hsu : s ⊆ u
hs : ↑↑μ s ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ η, 0 < η ∧ ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (indicator s fun _x => c) p μ ≤ ε
case 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✝ : Measure.OuterRegular μ
hp : p ≠ ⊤
s u : Set α
s_closed : IsClosed s
u_open : IsOpen u
hsu : s ⊆ u
hs : ↑↑μ s ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (indicator s fun _x => c) p μ ≤ ε
⊢ ∃ f,
    Continuous f ∧
      snorm (fun x => f x - indicator s (fun _y => c) x) p μ ≤ ε ∧
        (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ Memℒp f p
[PROOFSTEP]
exact exists_snorm_indicator_le hp c hε
[GOAL]
case 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✝ : Measure.OuterRegular μ
hp : p ≠ ⊤
s u : Set α
s_closed : IsClosed s
u_open : IsOpen u
hsu : s ⊆ u
hs : ↑↑μ s ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (indicator s fun _x => c) p μ ≤ ε
⊢ ∃ f,
    Continuous f ∧
      snorm (fun x => f x - indicator s (fun _y => c) x) p μ ≤ ε ∧
        (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ Memℒp f p
[PROOFSTEP]
have ηpos : (0 : ℝ≥0∞) < η := ENNReal.coe_lt_coe.2 η_pos
[GOAL]
case 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✝ : Measure.OuterRegular μ
hp : p ≠ ⊤
s u : Set α
s_closed : IsClosed s
u_open : IsOpen u
hsu : s ⊆ u
hs : ↑↑μ s ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (indicator s fun _x => c) p μ ≤ ε
ηpos : 0 < ↑η
⊢ ∃ f,
    Continuous f ∧
      snorm (fun x => f x - indicator s (fun _y => c) x) p μ ≤ ε ∧
        (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ Memℒp f p
[PROOFSTEP]
obtain ⟨V, sV, V_open, h'V, hV⟩ : ∃ (V : Set α), V ⊇ s ∧ IsOpen V ∧ μ V < ∞ ∧ μ (V \ s) < η
[GOAL]
α : 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✝ : Measure.OuterRegular μ
hp : p ≠ ⊤
s u : Set α
s_closed : IsClosed s
u_open : IsOpen u
hsu : s ⊆ u
hs : ↑↑μ s ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (indicator s fun _x => c) p μ ≤ ε
ηpos : 0 < ↑η
⊢ ∃ V, V ⊇ s ∧ IsOpen V ∧ ↑↑μ V < ⊤ ∧ ↑↑μ (V \ s) < ↑η
case intro.intro.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✝ : Measure.OuterRegular μ
hp : p ≠ ⊤
s u : Set α
s_closed : IsClosed s
u_open : IsOpen u
hsu : s ⊆ u
hs : ↑↑μ s ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (indicator s fun _x => c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen V
h'V : ↑↑μ V < ⊤
hV : ↑↑μ (V \ s) < ↑η
⊢ ∃ f,
    Continuous f ∧
      snorm (fun x => f x - indicator s (fun _y => c) x) p μ ≤ ε ∧
        (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ Memℒp f p
[PROOFSTEP]
exact s_closed.measurableSet.exists_isOpen_diff_lt hs ηpos.ne'
[GOAL]
case intro.intro.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✝ : Measure.OuterRegular μ
hp : p ≠ ⊤
s u : Set α
s_closed : IsClosed s
u_open : IsOpen u
hsu : s ⊆ u
hs : ↑↑μ s ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (indicator s fun _x => c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen V
h'V : ↑↑μ V < ⊤
hV : ↑↑μ (V \ s) < ↑η
⊢ ∃ f,
    Continuous f ∧
      snorm (fun x => f x - indicator s (fun _y => c) x) p μ ≤ ε ∧
        (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ Memℒp f p
[PROOFSTEP]
let v := u ∩ V
[GOAL]
case intro.intro.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✝ : Measure.OuterRegular μ
hp : p ≠ ⊤
s u : Set α
s_closed : IsClosed s
u_open : IsOpen u
hsu : s ⊆ u
hs : ↑↑μ s ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (indicator s fun _x => c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen V
h'V : ↑↑μ V < ⊤
hV : ↑↑μ (V \ s) < ↑η
v : Set α := u ∩ V
⊢ ∃ f,
    Continuous f ∧
      snorm (fun x => f x - indicator s (fun _y => c) x) p μ ≤ ε ∧
        (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ Memℒp f p
[PROOFSTEP]
have hsv : s ⊆ v := subset_inter hsu sV
[GOAL]
case intro.intro.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✝ : Measure.OuterRegular μ
hp : p ≠ ⊤
s u : Set α
s_closed : IsClosed s
u_open : IsOpen u
hsu : s ⊆ u
hs : ↑↑μ s ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (indicator s fun _x => c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen V
h'V : ↑↑μ V < ⊤
hV : ↑↑μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
⊢ ∃ f,
    Continuous f ∧
      snorm (fun x => f x - indicator s (fun _y => c) x) p μ ≤ ε ∧
        (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ Memℒp f p
[PROOFSTEP]
have hμv : μ v < ∞ := (measure_mono (inter_subset_right _ _)).trans_lt h'V
[GOAL]
case intro.intro.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✝ : Measure.OuterRegular μ
hp : p ≠ ⊤
s u : Set α
s_closed : IsClosed s
u_open : IsOpen u
hsu : s ⊆ u
hs : ↑↑μ s ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (indicator s fun _x => c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen V
h'V : ↑↑μ V < ⊤
hV : ↑↑μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : ↑↑μ v < ⊤
⊢ ∃ f,
    Continuous f ∧
      snorm (fun x => f x - indicator s (fun _y => c) x) p μ ≤ ε ∧
        (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ Memℒp f p
[PROOFSTEP]
obtain ⟨g, hgv, hgs, hg_range⟩ :=
  exists_continuous_zero_one_of_closed (u_open.inter V_open).isClosed_compl s_closed
    (disjoint_compl_left_iff.2 hsv)
      -- Multiply this by `c` to get a continuous approximation to the function `f`; the key point is
        -- that this is pointwise bounded by the indicator of the set `v \ s`, which has small measure.
[GOAL]
case intro.intro.intro.intro.intro.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✝ : Measure.OuterRegular μ
hp : p ≠ ⊤
s u : Set α
s_closed : IsClosed s
u_open : IsOpen u
hsu : s ⊆ u
hs : ↑↑μ s ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (indicator s fun _x => c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen V
h'V : ↑↑μ V < ⊤
hV : ↑↑μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : ↑↑μ v < ⊤
g : C(α, ℝ)
hgv : EqOn (↑g) 0 (u ∩ V)ᶜ
hgs : EqOn (↑g) 1 s
hg_range : ∀ (x : α), ↑g x ∈ Icc 0 1
⊢ ∃ f,
    Continuous f ∧
      snorm (fun x => f x - indicator s (fun _y => c) x) p μ ≤ ε ∧
        (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ Memℒp f p
[PROOFSTEP]
have g_norm : ∀ x, ‖g x‖ = g x := fun x => by rw [Real.norm_eq_abs, abs_of_nonneg (hg_range x).1]
[GOAL]
α : 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✝ : Measure.OuterRegular μ
hp : p ≠ ⊤
s u : Set α
s_closed : IsClosed s
u_open : IsOpen u
hsu : s ⊆ u
hs : ↑↑μ s ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (indicator s fun _x => c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen V
h'V : ↑↑μ V < ⊤
hV : ↑↑μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : ↑↑μ v < ⊤
g : C(α, ℝ)
hgv : EqOn (↑g) 0 (u ∩ V)ᶜ
hgs : EqOn (↑g) 1 s
hg_range : ∀ (x : α), ↑g x ∈ Icc 0 1
x : α
⊢ ‖↑g x‖ = ↑g x
[PROOFSTEP]
rw [Real.norm_eq_abs, abs_of_nonneg (hg_range x).1]
[GOAL]
case intro.intro.intro.intro.intro.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✝ : Measure.OuterRegular μ
hp : p ≠ ⊤
s u : Set α
s_closed : IsClosed s
u_open : IsOpen u
hsu : s ⊆ u
hs : ↑↑μ s ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (indicator s fun _x => c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen V
h'V : ↑↑μ V < ⊤
hV : ↑↑μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : ↑↑μ v < ⊤
g : C(α, ℝ)
hgv : EqOn (↑g) 0 (u ∩ V)ᶜ
hgs : EqOn (↑g) 1 s
hg_range : ∀ (x : α), ↑g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖↑g x‖ = ↑g x
⊢ ∃ f,
    Continuous f ∧
      snorm (fun x => f x - indicator s (fun _y => c) x) p μ ≤ ε ∧
        (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ Memℒp f p
[PROOFSTEP]
have gc_bd0 : ∀ x, ‖g x • c‖ ≤ ‖c‖ := by
  intro x
  simp only [norm_smul, g_norm x]
  apply mul_le_of_le_one_left (norm_nonneg _)
  exact (hg_range x).2
[GOAL]
α : 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✝ : Measure.OuterRegular μ
hp : p ≠ ⊤
s u : Set α
s_closed : IsClosed s
u_open : IsOpen u
hsu : s ⊆ u
hs : ↑↑μ s ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (indicator s fun _x => c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen V
h'V : ↑↑μ V < ⊤
hV : ↑↑μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : ↑↑μ v < ⊤
g : C(α, ℝ)
hgv : EqOn (↑g) 0 (u ∩ V)ᶜ
hgs : EqOn (↑g) 1 s
hg_range : ∀ (x : α), ↑g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖↑g x‖ = ↑g x
⊢ ∀ (x : α), ‖↑g x • c‖ ≤ ‖c‖
[PROOFSTEP]
intro x
[GOAL]
α : 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✝ : Measure.OuterRegular μ
hp : p ≠ ⊤
s u : Set α
s_closed : IsClosed s
u_open : IsOpen u
hsu : s ⊆ u
hs : ↑↑μ s ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (indicator s fun _x => c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen V
h'V : ↑↑μ V < ⊤
hV : ↑↑μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : ↑↑μ v < ⊤
g : C(α, ℝ)
hgv : EqOn (↑g) 0 (u ∩ V)ᶜ
hgs : EqOn (↑g) 1 s
hg_range : ∀ (x : α), ↑g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖↑g x‖ = ↑g x
x : α
⊢ ‖↑g x • c‖ ≤ ‖c‖
[PROOFSTEP]
simp only [norm_smul, g_norm x]
[GOAL]
α : 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✝ : Measure.OuterRegular μ
hp : p ≠ ⊤
s u : Set α
s_closed : IsClosed s
u_open : IsOpen u
hsu : s ⊆ u
hs : ↑↑μ s ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (indicator s fun _x => c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen V
h'V : ↑↑μ V < ⊤
hV : ↑↑μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : ↑↑μ v < ⊤
g : C(α, ℝ)
hgv : EqOn (↑g) 0 (u ∩ V)ᶜ
hgs : EqOn (↑g) 1 s
hg_range : ∀ (x : α), ↑g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖↑g x‖ = ↑g x
x : α
⊢ ↑g x * ‖c‖ ≤ ‖c‖
[PROOFSTEP]
apply mul_le_of_le_one_left (norm_nonneg _)
[GOAL]
α : 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✝ : Measure.OuterRegular μ
hp : p ≠ ⊤
s u : Set α
s_closed : IsClosed s
u_open : IsOpen u
hsu : s ⊆ u
hs : ↑↑μ s ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (indicator s fun _x => c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen V
h'V : ↑↑μ V < ⊤
hV : ↑↑μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : ↑↑μ v < ⊤
g : C(α, ℝ)
hgv : EqOn (↑g) 0 (u ∩ V)ᶜ
hgs : EqOn (↑g) 1 s
hg_range : ∀ (x : α), ↑g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖↑g x‖ = ↑g x
x : α
⊢ ↑g x ≤ 1
[PROOFSTEP]
exact (hg_range x).2
[GOAL]
case intro.intro.intro.intro.intro.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✝ : Measure.OuterRegular μ
hp : p ≠ ⊤
s u : Set α
s_closed : IsClosed s
u_open : IsOpen u
hsu : s ⊆ u
hs : ↑↑μ s ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (indicator s fun _x => c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen V
h'V : ↑↑μ V < ⊤
hV : ↑↑μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : ↑↑μ v < ⊤
g : C(α, ℝ)
hgv : EqOn (↑g) 0 (u ∩ V)ᶜ
hgs : EqOn (↑g) 1 s
hg_range : ∀ (x : α), ↑g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖↑g x‖ = ↑g x
gc_bd0 : ∀ (x : α), ‖↑g x • c‖ ≤ ‖c‖
⊢ ∃ f,
    Continuous f ∧
      snorm (fun x => f x - indicator s (fun _y => c) x) p μ ≤ ε ∧
        (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ Memℒp f p
[PROOFSTEP]
have gc_bd : ∀ x, ‖g x • c - s.indicator (fun _x => c) x‖ ≤ ‖(v \ s).indicator (fun _x => c) x‖ :=
  by
  intro x
  by_cases hv : x ∈ v
  · rw [← Set.diff_union_of_subset hsv] at hv 
    cases' hv with hsv hs
    · simpa only [hsv.2, Set.indicator_of_not_mem, not_false_iff, sub_zero, hsv, Set.indicator_of_mem] using gc_bd0 x
    · simp [hgs hs, hs]
  · simp [hgv hv, show x ∉ s from fun h => hv (hsv h)]
[GOAL]
α : 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✝ : Measure.OuterRegular μ
hp : p ≠ ⊤
s u : Set α
s_closed : IsClosed s
u_open : IsOpen u
hsu : s ⊆ u
hs : ↑↑μ s ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (indicator s fun _x => c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen V
h'V : ↑↑μ V < ⊤
hV : ↑↑μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : ↑↑μ v < ⊤
g : C(α, ℝ)
hgv : EqOn (↑g) 0 (u ∩ V)ᶜ
hgs : EqOn (↑g) 1 s
hg_range : ∀ (x : α), ↑g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖↑g x‖ = ↑g x
gc_bd0 : ∀ (x : α), ‖↑g x • c‖ ≤ ‖c‖
⊢ ∀ (x : α), ‖↑g x • c - indicator s (fun _x => c) x‖ ≤ ‖indicator (v \ s) (fun _x => c) x‖
[PROOFSTEP]
intro x
[GOAL]
α : 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✝ : Measure.OuterRegular μ
hp : p ≠ ⊤
s u : Set α
s_closed : IsClosed s
u_open : IsOpen u
hsu : s ⊆ u
hs : ↑↑μ s ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (indicator s fun _x => c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen V
h'V : ↑↑μ V < ⊤
hV : ↑↑μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : ↑↑μ v < ⊤
g : C(α, ℝ)
hgv : EqOn (↑g) 0 (u ∩ V)ᶜ
hgs : EqOn (↑g) 1 s
hg_range : ∀ (x : α), ↑g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖↑g x‖ = ↑g x
gc_bd0 : ∀ (x : α), ‖↑g x • c‖ ≤ ‖c‖
x : α
⊢ ‖↑g x • c - indicator s (fun _x => c) x‖ ≤ ‖indicator (v \ s) (fun _x => c) x‖
[PROOFSTEP]
by_cases hv : x ∈ v
[GOAL]
case pos
α : 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✝ : Measure.OuterRegular μ
hp : p ≠ ⊤
s u : Set α
s_closed : IsClosed s
u_open : IsOpen u
hsu : s ⊆ u
hs : ↑↑μ s ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (indicator s fun _x => c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen V
h'V : ↑↑μ V < ⊤
hV : ↑↑μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : ↑↑μ v < ⊤
g : C(α, ℝ)
hgv : EqOn (↑g) 0 (u ∩ V)ᶜ
hgs : EqOn (↑g) 1 s
hg_range : ∀ (x : α), ↑g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖↑g x‖ = ↑g x
gc_bd0 : ∀ (x : α), ‖↑g x • c‖ ≤ ‖c‖
x : α
hv : x ∈ v
⊢ ‖↑g x • c - indicator s (fun _x => c) x‖ ≤ ‖indicator (v \ s) (fun _x => c) x‖
[PROOFSTEP]
rw [← Set.diff_union_of_subset hsv] at hv 
[GOAL]
case pos
α : 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✝ : Measure.OuterRegular μ
hp : p ≠ ⊤
s u : Set α
s_closed : IsClosed s
u_open : IsOpen u
hsu : s ⊆ u
hs : ↑↑μ s ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (indicator s fun _x => c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen V
h'V : ↑↑μ V < ⊤
hV : ↑↑μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : ↑↑μ v < ⊤
g : C(α, ℝ)
hgv : EqOn (↑g) 0 (u ∩ V)ᶜ
hgs : EqOn (↑g) 1 s
hg_range : ∀ (x : α), ↑g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖↑g x‖ = ↑g x
gc_bd0 : ∀ (x : α), ‖↑g x • c‖ ≤ ‖c‖
x : α
hv : x ∈ v \ s ∪ s
⊢ ‖↑g x • c - indicator s (fun _x => c) x‖ ≤ ‖indicator (v \ s) (fun _x => c) x‖
[PROOFSTEP]
cases' hv with hsv hs
[GOAL]
case pos.inl
α : 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✝ : Measure.OuterRegular μ
hp : p ≠ ⊤
s u : Set α
s_closed : IsClosed s
u_open : IsOpen u
hsu : s ⊆ u
hs : ↑↑μ s ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (indicator s fun _x => c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen V
h'V : ↑↑μ V < ⊤
hV : ↑↑μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv✝ : s ⊆ v
hμv : ↑↑μ v < ⊤
g : C(α, ℝ)
hgv : EqOn (↑g) 0 (u ∩ V)ᶜ
hgs : EqOn (↑g) 1 s
hg_range : ∀ (x : α), ↑g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖↑g x‖ = ↑g x
gc_bd0 : ∀ (x : α), ‖↑g x • c‖ ≤ ‖c‖
x : α
hsv : x ∈ v \ s
⊢ ‖↑g x • c - indicator s (fun _x => c) x‖ ≤ ‖indicator (v \ s) (fun _x => c) x‖
[PROOFSTEP]
simpa only [hsv.2, Set.indicator_of_not_mem, not_false_iff, sub_zero, hsv, Set.indicator_of_mem] using gc_bd0 x
[GOAL]
case pos.inr
α : 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✝ : Measure.OuterRegular μ
hp : p ≠ ⊤
s u : Set α
s_closed : IsClosed s
u_open : IsOpen u
hsu : s ⊆ u
hs✝ : ↑↑μ s ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (indicator s fun _x => c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen V
h'V : ↑↑μ V < ⊤
hV : ↑↑μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : ↑↑μ v < ⊤
g : C(α, ℝ)
hgv : EqOn (↑g) 0 (u ∩ V)ᶜ
hgs : EqOn (↑g) 1 s
hg_range : ∀ (x : α), ↑g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖↑g x‖ = ↑g x
gc_bd0 : ∀ (x : α), ‖↑g x • c‖ ≤ ‖c‖
x : α
hs : x ∈ s
⊢ ‖↑g x • c - indicator s (fun _x => c) x‖ ≤ ‖indicator (v \ s) (fun _x => c) x‖
[PROOFSTEP]
simp [hgs hs, hs]
[GOAL]
case neg
α : 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✝ : Measure.OuterRegular μ
hp : p ≠ ⊤
s u : Set α
s_closed : IsClosed s
u_open : IsOpen u
hsu : s ⊆ u
hs : ↑↑μ s ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (indicator s fun _x => c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen V
h'V : ↑↑μ V < ⊤
hV : ↑↑μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : ↑↑μ v < ⊤
g : C(α, ℝ)
hgv : EqOn (↑g) 0 (u ∩ V)ᶜ
hgs : EqOn (↑g) 1 s
hg_range : ∀ (x : α), ↑g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖↑g x‖ = ↑g x
gc_bd0 : ∀ (x : α), ‖↑g x • c‖ ≤ ‖c‖
x : α
hv : ¬x ∈ v
⊢ ‖↑g x • c - indicator s (fun _x => c) x‖ ≤ ‖indicator (v \ s) (fun _x => c) x‖
[PROOFSTEP]
simp [hgv hv, show x ∉ s from fun h => hv (hsv h)]
[GOAL]
case intro.intro.intro.intro.intro.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✝ : Measure.OuterRegular μ
hp : p ≠ ⊤
s u : Set α
s_closed : IsClosed s
u_open : IsOpen u
hsu : s ⊆ u
hs : ↑↑μ s ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (indicator s fun _x => c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen V
h'V : ↑↑μ V < ⊤
hV : ↑↑μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : ↑↑μ v < ⊤
g : C(α, ℝ)
hgv : EqOn (↑g) 0 (u ∩ V)ᶜ
hgs : EqOn (↑g) 1 s
hg_range : ∀ (x : α), ↑g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖↑g x‖ = ↑g x
gc_bd0 : ∀ (x : α), ‖↑g x • c‖ ≤ ‖c‖
gc_bd : ∀ (x : α), ‖↑g x • c - indicator s (fun _x => c) x‖ ≤ ‖indicator (v \ s) (fun _x => c) x‖
⊢ ∃ f,
    Continuous f ∧
      snorm (fun x => f x - indicator s (fun _y => c) x) p μ ≤ ε ∧
        (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ Memℒp f p
[PROOFSTEP]
have gc_support : (Function.support fun x : α => g x • c) ⊆ v :=
  by
  refine' Function.support_subset_iff'.2 fun x hx => _
  simp only [hgv hx, Pi.zero_apply, zero_smul]
[GOAL]
α : 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✝ : Measure.OuterRegular μ
hp : p ≠ ⊤
s u : Set α
s_closed : IsClosed s
u_open : IsOpen u
hsu : s ⊆ u
hs : ↑↑μ s ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (indicator s fun _x => c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen V
h'V : ↑↑μ V < ⊤
hV : ↑↑μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : ↑↑μ v < ⊤
g : C(α, ℝ)
hgv : EqOn (↑g) 0 (u ∩ V)ᶜ
hgs : EqOn (↑g) 1 s
hg_range : ∀ (x : α), ↑g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖↑g x‖ = ↑g x
gc_bd0 : ∀ (x : α), ‖↑g x • c‖ ≤ ‖c‖
gc_bd : ∀ (x : α), ‖↑g x • c - indicator s (fun _x => c) x‖ ≤ ‖indicator (v \ s) (fun _x => c) x‖
⊢ (Function.support fun x => ↑g x • c) ⊆ v
[PROOFSTEP]
refine' Function.support_subset_iff'.2 fun x hx => _
[GOAL]
α : 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✝ : Measure.OuterRegular μ
hp : p ≠ ⊤
s u : Set α
s_closed : IsClosed s
u_open : IsOpen u
hsu : s ⊆ u
hs : ↑↑μ s ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (indicator s fun _x => c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen V
h'V : ↑↑μ V < ⊤
hV : ↑↑μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : ↑↑μ v < ⊤
g : C(α, ℝ)
hgv : EqOn (↑g) 0 (u ∩ V)ᶜ
hgs : EqOn (↑g) 1 s
hg_range : ∀ (x : α), ↑g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖↑g x‖ = ↑g x
gc_bd0 : ∀ (x : α), ‖↑g x • c‖ ≤ ‖c‖
gc_bd : ∀ (x : α), ‖↑g x • c - indicator s (fun _x => c) x‖ ≤ ‖indicator (v \ s) (fun _x => c) x‖
x : α
hx : ¬x ∈ v
⊢ ↑g x • c = 0
[PROOFSTEP]
simp only [hgv hx, Pi.zero_apply, zero_smul]
[GOAL]
case intro.intro.intro.intro.intro.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✝ : Measure.OuterRegular μ
hp : p ≠ ⊤
s u : Set α
s_closed : IsClosed s
u_open : IsOpen u
hsu : s ⊆ u
hs : ↑↑μ s ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (indicator s fun _x => c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen V
h'V : ↑↑μ V < ⊤
hV : ↑↑μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : ↑↑μ v < ⊤
g : C(α, ℝ)
hgv : EqOn (↑g) 0 (u ∩ V)ᶜ
hgs : EqOn (↑g) 1 s
hg_range : ∀ (x : α), ↑g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖↑g x‖ = ↑g x
gc_bd0 : ∀ (x : α), ‖↑g x • c‖ ≤ ‖c‖
gc_bd : ∀ (x : α), ‖↑g x • c - indicator s (fun _x => c) x‖ ≤ ‖indicator (v \ s) (fun _x => c) x‖
gc_support : (Function.support fun x => ↑g x • c) ⊆ v
⊢ ∃ f,
    Continuous f ∧
      snorm (fun x => f x - indicator s (fun _y => c) x) p μ ≤ ε ∧
        (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ Memℒp f p
[PROOFSTEP]
have gc_mem : Memℒp (fun x => g x • c) p μ :=
  by
  refine' Memℒp.smul_of_top_left (memℒp_top_const _) _
  refine' ⟨g.continuous.aestronglyMeasurable, _⟩
  have : snorm (v.indicator fun _x => (1 : ℝ)) p μ < ⊤ :=
    by
    refine' (snorm_indicator_const_le _ _).trans_lt _
    simp only [lt_top_iff_ne_top, hμv.ne, nnnorm_one, ENNReal.coe_one, one_div, one_mul, Ne.def,
      ENNReal.rpow_eq_top_iff, inv_lt_zero, false_and_iff, or_false_iff, not_and, not_lt, ENNReal.toReal_nonneg,
      imp_true_iff]
  refine' (snorm_mono fun x => _).trans_lt this
  by_cases hx : x ∈ v
  · simp only [hx, abs_of_nonneg (hg_range x).1, (hg_range x).2, Real.norm_eq_abs, indicator_of_mem, CstarRing.norm_one]
  · simp only [hgv hx, Pi.zero_apply, Real.norm_eq_abs, abs_zero, abs_nonneg]
[GOAL]
α : 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✝ : Measure.OuterRegular μ
hp : p ≠ ⊤
s u : Set α
s_closed : IsClosed s
u_open : IsOpen u
hsu : s ⊆ u
hs : ↑↑μ s ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (indicator s fun _x => c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen V
h'V : ↑↑μ V < ⊤
hV : ↑↑μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : ↑↑μ v < ⊤
g : C(α, ℝ)
hgv : EqOn (↑g) 0 (u ∩ V)ᶜ
hgs : EqOn (↑g) 1 s
hg_range : ∀ (x : α), ↑g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖↑g x‖ = ↑g x
gc_bd0 : ∀ (x : α), ‖↑g x • c‖ ≤ ‖c‖
gc_bd : ∀ (x : α), ‖↑g x • c - indicator s (fun _x => c) x‖ ≤ ‖indicator (v \ s) (fun _x => c) x‖
gc_support : (Function.support fun x => ↑g x • c) ⊆ v
⊢ Memℒp (fun x => ↑g x • c) p
[PROOFSTEP]
refine' Memℒp.smul_of_top_left (memℒp_top_const _) _
[GOAL]
α : 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✝ : Measure.OuterRegular μ
hp : p ≠ ⊤
s u : Set α
s_closed : IsClosed s
u_open : IsOpen u
hsu : s ⊆ u
hs : ↑↑μ s ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (indicator s fun _x => c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen V
h'V : ↑↑μ V < ⊤
hV : ↑↑μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : ↑↑μ v < ⊤
g : C(α, ℝ)
hgv : EqOn (↑g) 0 (u ∩ V)ᶜ
hgs : EqOn (↑g) 1 s
hg_range : ∀ (x : α), ↑g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖↑g x‖ = ↑g x
gc_bd0 : ∀ (x : α), ‖↑g x • c‖ ≤ ‖c‖
gc_bd : ∀ (x : α), ‖↑g x • c - indicator s (fun _x => c) x‖ ≤ ‖indicator (v \ s) (fun _x => c) x‖
gc_support : (Function.support fun x => ↑g x • c) ⊆ v
⊢ Memℒp (fun x => ↑g x) p
[PROOFSTEP]
refine' ⟨g.continuous.aestronglyMeasurable, _⟩
[GOAL]
α : 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✝ : Measure.OuterRegular μ
hp : p ≠ ⊤
s u : Set α
s_closed : IsClosed s
u_open : IsOpen u
hsu : s ⊆ u
hs : ↑↑μ s ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (indicator s fun _x => c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen V
h'V : ↑↑μ V < ⊤
hV : ↑↑μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : ↑↑μ v < ⊤
g : C(α, ℝ)
hgv : EqOn (↑g) 0 (u ∩ V)ᶜ
hgs : EqOn (↑g) 1 s
hg_range : ∀ (x : α), ↑g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖↑g x‖ = ↑g x
gc_bd0 : ∀ (x : α), ‖↑g x • c‖ ≤ ‖c‖
gc_bd : ∀ (x : α), ‖↑g x • c - indicator s (fun _x => c) x‖ ≤ ‖indicator (v \ s) (fun _x => c) x‖
gc_support : (Function.support fun x => ↑g x • c) ⊆ v
⊢ snorm (fun x => ↑g x) p μ < ⊤
[PROOFSTEP]
have : snorm (v.indicator fun _x => (1 : ℝ)) p μ < ⊤ :=
  by
  refine' (snorm_indicator_const_le _ _).trans_lt _
  simp only [lt_top_iff_ne_top, hμv.ne, nnnorm_one, ENNReal.coe_one, one_div, one_mul, Ne.def, ENNReal.rpow_eq_top_iff,
    inv_lt_zero, false_and_iff, or_false_iff, not_and, not_lt, ENNReal.toReal_nonneg, imp_true_iff]
[GOAL]
α : 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✝ : Measure.OuterRegular μ
hp : p ≠ ⊤
s u : Set α
s_closed : IsClosed s
u_open : IsOpen u
hsu : s ⊆ u
hs : ↑↑μ s ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (indicator s fun _x => c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen V
h'V : ↑↑μ V < ⊤
hV : ↑↑μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : ↑↑μ v < ⊤
g : C(α, ℝ)
hgv : EqOn (↑g) 0 (u ∩ V)ᶜ
hgs : EqOn (↑g) 1 s
hg_range : ∀ (x : α), ↑g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖↑g x‖ = ↑g x
gc_bd0 : ∀ (x : α), ‖↑g x • c‖ ≤ ‖c‖
gc_bd : ∀ (x : α), ‖↑g x • c - indicator s (fun _x => c) x‖ ≤ ‖indicator (v \ s) (fun _x => c) x‖
gc_support : (Function.support fun x => ↑g x • c) ⊆ v
⊢ snorm (indicator v fun _x => 1) p μ < ⊤
[PROOFSTEP]
refine' (snorm_indicator_const_le _ _).trans_lt _
[GOAL]
α : 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✝ : Measure.OuterRegular μ
hp : p ≠ ⊤
s u : Set α
s_closed : IsClosed s
u_open : IsOpen u
hsu : s ⊆ u
hs : ↑↑μ s ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (indicator s fun _x => c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen V
h'V : ↑↑μ V < ⊤
hV : ↑↑μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : ↑↑μ v < ⊤
g : C(α, ℝ)
hgv : EqOn (↑g) 0 (u ∩ V)ᶜ
hgs : EqOn (↑g) 1 s
hg_range : ∀ (x : α), ↑g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖↑g x‖ = ↑g x
gc_bd0 : ∀ (x : α), ‖↑g x • c‖ ≤ ‖c‖
gc_bd : ∀ (x : α), ‖↑g x • c - indicator s (fun _x => c) x‖ ≤ ‖indicator (v \ s) (fun _x => c) x‖
gc_support : (Function.support fun x => ↑g x • c) ⊆ v
⊢ ↑‖1‖₊ * ↑↑μ v ^ (1 / ENNReal.toReal p) < ⊤
[PROOFSTEP]
simp only [lt_top_iff_ne_top, hμv.ne, nnnorm_one, ENNReal.coe_one, one_div, one_mul, Ne.def, ENNReal.rpow_eq_top_iff,
  inv_lt_zero, false_and_iff, or_false_iff, not_and, not_lt, ENNReal.toReal_nonneg, imp_true_iff]
[GOAL]
α : 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✝ : Measure.OuterRegular μ
hp : p ≠ ⊤
s u : Set α
s_closed : IsClosed s
u_open : IsOpen u
hsu : s ⊆ u
hs : ↑↑μ s ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (indicator s fun _x => c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen V
h'V : ↑↑μ V < ⊤
hV : ↑↑μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : ↑↑μ v < ⊤
g : C(α, ℝ)
hgv : EqOn (↑g) 0 (u ∩ V)ᶜ
hgs : EqOn (↑g) 1 s
hg_range : ∀ (x : α), ↑g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖↑g x‖ = ↑g x
gc_bd0 : ∀ (x : α), ‖↑g x • c‖ ≤ ‖c‖
gc_bd : ∀ (x : α), ‖↑g x • c - indicator s (fun _x => c) x‖ ≤ ‖indicator (v \ s) (fun _x => c) x‖
gc_support : (Function.support fun x => ↑g x • c) ⊆ v
this : snorm (indicator v fun _x => 1) p μ < ⊤
⊢ snorm (fun x => ↑g x) p μ < ⊤
[PROOFSTEP]
refine' (snorm_mono fun x => _).trans_lt this
[GOAL]
α : 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✝ : Measure.OuterRegular μ
hp : p ≠ ⊤
s u : Set α
s_closed : IsClosed s
u_open : IsOpen u
hsu : s ⊆ u
hs : ↑↑μ s ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (indicator s fun _x => c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen V
h'V : ↑↑μ V < ⊤
hV : ↑↑μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : ↑↑μ v < ⊤
g : C(α, ℝ)
hgv : EqOn (↑g) 0 (u ∩ V)ᶜ
hgs : EqOn (↑g) 1 s
hg_range : ∀ (x : α), ↑g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖↑g x‖ = ↑g x
gc_bd0 : ∀ (x : α), ‖↑g x • c‖ ≤ ‖c‖
gc_bd : ∀ (x : α), ‖↑g x • c - indicator s (fun _x => c) x‖ ≤ ‖indicator (v \ s) (fun _x => c) x‖
gc_support : (Function.support fun x => ↑g x • c) ⊆ v
this : snorm (indicator v fun _x => 1) p μ < ⊤
x : α
⊢ ‖↑g x‖ ≤ ‖indicator v (fun _x => 1) x‖
[PROOFSTEP]
by_cases hx : x ∈ v
[GOAL]
case pos
α : 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✝ : Measure.OuterRegular μ
hp : p ≠ ⊤
s u : Set α
s_closed : IsClosed s
u_open : IsOpen u
hsu : s ⊆ u
hs : ↑↑μ s ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (indicator s fun _x => c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen V
h'V : ↑↑μ V < ⊤
hV : ↑↑μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : ↑↑μ v < ⊤
g : C(α, ℝ)
hgv : EqOn (↑g) 0 (u ∩ V)ᶜ
hgs : EqOn (↑g) 1 s
hg_range : ∀ (x : α), ↑g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖↑g x‖ = ↑g x
gc_bd0 : ∀ (x : α), ‖↑g x • c‖ ≤ ‖c‖
gc_bd : ∀ (x : α), ‖↑g x • c - indicator s (fun _x => c) x‖ ≤ ‖indicator (v \ s) (fun _x => c) x‖
gc_support : (Function.support fun x => ↑g x • c) ⊆ v
this : snorm (indicator v fun _x => 1) p μ < ⊤
x : α
hx : x ∈ v
⊢ ‖↑g x‖ ≤ ‖indicator v (fun _x => 1) x‖
[PROOFSTEP]
simp only [hx, abs_of_nonneg (hg_range x).1, (hg_range x).2, Real.norm_eq_abs, indicator_of_mem, CstarRing.norm_one]
[GOAL]
case neg
α : 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✝ : Measure.OuterRegular μ
hp : p ≠ ⊤
s u : Set α
s_closed : IsClosed s
u_open : IsOpen u
hsu : s ⊆ u
hs : ↑↑μ s ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (indicator s fun _x => c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen V
h'V : ↑↑μ V < ⊤
hV : ↑↑μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : ↑↑μ v < ⊤
g : C(α, ℝ)
hgv : EqOn (↑g) 0 (u ∩ V)ᶜ
hgs : EqOn (↑g) 1 s
hg_range : ∀ (x : α), ↑g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖↑g x‖ = ↑g x
gc_bd0 : ∀ (x : α), ‖↑g x • c‖ ≤ ‖c‖
gc_bd : ∀ (x : α), ‖↑g x • c - indicator s (fun _x => c) x‖ ≤ ‖indicator (v \ s) (fun _x => c) x‖
gc_support : (Function.support fun x => ↑g x • c) ⊆ v
this : snorm (indicator v fun _x => 1) p μ < ⊤
x : α
hx : ¬x ∈ v
⊢ ‖↑g x‖ ≤ ‖indicator v (fun _x => 1) x‖
[PROOFSTEP]
simp only [hgv hx, Pi.zero_apply, Real.norm_eq_abs, abs_zero, abs_nonneg]
[GOAL]
case intro.intro.intro.intro.intro.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✝ : Measure.OuterRegular μ
hp : p ≠ ⊤
s u : Set α
s_closed : IsClosed s
u_open : IsOpen u
hsu : s ⊆ u
hs : ↑↑μ s ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (indicator s fun _x => c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen V
h'V : ↑↑μ V < ⊤
hV : ↑↑μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : ↑↑μ v < ⊤
g : C(α, ℝ)
hgv : EqOn (↑g) 0 (u ∩ V)ᶜ
hgs : EqOn (↑g) 1 s
hg_range : ∀ (x : α), ↑g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖↑g x‖ = ↑g x
gc_bd0 : ∀ (x : α), ‖↑g x • c‖ ≤ ‖c‖
gc_bd : ∀ (x : α), ‖↑g x • c - indicator s (fun _x => c) x‖ ≤ ‖indicator (v \ s) (fun _x => c) x‖
gc_support : (Function.support fun x => ↑g x • c) ⊆ v
gc_mem : Memℒp (fun x => ↑g x • c) p
⊢ ∃ f,
    Continuous f ∧
      snorm (fun x => f x - indicator s (fun _y => c) x) p μ ≤ ε ∧
        (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ Memℒp f p
[PROOFSTEP]
refine'
  ⟨fun x => g x • c, g.continuous.smul continuous_const, (snorm_mono gc_bd).trans _, gc_bd0,
    gc_support.trans (inter_subset_left _ _), gc_mem⟩
[GOAL]
case intro.intro.intro.intro.intro.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✝ : Measure.OuterRegular μ
hp : p ≠ ⊤
s u : Set α
s_closed : IsClosed s
u_open : IsOpen u
hsu : s ⊆ u
hs : ↑↑μ s ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (indicator s fun _x => c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen V
h'V : ↑↑μ V < ⊤
hV : ↑↑μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : ↑↑μ v < ⊤
g : C(α, ℝ)
hgv : EqOn (↑g) 0 (u ∩ V)ᶜ
hgs : EqOn (↑g) 1 s
hg_range : ∀ (x : α), ↑g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖↑g x‖ = ↑g x
gc_bd0 : ∀ (x : α), ‖↑g x • c‖ ≤ ‖c‖
gc_bd : ∀ (x : α), ‖↑g x • c - indicator s (fun _x => c) x‖ ≤ ‖indicator (v \ s) (fun _x => c) x‖
gc_support : (Function.support fun x => ↑g x • c) ⊆ v
gc_mem : Memℒp (fun x => ↑g x • c) p
⊢ snorm (fun x => indicator (v \ s) (fun _x => c) x) p μ ≤ ε
[PROOFSTEP]
exact hη _ ((measure_mono (diff_subset_diff (inter_subset_right _ _) Subset.rfl)).trans hV.le)
[GOAL]
α : 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 μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ g, HasCompactSupport g ∧ snorm (f - g) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p
[PROOFSTEP]
suffices H : ∃ g : α → E, snorm (f - g) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p μ ∧ HasCompactSupport g
[GOAL]
α : 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 μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε : ℝ≥0∞
hε : ε ≠ 0
H : ∃ g, snorm (f - g) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p ∧ HasCompactSupport g
⊢ ∃ g, HasCompactSupport g ∧ snorm (f - g) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p
[PROOFSTEP]
rcases H with ⟨g, hg, g_cont, g_mem, g_support⟩
[GOAL]
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 μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε : ℝ≥0∞
hε : ε ≠ 0
g : α → E
hg : snorm (f - g) p μ ≤ ε
g_cont : Continuous g
g_mem : Memℒp g p
g_support : HasCompactSupport g
⊢ ∃ g, HasCompactSupport g ∧ snorm (f - g) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p
[PROOFSTEP]
exact
  ⟨g, g_support, hg, g_cont, g_mem⟩
    -- It suffices to check that the set of functions we consider approximates characteristic
      -- functions, is stable under addition and consists of ae strongly measurable functions.
      -- First check the latter easy facts.
[GOAL]
case 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 μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ g, snorm (f - g) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p ∧ HasCompactSupport g
[PROOFSTEP]
apply hf.induction_dense hp _ _ _ _ hε
[GOAL]
α : 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 μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      ↑↑μ s < ⊤ →
        ∀ {ε : ℝ≥0∞},
          ε ≠ 0 → ∃ g, snorm (g - Set.indicator s fun x => c) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p ∧ HasCompactSupport g
α : 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 μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∀ (f g : α → E),
    Continuous f ∧ Memℒp f p ∧ HasCompactSupport f →
      Continuous g ∧ Memℒp g p ∧ HasCompactSupport g → Continuous (f + g) ∧ Memℒp (f + g) p ∧ HasCompactSupport (f + g)
α : 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 μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∀ (f : α → E), Continuous f ∧ Memℒp f p ∧ HasCompactSupport f → AEStronglyMeasurable f μ
[PROOFSTEP]
rotate_left
  -- stability under addition
[GOAL]
α : 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 μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∀ (f g : α → E),
    Continuous f ∧ Memℒp f p ∧ HasCompactSupport f →
      Continuous g ∧ Memℒp g p ∧ HasCompactSupport g → Continuous (f + g) ∧ Memℒp (f + g) p ∧ HasCompactSupport (f + g)
[PROOFSTEP]
rintro f g ⟨f_cont, f_mem, hf⟩ ⟨g_cont, g_mem, hg⟩
[GOAL]
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 μ
hp : p ≠ ⊤
f✝ : α → E
hf✝ : Memℒp f✝ p
ε : ℝ≥0∞
hε : ε ≠ 0
f g : α → E
f_cont : Continuous f
f_mem : Memℒp f p
hf : HasCompactSupport f
g_cont : Continuous g
g_mem : Memℒp g p
hg : HasCompactSupport g
⊢ Continuous (f + g) ∧ Memℒp (f + g) p ∧ HasCompactSupport (f + g)
[PROOFSTEP]
exact
  ⟨f_cont.add g_cont, f_mem.add g_mem, hf.add hg⟩
    -- ae strong measurability
[GOAL]
α : 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 μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∀ (f : α → E), Continuous f ∧ Memℒp f p ∧ HasCompactSupport f → AEStronglyMeasurable f μ
[PROOFSTEP]
rintro f ⟨_f_cont, f_mem, _hf⟩
[GOAL]
case 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 μ
hp : p ≠ ⊤
f✝ : α → E
hf : Memℒp f✝ p
ε : ℝ≥0∞
hε : ε ≠ 0
f : α → E
_f_cont : Continuous f
f_mem : Memℒp f p
_hf : HasCompactSupport f
⊢ AEStronglyMeasurable f μ
[PROOFSTEP]
exact f_mem.aestronglyMeasurable
[GOAL]
α : 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 μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      ↑↑μ s < ⊤ →
        ∀ {ε : ℝ≥0∞},
          ε ≠ 0 → ∃ g, snorm (g - Set.indicator s fun x => c) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p ∧ HasCompactSupport g
[PROOFSTEP]
intro c t ht htμ ε hε
[GOAL]
α : 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 μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : ↑↑μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ g, snorm (g - Set.indicator t fun x => c) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p ∧ HasCompactSupport g
[PROOFSTEP]
rcases exists_Lp_half E μ p hε with ⟨δ, δpos, hδ⟩
[GOAL]
case 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 μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : ↑↑μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → snorm f p μ ≤ δ → snorm g p μ ≤ δ → snorm (f + g) p μ < ε
⊢ ∃ g, snorm (g - Set.indicator t fun x => c) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p ∧ HasCompactSupport g
[PROOFSTEP]
obtain ⟨η, ηpos, hη⟩ : ∃ η : ℝ≥0, 0 < η ∧ ∀ s : Set α, μ s ≤ η → snorm (s.indicator fun _x => c) p μ ≤ δ
[GOAL]
α : 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 μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : ↑↑μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → snorm f p μ ≤ δ → snorm g p μ ≤ δ → snorm (f + g) p μ < ε
⊢ ∃ η, 0 < η ∧ ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun _x => c) 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 μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : ↑↑μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → snorm f p μ ≤ δ → snorm g p μ ≤ δ → snorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun _x => c) p μ ≤ δ
⊢ ∃ g, snorm (g - Set.indicator t fun x => c) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p ∧ HasCompactSupport g
[PROOFSTEP]
exact exists_snorm_indicator_le hp c δpos.ne'
[GOAL]
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 μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : ↑↑μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → snorm f p μ ≤ δ → snorm g p μ ≤ δ → snorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun _x => c) p μ ≤ δ
⊢ ∃ g, snorm (g - Set.indicator t fun x => c) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p ∧ HasCompactSupport g
[PROOFSTEP]
have hη_pos' : (0 : ℝ≥0∞) < η := ENNReal.coe_pos.2 ηpos
[GOAL]
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 μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : ↑↑μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → snorm f p μ ≤ δ → snorm g p μ ≤ δ → snorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun _x => c) p μ ≤ δ
hη_pos' : 0 < ↑η
⊢ ∃ g, snorm (g - Set.indicator t fun x => c) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p ∧ HasCompactSupport g
[PROOFSTEP]
obtain ⟨s, st, s_compact, μs⟩ : ∃ s, s ⊆ t ∧ IsCompact s ∧ μ (t \ s) < η
[GOAL]
α : 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 μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : ↑↑μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → snorm f p μ ≤ δ → snorm g p μ ≤ δ → snorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun _x => c) p μ ≤ δ
hη_pos' : 0 < ↑η
⊢ ∃ s, s ⊆ t ∧ IsCompact s ∧ ↑↑μ (t \ s) < ↑η
case intro.intro.intro.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 μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : ↑↑μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → snorm f p μ ≤ δ → snorm g p μ ≤ δ → snorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun _x => c) p μ ≤ δ
hη_pos' : 0 < ↑η
s : Set α
st : s ⊆ t
s_compact : IsCompact s
μs : ↑↑μ (t \ s) < ↑η
⊢ ∃ g, snorm (g - Set.indicator t fun x => c) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p ∧ HasCompactSupport g
[PROOFSTEP]
exact ht.exists_isCompact_diff_lt htμ.ne hη_pos'.ne'
[GOAL]
case intro.intro.intro.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 μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : ↑↑μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → snorm f p μ ≤ δ → snorm g p μ ≤ δ → snorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun _x => c) p μ ≤ δ
hη_pos' : 0 < ↑η
s : Set α
st : s ⊆ t
s_compact : IsCompact s
μs : ↑↑μ (t \ s) < ↑η
⊢ ∃ g, snorm (g - Set.indicator t fun x => c) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p ∧ HasCompactSupport g
[PROOFSTEP]
have hsμ : μ s < ∞ := (measure_mono st).trans_lt htμ
[GOAL]
case intro.intro.intro.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 μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : ↑↑μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → snorm f p μ ≤ δ → snorm g p μ ≤ δ → snorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun _x => c) p μ ≤ δ
hη_pos' : 0 < ↑η
s : Set α
st : s ⊆ t
s_compact : IsCompact s
μs : ↑↑μ (t \ s) < ↑η
hsμ : ↑↑μ s < ⊤
⊢ ∃ g, snorm (g - Set.indicator t fun x => c) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p ∧ HasCompactSupport g
[PROOFSTEP]
have I1 : snorm ((s.indicator fun _y => c) - t.indicator fun _y => c) p μ ≤ δ :=
  by
  rw [← snorm_neg, neg_sub, ← indicator_diff st]
  exact hη _ μs.le
[GOAL]
α : 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 μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : ↑↑μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → snorm f p μ ≤ δ → snorm g p μ ≤ δ → snorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun _x => c) p μ ≤ δ
hη_pos' : 0 < ↑η
s : Set α
st : s ⊆ t
s_compact : IsCompact s
μs : ↑↑μ (t \ s) < ↑η
hsμ : ↑↑μ s < ⊤
⊢ snorm ((Set.indicator s fun _y => c) - Set.indicator t fun _y => c) p μ ≤ δ
[PROOFSTEP]
rw [← snorm_neg, neg_sub, ← indicator_diff st]
[GOAL]
α : 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 μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : ↑↑μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → snorm f p μ ≤ δ → snorm g p μ ≤ δ → snorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun _x => c) p μ ≤ δ
hη_pos' : 0 < ↑η
s : Set α
st : s ⊆ t
s_compact : IsCompact s
μs : ↑↑μ (t \ s) < ↑η
hsμ : ↑↑μ s < ⊤
⊢ snorm (Set.indicator (t \ s) fun _y => c) p μ ≤ δ
[PROOFSTEP]
exact hη _ μs.le
[GOAL]
case intro.intro.intro.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 μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : ↑↑μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → snorm f p μ ≤ δ → snorm g p μ ≤ δ → snorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun _x => c) p μ ≤ δ
hη_pos' : 0 < ↑η
s : Set α
st : s ⊆ t
s_compact : IsCompact s
μs : ↑↑μ (t \ s) < ↑η
hsμ : ↑↑μ s < ⊤
I1 : snorm ((Set.indicator s fun _y => c) - Set.indicator t fun _y => c) p μ ≤ δ
⊢ ∃ g, snorm (g - Set.indicator t fun x => c) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p ∧ HasCompactSupport g
[PROOFSTEP]
obtain ⟨k, k_compact, sk⟩ : ∃ k : Set α, IsCompact k ∧ s ⊆ interior k := exists_compact_superset s_compact
[GOAL]
case intro.intro.intro.intro.intro.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 μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : ↑↑μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → snorm f p μ ≤ δ → snorm g p μ ≤ δ → snorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun _x => c) p μ ≤ δ
hη_pos' : 0 < ↑η
s : Set α
st : s ⊆ t
s_compact : IsCompact s
μs : ↑↑μ (t \ s) < ↑η
hsμ : ↑↑μ s < ⊤
I1 : snorm ((Set.indicator s fun _y => c) - Set.indicator t fun _y => c) p μ ≤ δ
k : Set α
k_compact : IsCompact k
sk : s ⊆ interior k
⊢ ∃ g, snorm (g - Set.indicator t fun x => c) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p ∧ HasCompactSupport g
[PROOFSTEP]
rcases exists_continuous_snorm_sub_le_of_closed hp s_compact.isClosed isOpen_interior sk hsμ.ne c δpos.ne' with
  ⟨f, f_cont, I2, _f_bound, f_support, f_mem⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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 μ
hp : p ≠ ⊤
f✝ : α → E
hf : Memℒp f✝ p
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : ↑↑μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → snorm f p μ ≤ δ → snorm g p μ ≤ δ → snorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun _x => c) p μ ≤ δ
hη_pos' : 0 < ↑η
s : Set α
st : s ⊆ t
s_compact : IsCompact s
μs : ↑↑μ (t \ s) < ↑η
hsμ : ↑↑μ s < ⊤
I1 : snorm ((Set.indicator s fun _y => c) - Set.indicator t fun _y => c) p μ ≤ δ
k : Set α
k_compact : IsCompact k
sk : s ⊆ interior k
f : α → E
f_cont : Continuous f
I2 : snorm (fun x => f x - Set.indicator s (fun _y => c) x) p μ ≤ δ
_f_bound : ∀ (x : α), ‖f x‖ ≤ ‖c‖
f_support : Function.support f ⊆ interior k
f_mem : Memℒp f p
⊢ ∃ g, snorm (g - Set.indicator t fun x => c) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p ∧ HasCompactSupport g
[PROOFSTEP]
have I3 : snorm (f - t.indicator fun _y => c) p μ ≤ ε :=
  by
  convert
    (hδ _ _ (f_mem.aestronglyMeasurable.sub (aestronglyMeasurable_const.indicator s_compact.measurableSet))
        ((aestronglyMeasurable_const.indicator s_compact.measurableSet).sub (aestronglyMeasurable_const.indicator ht))
        I2 I1).le using
    2
  simp only [sub_add_sub_cancel]
[GOAL]
α : 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 μ
hp : p ≠ ⊤
f✝ : α → E
hf : Memℒp f✝ p
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : ↑↑μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → snorm f p μ ≤ δ → snorm g p μ ≤ δ → snorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun _x => c) p μ ≤ δ
hη_pos' : 0 < ↑η
s : Set α
st : s ⊆ t
s_compact : IsCompact s
μs : ↑↑μ (t \ s) < ↑η
hsμ : ↑↑μ s < ⊤
I1 : snorm ((Set.indicator s fun _y => c) - Set.indicator t fun _y => c) p μ ≤ δ
k : Set α
k_compact : IsCompact k
sk : s ⊆ interior k
f : α → E
f_cont : Continuous f
I2 : snorm (fun x => f x - Set.indicator s (fun _y => c) x) p μ ≤ δ
_f_bound : ∀ (x : α), ‖f x‖ ≤ ‖c‖
f_support : Function.support f ⊆ interior k
f_mem : Memℒp f p
⊢ snorm (f - Set.indicator t fun _y => c) p μ ≤ ε
[PROOFSTEP]
convert
  (hδ _ _ (f_mem.aestronglyMeasurable.sub (aestronglyMeasurable_const.indicator s_compact.measurableSet))
      ((aestronglyMeasurable_const.indicator s_compact.measurableSet).sub (aestronglyMeasurable_const.indicator ht)) I2
      I1).le using
  2
[GOAL]
case h.e'_3.h.e'_5
α : 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 μ
hp : p ≠ ⊤
f✝ : α → E
hf : Memℒp f✝ p
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : ↑↑μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → snorm f p μ ≤ δ → snorm g p μ ≤ δ → snorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun _x => c) p μ ≤ δ
hη_pos' : 0 < ↑η
s : Set α
st : s ⊆ t
s_compact : IsCompact s
μs : ↑↑μ (t \ s) < ↑η
hsμ : ↑↑μ s < ⊤
I1 : snorm ((Set.indicator s fun _y => c) - Set.indicator t fun _y => c) p μ ≤ δ
k : Set α
k_compact : IsCompact k
sk : s ⊆ interior k
f : α → E
f_cont : Continuous f
I2 : snorm (fun x => f x - Set.indicator s (fun _y => c) x) p μ ≤ δ
_f_bound : ∀ (x : α), ‖f x‖ ≤ ‖c‖
f_support : Function.support f ⊆ interior k
f_mem : Memℒp f p
⊢ (f - Set.indicator t fun _y => c) =
    (f - Set.indicator s fun x => c) + ((Set.indicator s fun x => c) - Set.indicator t fun x => c)
[PROOFSTEP]
simp only [sub_add_sub_cancel]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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 μ
hp : p ≠ ⊤
f✝ : α → E
hf : Memℒp f✝ p
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : ↑↑μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → snorm f p μ ≤ δ → snorm g p μ ≤ δ → snorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun _x => c) p μ ≤ δ
hη_pos' : 0 < ↑η
s : Set α
st : s ⊆ t
s_compact : IsCompact s
μs : ↑↑μ (t \ s) < ↑η
hsμ : ↑↑μ s < ⊤
I1 : snorm ((Set.indicator s fun _y => c) - Set.indicator t fun _y => c) p μ ≤ δ
k : Set α
k_compact : IsCompact k
sk : s ⊆ interior k
f : α → E
f_cont : Continuous f
I2 : snorm (fun x => f x - Set.indicator s (fun _y => c) x) p μ ≤ δ
_f_bound : ∀ (x : α), ‖f x‖ ≤ ‖c‖
f_support : Function.support f ⊆ interior k
f_mem : Memℒp f p
I3 : snorm (f - Set.indicator t fun _y => c) p μ ≤ ε
⊢ ∃ g, snorm (g - Set.indicator t fun x => c) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p ∧ HasCompactSupport g
[PROOFSTEP]
refine' ⟨f, I3, f_cont, f_mem, HasCompactSupport.intro k_compact fun x hx => _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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 μ
hp : p ≠ ⊤
f✝ : α → E
hf : Memℒp f✝ p
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : ↑↑μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → snorm f p μ ≤ δ → snorm g p μ ≤ δ → snorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun _x => c) p μ ≤ δ
hη_pos' : 0 < ↑η
s : Set α
st : s ⊆ t
s_compact : IsCompact s
μs : ↑↑μ (t \ s) < ↑η
hsμ : ↑↑μ s < ⊤
I1 : snorm ((Set.indicator s fun _y => c) - Set.indicator t fun _y => c) p μ ≤ δ
k : Set α
k_compact : IsCompact k
sk : s ⊆ interior k
f : α → E
f_cont : Continuous f
I2 : snorm (fun x => f x - Set.indicator s (fun _y => c) x) p μ ≤ δ
_f_bound : ∀ (x : α), ‖f x‖ ≤ ‖c‖
f_support : Function.support f ⊆ interior k
f_mem : Memℒp f p
I3 : snorm (f - Set.indicator t fun _y => c) p μ ≤ ε
x : α
hx : ¬x ∈ k
⊢ f x = 0
[PROOFSTEP]
rw [← Function.nmem_support]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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 μ
hp : p ≠ ⊤
f✝ : α → E
hf : Memℒp f✝ p
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : ↑↑μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → snorm f p μ ≤ δ → snorm g p μ ≤ δ → snorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun _x => c) p μ ≤ δ
hη_pos' : 0 < ↑η
s : Set α
st : s ⊆ t
s_compact : IsCompact s
μs : ↑↑μ (t \ s) < ↑η
hsμ : ↑↑μ s < ⊤
I1 : snorm ((Set.indicator s fun _y => c) - Set.indicator t fun _y => c) p μ ≤ δ
k : Set α
k_compact : IsCompact k
sk : s ⊆ interior k
f : α → E
f_cont : Continuous f
I2 : snorm (fun x => f x - Set.indicator s (fun _y => c) x) p μ ≤ δ
_f_bound : ∀ (x : α), ‖f x‖ ≤ ‖c‖
f_support : Function.support f ⊆ interior k
f_mem : Memℒp f p
I3 : snorm (f - Set.indicator t fun _y => c) p μ ≤ ε
x : α
hx : ¬x ∈ k
⊢ ¬x ∈ Function.support f
[PROOFSTEP]
contrapose! hx
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.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 μ
hp : p ≠ ⊤
f✝ : α → E
hf : Memℒp f✝ p
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : ↑↑μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → snorm f p μ ≤ δ → snorm g p μ ≤ δ → snorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun _x => c) p μ ≤ δ
hη_pos' : 0 < ↑η
s : Set α
st : s ⊆ t
s_compact : IsCompact s
μs : ↑↑μ (t \ s) < ↑η
hsμ : ↑↑μ s < ⊤
I1 : snorm ((Set.indicator s fun _y => c) - Set.indicator t fun _y => c) p μ ≤ δ
k : Set α
k_compact : IsCompact k
sk : s ⊆ interior k
f : α → E
f_cont : Continuous f
I2 : snorm (fun x => f x - Set.indicator s (fun _y => c) x) p μ ≤ δ
_f_bound : ∀ (x : α), ‖f x‖ ≤ ‖c‖
f_support : Function.support f ⊆ interior k
f_mem : Memℒp f p
I3 : snorm (f - Set.indicator t fun _y => c) p μ ≤ ε
x : α
hx : x ∈ Function.support f
⊢ x ∈ k
[PROOFSTEP]
exact interior_subset (f_support hx)
[GOAL]
α : 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)
[PROOFSTEP]
have I : 0 < ε ^ (1 / p) := Real.rpow_pos_of_pos hε _
[GOAL]
α : 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)
[PROOFSTEP]
have A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0 := by simp only [Ne.def, ENNReal.ofReal_eq_zero, not_le, I]
[GOAL]
α : 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
[PROOFSTEP]
simp only [Ne.def, ENNReal.ofReal_eq_zero, not_le, I]
[GOAL]
α : 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)
[PROOFSTEP]
have B : ENNReal.ofReal p ≠ 0 := by simpa only [Ne.def, ENNReal.ofReal_eq_zero, not_le] using hp
[GOAL]
α : 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
[PROOFSTEP]
simpa only [Ne.def, ENNReal.ofReal_eq_zero, not_le] using hp
[GOAL]
α : 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)
[PROOFSTEP]
rcases hf.exists_hasCompactSupport_snorm_sub_le ENNReal.coe_ne_top A with ⟨g, g_support, hg, g_cont, g_mem⟩
[GOAL]
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)
[PROOFSTEP]
change snorm _ (ENNReal.ofReal p) _ ≤ _ at hg 
[GOAL]
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)
[PROOFSTEP]
refine' ⟨g, g_support, _, g_cont, g_mem⟩
[GOAL]
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 ∂μ ≤ ε
[PROOFSTEP]
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 
[GOAL]
α : 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 ∂μ
[PROOFSTEP]
exact integral_nonneg fun x => Real.rpow_nonneg_of_nonneg (norm_nonneg _) _
[GOAL]
α : 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 μ
f : α → E
hf : Integrable f
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ g, HasCompactSupport g ∧ ∫⁻ (x : α), ↑‖f x - g x‖₊ ∂μ ≤ ε ∧ Continuous g ∧ Integrable g
[PROOFSTEP]
simp only [← memℒp_one_iff_integrable, ← snorm_one_eq_lintegral_nnnorm] at hf ⊢
[GOAL]
α : 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 μ
f : α → E
ε : ℝ≥0∞
hε : ε ≠ 0
hf : Memℒp f 1
⊢ ∃ g, HasCompactSupport g ∧ snorm (fun x => f x - g x) 1 μ ≤ ε ∧ Continuous g ∧ Memℒp g 1
[PROOFSTEP]
exact hf.exists_hasCompactSupport_snorm_sub_le ENNReal.one_ne_top hε
[GOAL]
α : 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 μ
f : α → E
hf : Integrable f
ε : ℝ
hε : 0 < ε
⊢ ∃ g, HasCompactSupport g ∧ ∫ (x : α), ‖f x - g x‖ ∂μ ≤ ε ∧ Continuous g ∧ Integrable g
[PROOFSTEP]
simp only [← memℒp_one_iff_integrable, ← snorm_one_eq_lintegral_nnnorm, ← ENNReal.ofReal_one] at hf ⊢
[GOAL]
α : 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 μ
f : α → E
ε : ℝ
hε : 0 < ε
hf : Memℒp f (ENNReal.ofReal 1)
⊢ ∃ g, HasCompactSupport g ∧ ∫ (x : α), ‖f x - g x‖ ∂μ ≤ ε ∧ Continuous g ∧ Memℒp g (ENNReal.ofReal 1)
[PROOFSTEP]
simpa using hf.exists_hasCompactSupport_integral_rpow_sub_le zero_lt_one hε
[GOAL]
α : 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✝ : Measure.WeaklyRegular μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ g, snorm (f - ↑g) p μ ≤ ε ∧ Memℒp (↑g) p
[PROOFSTEP]
suffices H : ∃ g : α → E, snorm (f - g) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p μ ∧ Metric.Bounded (range g)
[GOAL]
α : 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✝ : Measure.WeaklyRegular μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε : ℝ≥0∞
hε : ε ≠ 0
H : ∃ g, snorm (f - g) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p ∧ Metric.Bounded (range g)
⊢ ∃ g, snorm (f - ↑g) p μ ≤ ε ∧ Memℒp (↑g) p
[PROOFSTEP]
rcases H with ⟨g, hg, g_cont, g_mem, g_bd⟩
[GOAL]
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✝ : Measure.WeaklyRegular μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε : ℝ≥0∞
hε : ε ≠ 0
g : α → E
hg : snorm (f - g) p μ ≤ ε
g_cont : Continuous g
g_mem : Memℒp g p
g_bd : Metric.Bounded (range g)
⊢ ∃ g, snorm (f - ↑g) p μ ≤ ε ∧ Memℒp (↑g) p
[PROOFSTEP]
exact
  ⟨⟨⟨g, g_cont⟩, Metric.bounded_range_iff.1 g_bd⟩, hg, g_mem⟩
    -- It suffices to check that the set of functions we consider approximates characteristic
      -- functions, is stable under addition and made of ae strongly measurable functions.
      -- First check the latter easy facts.
[GOAL]
case 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✝ : Measure.WeaklyRegular μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ g, snorm (f - g) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p ∧ Metric.Bounded (range g)
[PROOFSTEP]
apply hf.induction_dense hp _ _ _ _ hε
[GOAL]
α : 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✝ : Measure.WeaklyRegular μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      ↑↑μ s < ⊤ →
        ∀ {ε : ℝ≥0∞},
          ε ≠ 0 →
            ∃ g, snorm (g - Set.indicator s fun x => c) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p ∧ Metric.Bounded (range g)
α : 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✝ : Measure.WeaklyRegular μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∀ (f g : α → E),
    Continuous f ∧ Memℒp f p ∧ Metric.Bounded (range f) →
      Continuous g ∧ Memℒp g p ∧ Metric.Bounded (range g) →
        Continuous (f + g) ∧ Memℒp (f + g) p ∧ Metric.Bounded (range (f + g))
α : 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✝ : Measure.WeaklyRegular μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∀ (f : α → E), Continuous f ∧ Memℒp f p ∧ Metric.Bounded (range f) → AEStronglyMeasurable f μ
[PROOFSTEP]
rotate_left
  -- stability under addition
[GOAL]
α : 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✝ : Measure.WeaklyRegular μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∀ (f g : α → E),
    Continuous f ∧ Memℒp f p ∧ Metric.Bounded (range f) →
      Continuous g ∧ Memℒp g p ∧ Metric.Bounded (range g) →
        Continuous (f + g) ∧ Memℒp (f + g) p ∧ Metric.Bounded (range (f + g))
[PROOFSTEP]
rintro f g ⟨f_cont, f_mem, f_bd⟩ ⟨g_cont, g_mem, g_bd⟩
[GOAL]
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✝ : Measure.WeaklyRegular μ
hp : p ≠ ⊤
f✝ : α → E
hf : Memℒp f✝ p
ε : ℝ≥0∞
hε : ε ≠ 0
f g : α → E
f_cont : Continuous f
f_mem : Memℒp f p
f_bd : Metric.Bounded (range f)
g_cont : Continuous g
g_mem : Memℒp g p
g_bd : Metric.Bounded (range g)
⊢ Continuous (f + g) ∧ Memℒp (f + g) p ∧ Metric.Bounded (range (f + g))
[PROOFSTEP]
refine' ⟨f_cont.add g_cont, f_mem.add g_mem, _⟩
[GOAL]
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✝ : Measure.WeaklyRegular μ
hp : p ≠ ⊤
f✝ : α → E
hf : Memℒp f✝ p
ε : ℝ≥0∞
hε : ε ≠ 0
f g : α → E
f_cont : Continuous f
f_mem : Memℒp f p
f_bd : Metric.Bounded (range f)
g_cont : Continuous g
g_mem : Memℒp g p
g_bd : Metric.Bounded (range g)
⊢ Metric.Bounded (range (f + g))
[PROOFSTEP]
let f' : α →ᵇ E := ⟨⟨f, f_cont⟩, Metric.bounded_range_iff.1 f_bd⟩
[GOAL]
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✝ : Measure.WeaklyRegular μ
hp : p ≠ ⊤
f✝ : α → E
hf : Memℒp f✝ p
ε : ℝ≥0∞
hε : ε ≠ 0
f g : α → E
f_cont : Continuous f
f_mem : Memℒp f p
f_bd : Metric.Bounded (range f)
g_cont : Continuous g
g_mem : Memℒp g p
g_bd : Metric.Bounded (range g)
f' : α →ᵇ E :=
  { toContinuousMap := ContinuousMap.mk f,
    map_bounded' :=
      (_ :
        ∃ C,
          ∀ (x y : α),
            dist (ContinuousMap.toFun (ContinuousMap.mk f) x) (ContinuousMap.toFun (ContinuousMap.mk f) y) ≤ C) }
⊢ Metric.Bounded (range (f + g))
[PROOFSTEP]
let g' : α →ᵇ E := ⟨⟨g, g_cont⟩, Metric.bounded_range_iff.1 g_bd⟩
[GOAL]
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✝ : Measure.WeaklyRegular μ
hp : p ≠ ⊤
f✝ : α → E
hf : Memℒp f✝ p
ε : ℝ≥0∞
hε : ε ≠ 0
f g : α → E
f_cont : Continuous f
f_mem : Memℒp f p
f_bd : Metric.Bounded (range f)
g_cont : Continuous g
g_mem : Memℒp g p
g_bd : Metric.Bounded (range g)
f' : α →ᵇ E :=
  { toContinuousMap := ContinuousMap.mk f,
    map_bounded' :=
      (_ :
        ∃ C,
          ∀ (x y : α),
            dist (ContinuousMap.toFun (ContinuousMap.mk f) x) (ContinuousMap.toFun (ContinuousMap.mk f) y) ≤ C) }
g' : α →ᵇ E :=
  { toContinuousMap := ContinuousMap.mk g,
    map_bounded' :=
      (_ :
        ∃ C,
          ∀ (x y : α),
            dist (ContinuousMap.toFun (ContinuousMap.mk g) x) (ContinuousMap.toFun (ContinuousMap.mk g) y) ≤ C) }
⊢ Metric.Bounded (range (f + g))
[PROOFSTEP]
exact (f' + g').bounded_range
[GOAL]
α : 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✝ : Measure.WeaklyRegular μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∀ (f : α → E), Continuous f ∧ Memℒp f p ∧ Metric.Bounded (range f) → AEStronglyMeasurable f μ
[PROOFSTEP]
exact fun f ⟨_, h, _⟩ => h.aestronglyMeasurable
[GOAL]
α : 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✝ : Measure.WeaklyRegular μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      ↑↑μ s < ⊤ →
        ∀ {ε : ℝ≥0∞},
          ε ≠ 0 →
            ∃ g, snorm (g - Set.indicator s fun x => c) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p ∧ Metric.Bounded (range g)
[PROOFSTEP]
intro c t ht htμ ε hε
[GOAL]
α : 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✝ : Measure.WeaklyRegular μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : ↑↑μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ g, snorm (g - Set.indicator t fun x => c) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p ∧ Metric.Bounded (range g)
[PROOFSTEP]
rcases exists_Lp_half E μ p hε with ⟨δ, δpos, hδ⟩
[GOAL]
case 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✝ : Measure.WeaklyRegular μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : ↑↑μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → snorm f p μ ≤ δ → snorm g p μ ≤ δ → snorm (f + g) p μ < ε
⊢ ∃ g, snorm (g - Set.indicator t fun x => c) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p ∧ Metric.Bounded (range g)
[PROOFSTEP]
obtain ⟨η, ηpos, hη⟩ : ∃ η : ℝ≥0, 0 < η ∧ ∀ s : Set α, μ s ≤ η → snorm (s.indicator fun _x => c) p μ ≤ δ
[GOAL]
α : 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✝ : Measure.WeaklyRegular μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : ↑↑μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → snorm f p μ ≤ δ → snorm g p μ ≤ δ → snorm (f + g) p μ < ε
⊢ ∃ η, 0 < η ∧ ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun _x => c) 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✝ : Measure.WeaklyRegular μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : ↑↑μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → snorm f p μ ≤ δ → snorm g p μ ≤ δ → snorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun _x => c) p μ ≤ δ
⊢ ∃ g, snorm (g - Set.indicator t fun x => c) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p ∧ Metric.Bounded (range g)
[PROOFSTEP]
exact exists_snorm_indicator_le hp c δpos.ne'
[GOAL]
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✝ : Measure.WeaklyRegular μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : ↑↑μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → snorm f p μ ≤ δ → snorm g p μ ≤ δ → snorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun _x => c) p μ ≤ δ
⊢ ∃ g, snorm (g - Set.indicator t fun x => c) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p ∧ Metric.Bounded (range g)
[PROOFSTEP]
have hη_pos' : (0 : ℝ≥0∞) < η := ENNReal.coe_pos.2 ηpos
[GOAL]
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✝ : Measure.WeaklyRegular μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : ↑↑μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → snorm f p μ ≤ δ → snorm g p μ ≤ δ → snorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun _x => c) p μ ≤ δ
hη_pos' : 0 < ↑η
⊢ ∃ g, snorm (g - Set.indicator t fun x => c) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p ∧ Metric.Bounded (range g)
[PROOFSTEP]
obtain ⟨s, st, s_closed, μs⟩ : ∃ s, s ⊆ t ∧ IsClosed s ∧ μ (t \ s) < η
[GOAL]
α : 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✝ : Measure.WeaklyRegular μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : ↑↑μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → snorm f p μ ≤ δ → snorm g p μ ≤ δ → snorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun _x => c) p μ ≤ δ
hη_pos' : 0 < ↑η
⊢ ∃ s, s ⊆ t ∧ IsClosed s ∧ ↑↑μ (t \ s) < ↑η
case intro.intro.intro.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✝ : Measure.WeaklyRegular μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : ↑↑μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → snorm f p μ ≤ δ → snorm g p μ ≤ δ → snorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun _x => c) p μ ≤ δ
hη_pos' : 0 < ↑η
s : Set α
st : s ⊆ t
s_closed : IsClosed s
μs : ↑↑μ (t \ s) < ↑η
⊢ ∃ g, snorm (g - Set.indicator t fun x => c) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p ∧ Metric.Bounded (range g)
[PROOFSTEP]
exact ht.exists_isClosed_diff_lt htμ.ne hη_pos'.ne'
[GOAL]
case intro.intro.intro.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✝ : Measure.WeaklyRegular μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : ↑↑μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → snorm f p μ ≤ δ → snorm g p μ ≤ δ → snorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun _x => c) p μ ≤ δ
hη_pos' : 0 < ↑η
s : Set α
st : s ⊆ t
s_closed : IsClosed s
μs : ↑↑μ (t \ s) < ↑η
⊢ ∃ g, snorm (g - Set.indicator t fun x => c) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p ∧ Metric.Bounded (range g)
[PROOFSTEP]
have hsμ : μ s < ∞ := (measure_mono st).trans_lt htμ
[GOAL]
case intro.intro.intro.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✝ : Measure.WeaklyRegular μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : ↑↑μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → snorm f p μ ≤ δ → snorm g p μ ≤ δ → snorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun _x => c) p μ ≤ δ
hη_pos' : 0 < ↑η
s : Set α
st : s ⊆ t
s_closed : IsClosed s
μs : ↑↑μ (t \ s) < ↑η
hsμ : ↑↑μ s < ⊤
⊢ ∃ g, snorm (g - Set.indicator t fun x => c) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p ∧ Metric.Bounded (range g)
[PROOFSTEP]
have I1 : snorm ((s.indicator fun _y => c) - t.indicator fun _y => c) p μ ≤ δ :=
  by
  rw [← snorm_neg, neg_sub, ← indicator_diff st]
  exact hη _ μs.le
[GOAL]
α : 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✝ : Measure.WeaklyRegular μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : ↑↑μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → snorm f p μ ≤ δ → snorm g p μ ≤ δ → snorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun _x => c) p μ ≤ δ
hη_pos' : 0 < ↑η
s : Set α
st : s ⊆ t
s_closed : IsClosed s
μs : ↑↑μ (t \ s) < ↑η
hsμ : ↑↑μ s < ⊤
⊢ snorm ((Set.indicator s fun _y => c) - Set.indicator t fun _y => c) p μ ≤ δ
[PROOFSTEP]
rw [← snorm_neg, neg_sub, ← indicator_diff st]
[GOAL]
α : 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✝ : Measure.WeaklyRegular μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : ↑↑μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → snorm f p μ ≤ δ → snorm g p μ ≤ δ → snorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun _x => c) p μ ≤ δ
hη_pos' : 0 < ↑η
s : Set α
st : s ⊆ t
s_closed : IsClosed s
μs : ↑↑μ (t \ s) < ↑η
hsμ : ↑↑μ s < ⊤
⊢ snorm (Set.indicator (t \ s) fun _y => c) p μ ≤ δ
[PROOFSTEP]
exact hη _ μs.le
[GOAL]
case intro.intro.intro.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✝ : Measure.WeaklyRegular μ
hp : p ≠ ⊤
f : α → E
hf : Memℒp f p
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : ↑↑μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → snorm f p μ ≤ δ → snorm g p μ ≤ δ → snorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun _x => c) p μ ≤ δ
hη_pos' : 0 < ↑η
s : Set α
st : s ⊆ t
s_closed : IsClosed s
μs : ↑↑μ (t \ s) < ↑η
hsμ : ↑↑μ s < ⊤
I1 : snorm ((Set.indicator s fun _y => c) - Set.indicator t fun _y => c) p μ ≤ δ
⊢ ∃ g, snorm (g - Set.indicator t fun x => c) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p ∧ Metric.Bounded (range g)
[PROOFSTEP]
rcases exists_continuous_snorm_sub_le_of_closed hp s_closed isOpen_univ (subset_univ _) hsμ.ne c δpos.ne' with
  ⟨f, f_cont, I2, f_bound, -, f_mem⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.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✝ : Measure.WeaklyRegular μ
hp : p ≠ ⊤
f✝ : α → E
hf : Memℒp f✝ p
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : ↑↑μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → snorm f p μ ≤ δ → snorm g p μ ≤ δ → snorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun _x => c) p μ ≤ δ
hη_pos' : 0 < ↑η
s : Set α
st : s ⊆ t
s_closed : IsClosed s
μs : ↑↑μ (t \ s) < ↑η
hsμ : ↑↑μ s < ⊤
I1 : snorm ((Set.indicator s fun _y => c) - Set.indicator t fun _y => c) p μ ≤ δ
f : α → E
f_cont : Continuous f
I2 : snorm (fun x => f x - Set.indicator s (fun _y => c) x) p μ ≤ δ
f_bound : ∀ (x : α), ‖f x‖ ≤ ‖c‖
f_mem : Memℒp f p
⊢ ∃ g, snorm (g - Set.indicator t fun x => c) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p ∧ Metric.Bounded (range g)
[PROOFSTEP]
have I3 : snorm (f - t.indicator fun _y => c) p μ ≤ ε :=
  by
  convert
    (hδ _ _ (f_mem.aestronglyMeasurable.sub (aestronglyMeasurable_const.indicator s_closed.measurableSet))
        ((aestronglyMeasurable_const.indicator s_closed.measurableSet).sub (aestronglyMeasurable_const.indicator ht)) I2
        I1).le using
    2
  simp only [sub_add_sub_cancel]
[GOAL]
α : 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✝ : Measure.WeaklyRegular μ
hp : p ≠ ⊤
f✝ : α → E
hf : Memℒp f✝ p
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : ↑↑μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → snorm f p μ ≤ δ → snorm g p μ ≤ δ → snorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun _x => c) p μ ≤ δ
hη_pos' : 0 < ↑η
s : Set α
st : s ⊆ t
s_closed : IsClosed s
μs : ↑↑μ (t \ s) < ↑η
hsμ : ↑↑μ s < ⊤
I1 : snorm ((Set.indicator s fun _y => c) - Set.indicator t fun _y => c) p μ ≤ δ
f : α → E
f_cont : Continuous f
I2 : snorm (fun x => f x - Set.indicator s (fun _y => c) x) p μ ≤ δ
f_bound : ∀ (x : α), ‖f x‖ ≤ ‖c‖
f_mem : Memℒp f p
⊢ snorm (f - Set.indicator t fun _y => c) p μ ≤ ε
[PROOFSTEP]
convert
  (hδ _ _ (f_mem.aestronglyMeasurable.sub (aestronglyMeasurable_const.indicator s_closed.measurableSet))
      ((aestronglyMeasurable_const.indicator s_closed.measurableSet).sub (aestronglyMeasurable_const.indicator ht)) I2
      I1).le using
  2
[GOAL]
case h.e'_3.h.e'_5
α : 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✝ : Measure.WeaklyRegular μ
hp : p ≠ ⊤
f✝ : α → E
hf : Memℒp f✝ p
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : ↑↑μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → snorm f p μ ≤ δ → snorm g p μ ≤ δ → snorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun _x => c) p μ ≤ δ
hη_pos' : 0 < ↑η
s : Set α
st : s ⊆ t
s_closed : IsClosed s
μs : ↑↑μ (t \ s) < ↑η
hsμ : ↑↑μ s < ⊤
I1 : snorm ((Set.indicator s fun _y => c) - Set.indicator t fun _y => c) p μ ≤ δ
f : α → E
f_cont : Continuous f
I2 : snorm (fun x => f x - Set.indicator s (fun _y => c) x) p μ ≤ δ
f_bound : ∀ (x : α), ‖f x‖ ≤ ‖c‖
f_mem : Memℒp f p
⊢ (f - Set.indicator t fun _y => c) =
    (f - Set.indicator s fun x => c) + ((Set.indicator s fun x => c) - Set.indicator t fun x => c)
[PROOFSTEP]
simp only [sub_add_sub_cancel]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.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✝ : Measure.WeaklyRegular μ
hp : p ≠ ⊤
f✝ : α → E
hf : Memℒp f✝ p
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : ↑↑μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → snorm f p μ ≤ δ → snorm g p μ ≤ δ → snorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun _x => c) p μ ≤ δ
hη_pos' : 0 < ↑η
s : Set α
st : s ⊆ t
s_closed : IsClosed s
μs : ↑↑μ (t \ s) < ↑η
hsμ : ↑↑μ s < ⊤
I1 : snorm ((Set.indicator s fun _y => c) - Set.indicator t fun _y => c) p μ ≤ δ
f : α → E
f_cont : Continuous f
I2 : snorm (fun x => f x - Set.indicator s (fun _y => c) x) p μ ≤ δ
f_bound : ∀ (x : α), ‖f x‖ ≤ ‖c‖
f_mem : Memℒp f p
I3 : snorm (f - Set.indicator t fun _y => c) p μ ≤ ε
⊢ ∃ g, snorm (g - Set.indicator t fun x => c) p μ ≤ ε ∧ Continuous g ∧ Memℒp g p ∧ Metric.Bounded (range g)
[PROOFSTEP]
refine' ⟨f, I3, f_cont, f_mem, _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.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✝ : Measure.WeaklyRegular μ
hp : p ≠ ⊤
f✝ : α → E
hf : Memℒp f✝ p
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : ↑↑μ t < ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → snorm f p μ ≤ δ → snorm g p μ ≤ δ → snorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun _x => c) p μ ≤ δ
hη_pos' : 0 < ↑η
s : Set α
st : s ⊆ t
s_closed : IsClosed s
μs : ↑↑μ (t \ s) < ↑η
hsμ : ↑↑μ s < ⊤
I1 : snorm ((Set.indicator s fun _y => c) - Set.indicator t fun _y => c) p μ ≤ δ
f : α → E
f_cont : Continuous f
I2 : snorm (fun x => f x - Set.indicator s (fun _y => c) x) p μ ≤ δ
f_bound : ∀ (x : α), ‖f x‖ ≤ ‖c‖
f_mem : Memℒp f p
I3 : snorm (f - Set.indicator t fun _y => c) p μ ≤ ε
⊢ Metric.Bounded (range f)
[PROOFSTEP]
exact (BoundedContinuousFunction.ofNormedAddCommGroup f f_cont _ f_bound).bounded_range
[GOAL]
α : 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✝ : Measure.WeaklyRegular μ
p : ℝ
hp : 0 < p
f : α → E
hf : Memℒp f (ENNReal.ofReal p)
ε : ℝ
hε : 0 < ε
⊢ ∃ g, ∫ (x : α), ‖f x - ↑g x‖ ^ p ∂μ ≤ ε ∧ Memℒp (↑g) (ENNReal.ofReal p)
[PROOFSTEP]
have I : 0 < ε ^ (1 / p) := Real.rpow_pos_of_pos hε _
[GOAL]
α : 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✝ : Measure.WeaklyRegular μ
p : ℝ
hp : 0 < p
f : α → E
hf : Memℒp f (ENNReal.ofReal p)
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
⊢ ∃ g, ∫ (x : α), ‖f x - ↑g x‖ ^ p ∂μ ≤ ε ∧ Memℒp (↑g) (ENNReal.ofReal p)
[PROOFSTEP]
have A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0 := by simp only [Ne.def, ENNReal.ofReal_eq_zero, not_le, I]
[GOAL]
α : 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✝ : Measure.WeaklyRegular μ
p : ℝ
hp : 0 < p
f : α → E
hf : Memℒp f (ENNReal.ofReal p)
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
⊢ ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
[PROOFSTEP]
simp only [Ne.def, ENNReal.ofReal_eq_zero, not_le, I]
[GOAL]
α : 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✝ : Measure.WeaklyRegular μ
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, ∫ (x : α), ‖f x - ↑g x‖ ^ p ∂μ ≤ ε ∧ Memℒp (↑g) (ENNReal.ofReal p)
[PROOFSTEP]
have B : ENNReal.ofReal p ≠ 0 := by simpa only [Ne.def, ENNReal.ofReal_eq_zero, not_le] using hp
[GOAL]
α : 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✝ : Measure.WeaklyRegular μ
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
[PROOFSTEP]
simpa only [Ne.def, ENNReal.ofReal_eq_zero, not_le] using hp
[GOAL]
α : 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✝ : Measure.WeaklyRegular μ
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, ∫ (x : α), ‖f x - ↑g x‖ ^ p ∂μ ≤ ε ∧ Memℒp (↑g) (ENNReal.ofReal p)
[PROOFSTEP]
rcases hf.exists_boundedContinuous_snorm_sub_le ENNReal.coe_ne_top A with ⟨g, hg, g_mem⟩
[GOAL]
case 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✝ : Measure.WeaklyRegular μ
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
hg : snorm (f - ↑g) (↑(Real.toNNReal p)) μ ≤ ENNReal.ofReal (ε ^ (1 / p))
g_mem : Memℒp ↑g ↑(Real.toNNReal p)
⊢ ∃ g, ∫ (x : α), ‖f x - ↑g x‖ ^ p ∂μ ≤ ε ∧ Memℒp (↑g) (ENNReal.ofReal p)
[PROOFSTEP]
change snorm _ (ENNReal.ofReal p) _ ≤ _ at hg 
[GOAL]
case 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✝ : Measure.WeaklyRegular μ
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_mem : Memℒp ↑g ↑(Real.toNNReal p)
hg : snorm (f - ↑g) (ENNReal.ofReal p) μ ≤ ENNReal.ofReal (ε ^ (1 / p))
⊢ ∃ g, ∫ (x : α), ‖f x - ↑g x‖ ^ p ∂μ ≤ ε ∧ Memℒp (↑g) (ENNReal.ofReal p)
[PROOFSTEP]
refine' ⟨g, _, g_mem⟩
[GOAL]
case 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✝ : Measure.WeaklyRegular μ
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_mem : Memℒp ↑g ↑(Real.toNNReal p)
hg : snorm (f - ↑g) (ENNReal.ofReal p) μ ≤ ENNReal.ofReal (ε ^ (1 / p))
⊢ ∫ (x : α), ‖f x - ↑g x‖ ^ p ∂μ ≤ ε
[PROOFSTEP]
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 
[GOAL]
α : 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✝ : Measure.WeaklyRegular μ
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_mem : Memℒp ↑g ↑(Real.toNNReal p)
hg : (∫ (a : α), ‖(f - ↑g) a‖ ^ p ∂μ) ^ p⁻¹ ≤ ε ^ p⁻¹
⊢ 0 ≤ ∫ (a : α), ‖(f - ↑g) a‖ ^ p ∂μ
[PROOFSTEP]
exact integral_nonneg fun x => Real.rpow_nonneg_of_nonneg (norm_nonneg _) _
[GOAL]
α : 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✝ : Measure.WeaklyRegular μ
f : α → E
hf : Integrable f
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ g, ∫⁻ (x : α), ↑‖f x - ↑g x‖₊ ∂μ ≤ ε ∧ Integrable ↑g
[PROOFSTEP]
simp only [← memℒp_one_iff_integrable, ← snorm_one_eq_lintegral_nnnorm] at hf ⊢
[GOAL]
α : 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✝ : Measure.WeaklyRegular μ
f : α → E
ε : ℝ≥0∞
hε : ε ≠ 0
hf : Memℒp f 1
⊢ ∃ g, snorm (fun x => f x - ↑g x) 1 μ ≤ ε ∧ Memℒp (↑g) 1
[PROOFSTEP]
exact hf.exists_boundedContinuous_snorm_sub_le ENNReal.one_ne_top hε
[GOAL]
α : 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✝ : Measure.WeaklyRegular μ
f : α → E
hf : Integrable f
ε : ℝ
hε : 0 < ε
⊢ ∃ g, ∫ (x : α), ‖f x - ↑g x‖ ∂μ ≤ ε ∧ Integrable ↑g
[PROOFSTEP]
simp only [← memℒp_one_iff_integrable, ← snorm_one_eq_lintegral_nnnorm, ← ENNReal.ofReal_one] at hf ⊢
[GOAL]
α : 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✝ : Measure.WeaklyRegular μ
f : α → E
ε : ℝ
hε : 0 < ε
hf : Memℒp f (ENNReal.ofReal 1)
⊢ ∃ g, ∫ (x : α), ‖f x - ↑g x‖ ∂μ ≤ ε ∧ Memℒp (↑g) (ENNReal.ofReal 1)
[PROOFSTEP]
simpa using hf.exists_boundedContinuous_integral_rpow_sub_le zero_lt_one hε
[GOAL]
α : 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✝¹ : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
hp : p ≠ ⊤
inst✝ : Measure.WeaklyRegular μ
⊢ AddSubgroup.topologicalClosure (boundedContinuousFunction E p μ) = ⊤
[PROOFSTEP]
rw [AddSubgroup.eq_top_iff']
[GOAL]
α : 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✝¹ : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
hp : p ≠ ⊤
inst✝ : Measure.WeaklyRegular μ
⊢ ∀ (x : { x // x ∈ Lp E p }), x ∈ AddSubgroup.topologicalClosure (boundedContinuousFunction E p μ)
[PROOFSTEP]
intro f
[GOAL]
α : 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✝¹ : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
hp : p ≠ ⊤
inst✝ : Measure.WeaklyRegular μ
f : { x // x ∈ Lp E p }
⊢ f ∈ AddSubgroup.topologicalClosure (boundedContinuousFunction E p μ)
[PROOFSTEP]
refine' mem_closure_iff_frequently.mpr _
[GOAL]
α : 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✝¹ : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
hp : p ≠ ⊤
inst✝ : Measure.WeaklyRegular μ
f : { x // x ∈ Lp E p }
⊢ ∃ᶠ (x : { x // x ∈ Lp E p }) in 𝓝 f, x ∈ ↑(boundedContinuousFunction E p μ)
[PROOFSTEP]
rw [Metric.nhds_basis_closedBall.frequently_iff]
[GOAL]
α : 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✝¹ : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
hp : p ≠ ⊤
inst✝ : Measure.WeaklyRegular μ
f : { x // x ∈ Lp E p }
⊢ ∀ (i : ℝ), 0 < i → ∃ x, x ∈ Metric.closedBall f i ∧ x ∈ ↑(boundedContinuousFunction E p μ)
[PROOFSTEP]
intro ε hε
[GOAL]
α : 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✝¹ : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
hp : p ≠ ⊤
inst✝ : Measure.WeaklyRegular μ
f : { x // x ∈ Lp E p }
ε : ℝ
hε : 0 < ε
⊢ ∃ x, x ∈ Metric.closedBall f ε ∧ x ∈ ↑(boundedContinuousFunction E p μ)
[PROOFSTEP]
have A : ENNReal.ofReal ε ≠ 0 := by simp only [Ne.def, ENNReal.ofReal_eq_zero, not_le, hε]
[GOAL]
α : 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✝¹ : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
hp : p ≠ ⊤
inst✝ : Measure.WeaklyRegular μ
f : { x // x ∈ Lp E p }
ε : ℝ
hε : 0 < ε
⊢ ENNReal.ofReal ε ≠ 0
[PROOFSTEP]
simp only [Ne.def, ENNReal.ofReal_eq_zero, not_le, hε]
[GOAL]
α : 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✝¹ : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
hp : p ≠ ⊤
inst✝ : Measure.WeaklyRegular μ
f : { x // x ∈ Lp E p }
ε : ℝ
hε : 0 < ε
A : ENNReal.ofReal ε ≠ 0
⊢ ∃ x, x ∈ Metric.closedBall f ε ∧ x ∈ ↑(boundedContinuousFunction E p μ)
[PROOFSTEP]
obtain ⟨g, hg, g_mem⟩ : ∃ g : α →ᵇ E, snorm ((f : α → E) - (g : α → E)) p μ ≤ ENNReal.ofReal ε ∧ Memℒp g p μ :=
  (Lp.memℒp f).exists_boundedContinuous_snorm_sub_le hp A
[GOAL]
case 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✝¹ : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
hp : p ≠ ⊤
inst✝ : Measure.WeaklyRegular μ
f : { x // x ∈ Lp E p }
ε : ℝ
hε : 0 < ε
A : ENNReal.ofReal ε ≠ 0
g : α →ᵇ E
hg : snorm (↑↑f - ↑g) p μ ≤ ENNReal.ofReal ε
g_mem : Memℒp (↑g) p
⊢ ∃ x, x ∈ Metric.closedBall f ε ∧ x ∈ ↑(boundedContinuousFunction E p μ)
[PROOFSTEP]
refine' ⟨g_mem.toLp _, _, ⟨g, rfl⟩⟩
[GOAL]
case 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✝¹ : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
hp : p ≠ ⊤
inst✝ : Measure.WeaklyRegular μ
f : { x // x ∈ Lp E p }
ε : ℝ
hε : 0 < ε
A : ENNReal.ofReal ε ≠ 0
g : α →ᵇ E
hg : snorm (↑↑f - ↑g) p μ ≤ ENNReal.ofReal ε
g_mem : Memℒp (↑g) p
⊢ Memℒp.toLp (↑g) g_mem ∈ Metric.closedBall f ε
[PROOFSTEP]
simp only [dist_eq_norm, Metric.mem_closedBall']
[GOAL]
case 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✝¹ : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
hp : p ≠ ⊤
inst✝ : Measure.WeaklyRegular μ
f : { x // x ∈ Lp E p }
ε : ℝ
hε : 0 < ε
A : ENNReal.ofReal ε ≠ 0
g : α →ᵇ E
hg : snorm (↑↑f - ↑g) p μ ≤ ENNReal.ofReal ε
g_mem : Memℒp (↑g) p
⊢ ‖f - Memℒp.toLp (↑g) g_mem‖ ≤ ε
[PROOFSTEP]
rw [Lp.norm_def]
  -- porting note: original proof started with:
    -- convert ENNReal.toReal_le_of_le_ofReal hε.le hg using 2
    -- the `convert` was completely borked and timed out
[GOAL]
case 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✝¹ : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
hp : p ≠ ⊤
inst✝ : Measure.WeaklyRegular μ
f : { x // x ∈ Lp E p }
ε : ℝ
hε : 0 < ε
A : ENNReal.ofReal ε ≠ 0
g : α →ᵇ E
hg : snorm (↑↑f - ↑g) p μ ≤ ENNReal.ofReal ε
g_mem : Memℒp (↑g) p
⊢ ENNReal.toReal (snorm (↑↑(f - Memℒp.toLp (↑g) g_mem)) p μ) ≤ ε
[PROOFSTEP]
have key : snorm ((f : α → E) - (g : α → E)) p μ = snorm (f - Memℒp.toLp (↑g) g_mem) p μ :=
  by
  apply snorm_congr_ae
  filter_upwards [coeFn_sub f (g_mem.toLp g), g_mem.coeFn_toLp] with x hx h'x
  simp only [hx, Pi.sub_apply, sub_right_inj, h'x]
[GOAL]
α : 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✝¹ : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
hp : p ≠ ⊤
inst✝ : Measure.WeaklyRegular μ
f : { x // x ∈ Lp E p }
ε : ℝ
hε : 0 < ε
A : ENNReal.ofReal ε ≠ 0
g : α →ᵇ E
hg : snorm (↑↑f - ↑g) p μ ≤ ENNReal.ofReal ε
g_mem : Memℒp (↑g) p
⊢ snorm (↑↑f - ↑g) p μ = snorm (↑↑(f - Memℒp.toLp (↑g) g_mem)) p μ
[PROOFSTEP]
apply snorm_congr_ae
[GOAL]
case hfg
α : 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✝¹ : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
hp : p ≠ ⊤
inst✝ : Measure.WeaklyRegular μ
f : { x // x ∈ Lp E p }
ε : ℝ
hε : 0 < ε
A : ENNReal.ofReal ε ≠ 0
g : α →ᵇ E
hg : snorm (↑↑f - ↑g) p μ ≤ ENNReal.ofReal ε
g_mem : Memℒp (↑g) p
⊢ ↑↑f - ↑g =ᵐ[μ] ↑↑(f - Memℒp.toLp (↑g) g_mem)
[PROOFSTEP]
filter_upwards [coeFn_sub f (g_mem.toLp g), g_mem.coeFn_toLp] with x hx h'x
[GOAL]
case 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✝¹ : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
hp : p ≠ ⊤
inst✝ : Measure.WeaklyRegular μ
f : { x // x ∈ Lp E p }
ε : ℝ
hε : 0 < ε
A : ENNReal.ofReal ε ≠ 0
g : α →ᵇ E
hg : snorm (↑↑f - ↑g) p μ ≤ ENNReal.ofReal ε
g_mem : Memℒp (↑g) p
x : α
hx : ↑↑(f - Memℒp.toLp (↑g) g_mem) x = (↑↑f - ↑↑(Memℒp.toLp (↑g) g_mem)) x
h'x : ↑↑(Memℒp.toLp (↑g) g_mem) x = ↑g x
⊢ (↑↑f - ↑g) x = ↑↑(f - Memℒp.toLp (↑g) g_mem) x
[PROOFSTEP]
simp only [hx, Pi.sub_apply, sub_right_inj, h'x]
[GOAL]
case 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✝¹ : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
hp : p ≠ ⊤
inst✝ : Measure.WeaklyRegular μ
f : { x // x ∈ Lp E p }
ε : ℝ
hε : 0 < ε
A : ENNReal.ofReal ε ≠ 0
g : α →ᵇ E
hg : snorm (↑↑f - ↑g) p μ ≤ ENNReal.ofReal ε
g_mem : Memℒp (↑g) p
key : snorm (↑↑f - ↑g) p μ = snorm (↑↑(f - Memℒp.toLp (↑g) g_mem)) p μ
⊢ ENNReal.toReal (snorm (↑↑(f - Memℒp.toLp (↑g) g_mem)) p μ) ≤ ε
[PROOFSTEP]
simpa only [key] using ENNReal.toReal_le_of_le_ofReal hε.le hg
[GOAL]
α : Type u_1
inst✝¹⁰ : MeasurableSpace α
inst✝⁹ : TopologicalSpace α
inst✝⁸ : NormalSpace α
inst✝⁷ : BorelSpace α
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝⁵ : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
hp : p ≠ ⊤
𝕜 : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAlgebra ℝ 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : Measure.WeaklyRegular μ
inst✝ : IsFiniteMeasure μ
⊢ DenseRange ↑(toLp p μ 𝕜)
[PROOFSTEP]
haveI : NormedSpace ℝ E := RestrictScalars.normedSpace ℝ 𝕜 E
[GOAL]
α : Type u_1
inst✝¹⁰ : MeasurableSpace α
inst✝⁹ : TopologicalSpace α
inst✝⁸ : NormalSpace α
inst✝⁷ : BorelSpace α
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝⁵ : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
hp : p ≠ ⊤
𝕜 : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAlgebra ℝ 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : Measure.WeaklyRegular μ
inst✝ : IsFiniteMeasure μ
this : NormedSpace ℝ E
⊢ DenseRange ↑(toLp p μ 𝕜)
[PROOFSTEP]
rw [denseRange_iff_closure_range]
[GOAL]
α : Type u_1
inst✝¹⁰ : MeasurableSpace α
inst✝⁹ : TopologicalSpace α
inst✝⁸ : NormalSpace α
inst✝⁷ : BorelSpace α
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝⁵ : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
hp : p ≠ ⊤
𝕜 : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAlgebra ℝ 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : Measure.WeaklyRegular μ
inst✝ : IsFiniteMeasure μ
this : NormedSpace ℝ E
⊢ closure (range ↑(toLp p μ 𝕜)) = univ
[PROOFSTEP]
suffices (LinearMap.range (toLp p μ 𝕜 : _ →L[𝕜] Lp E p μ)).toAddSubgroup.topologicalClosure = ⊤ by
  exact congr_arg ((↑) : AddSubgroup (Lp E p μ) → Set (Lp E p μ)) this
[GOAL]
α : Type u_1
inst✝¹⁰ : MeasurableSpace α
inst✝⁹ : TopologicalSpace α
inst✝⁸ : NormalSpace α
inst✝⁷ : BorelSpace α
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝⁵ : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
hp : p ≠ ⊤
𝕜 : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAlgebra ℝ 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : Measure.WeaklyRegular μ
inst✝ : IsFiniteMeasure μ
this✝ : NormedSpace ℝ E
this : AddSubgroup.topologicalClosure (Submodule.toAddSubgroup (LinearMap.range (toLp p μ 𝕜))) = ⊤
⊢ closure (range ↑(toLp p μ 𝕜)) = univ
[PROOFSTEP]
exact congr_arg ((↑) : AddSubgroup (Lp E p μ) → Set (Lp E p μ)) this
[GOAL]
α : Type u_1
inst✝¹⁰ : MeasurableSpace α
inst✝⁹ : TopologicalSpace α
inst✝⁸ : NormalSpace α
inst✝⁷ : BorelSpace α
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝⁵ : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
hp : p ≠ ⊤
𝕜 : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAlgebra ℝ 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : Measure.WeaklyRegular μ
inst✝ : IsFiniteMeasure μ
this : NormedSpace ℝ E
⊢ AddSubgroup.topologicalClosure (Submodule.toAddSubgroup (LinearMap.range (toLp p μ 𝕜))) = ⊤
[PROOFSTEP]
simpa [range_toLp p μ] using MeasureTheory.Lp.boundedContinuousFunction_dense E hp
[GOAL]
α : Type u_1
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : NormalSpace α
inst✝⁸ : BorelSpace α
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝⁶ : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
hp : p ≠ ⊤
𝕜 : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : NormedAlgebra ℝ 𝕜
inst✝³ : NormedSpace 𝕜 E
inst✝² : CompactSpace α
inst✝¹ : Measure.WeaklyRegular μ
inst✝ : IsFiniteMeasure μ
⊢ DenseRange ↑(toLp p μ 𝕜)
[PROOFSTEP]
refine (BoundedContinuousFunction.toLp_denseRange _ _ hp 𝕜).mono ?_
[GOAL]
α : Type u_1
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : NormalSpace α
inst✝⁸ : BorelSpace α
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝⁶ : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
hp : p ≠ ⊤
𝕜 : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : NormedAlgebra ℝ 𝕜
inst✝³ : NormedSpace 𝕜 E
inst✝² : CompactSpace α
inst✝¹ : Measure.WeaklyRegular μ
inst✝ : IsFiniteMeasure μ
⊢ range ↑(BoundedContinuousFunction.toLp p μ 𝕜) ⊆ range ↑(toLp p μ 𝕜)
[PROOFSTEP]
refine range_subset_iff.2 fun f ↦ ?_
[GOAL]
α : Type u_1
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : NormalSpace α
inst✝⁸ : BorelSpace α
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝⁶ : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
hp : p ≠ ⊤
𝕜 : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : NormedAlgebra ℝ 𝕜
inst✝³ : NormedSpace 𝕜 E
inst✝² : CompactSpace α
inst✝¹ : Measure.WeaklyRegular μ
inst✝ : IsFiniteMeasure μ
f : α →ᵇ E
⊢ ↑(BoundedContinuousFunction.toLp p μ 𝕜) f ∈ range ↑(toLp p μ 𝕜)
[PROOFSTEP]
exact ⟨f.toContinuousMap, rfl⟩
