α : 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
α : 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
obtain ⟨η, η_pos, hη⟩ :
  ∃ η : ℝ≥0, 0 < η ∧ ∀ s : Set α, μ s ≤ η → snorm (s.indicator 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
α : 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
exact exists_snorm_indicator_le hp c hε
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
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
have ηpos : (0 : ℝ≥0∞) < η := ENNReal.coe_lt_coe.2 η_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, 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
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
obtain ⟨V, sV, V_open, h'V, hV⟩ : ∃ (V : Set α), 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
α : 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
exact s_closed.measurableSet.exists_isOpen_diff_lt hs ηpos.ne'
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
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
let v := u ∩ V
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
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
have hsv : s ⊆ v := subset_inter hsu sV
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
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
have hμv : μ v < ∞ := (measure_mono (inter_subset_right _ _)).trans_lt h'V
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
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
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)
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
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
have g_norm : ∀ x, ‖g x‖ = g x := fun x => by rw [Real.norm_eq_abs, abs_of_nonneg (hg_range x).1]
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
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
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
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
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
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]
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 μ ≤ ε
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
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⟩
no goals
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 μ ≤ ε
exact hη _ ((measure_mono (diff_subset_diff (inter_subset_right _ _) Subset.rfl)).trans hV.le)
no goals
α : Type u_1
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : NormalSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedSpace ℝ E
inst✝ : 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
rw [Real.norm_eq_abs, abs_of_nonneg (hg_range x).1]
α : 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‖
α : 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‖
intro x
α : 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‖
α : 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‖
simp only [norm_smul, g_norm x]
α : 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
α : 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‖
apply mul_le_of_le_one_left (norm_nonneg _)
no goals
α : Type u_1
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : NormalSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedSpace ℝ E
inst✝ : 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
exact (hg_range x).2
α : 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‖
α : 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‖
intro x
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‖

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‖
α : 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‖
by_cases hv : x ∈ v
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‖
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‖
rw [← Set.diff_union_of_subset hsv] at hv
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‖

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‖
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‖
cases' hv with hsv hs
no goals
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‖
simpa only [hsv.2, Set.indicator_of_not_mem, not_false_iff, sub_zero, hsv,
  Set.indicator_of_mem] using gc_bd0 x
no goals
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‖
simp [hgs hs, hs]
no goals
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‖
simp [hgv hv, show x ∉ s from fun h => hv (hsv 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.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
α : 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
refine' Function.support_subset_iff'.2 fun x hx => _
no goals
α : Type u_1
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : NormalSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedSpace ℝ E
inst✝ : 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
simp only [hgv hx, Pi.zero_apply, zero_smul]
α : 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
α : 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
refine' Memℒp.smul_of_top_left (memℒp_top_const _) _
α : 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 μ < ⊤
α : 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
refine' ⟨g.continuous.aestronglyMeasurable, _⟩
α : 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 μ < ⊤
α : 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 μ < ⊤
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]
α : 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‖
α : 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 μ < ⊤
refine' (snorm_mono fun x => _).trans_lt this
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‖

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‖
α : 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‖
by_cases hx : x ∈ v
α : 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) < ⊤
α : 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 μ < ⊤
refine' (snorm_indicator_const_le _ _).trans_lt _
no goals
α : Type u_1
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : NormalSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedSpace ℝ E
inst✝ : 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) < ⊤
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]
no goals
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‖
simp only [hx, abs_of_nonneg (hg_range x).1, (hg_range x).2, Real.norm_eq_abs,
  indicator_of_mem, CstarRing.norm_one]
no goals
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‖
simp only [hgv hx, Pi.zero_apply, Real.norm_eq_abs, abs_zero, abs_nonneg]