case intro.intro
α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
⊢ ∃ δ hδ,
    ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s f) p μ ≤ 2 * ENNReal.ofReal ε
α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
⊢ ∃ δ hδ,
    ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s f) p μ ≤ 2 * ENNReal.ofReal ε
obtain ⟨M, hMpos, hM⟩ := hf.snorm_indicator_norm_ge_pos_le μ hmeas hε
case intro.intro.intro.intro
α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (Set.indicator {x | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ δ hδ,
    ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s f) p μ ≤ 2 * ENNReal.ofReal ε
case intro.intro
α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
⊢ ∃ δ hδ,
    ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s f) p μ ≤ 2 * ENNReal.ofReal ε
obtain ⟨δ, hδpos, hδ⟩ :=
  snorm_indicator_le_of_bound μ (f := { x | ‖f x‖ < M }.indicator f) hp_top hε (by
    intro x
    rw [norm_indicator_eq_indicator_norm, Set.indicator_apply]
    split_ifs with h
    exacts [h, hMpos])
α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
x : α
⊢ ‖Set.indicator {x | ‖f x‖ < M} f x‖ < ?m.130677
α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
⊢ ∀ (x : α), ‖Set.indicator {x | ‖f x‖ < M} f x‖ < ?m.130677
intro x
α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
x : α
⊢ (if x ∈ {x | ‖f x‖ < M} then ‖f x‖ else 0) < ?m.130677

α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
⊢ ℝ

α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
⊢ ℝ
α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
x : α
⊢ ‖Set.indicator {x | ‖f x‖ < M} f x‖ < ?m.130677
rw [norm_indicator_eq_indicator_norm, Set.indicator_apply]
case inl
α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
x : α
h : x ∈ {x | ‖f x‖ < M}
⊢ ‖f x‖ < ?m.130677

case inr
α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
x : α
h : ¬x ∈ {x | ‖f x‖ < M}
⊢ 0 < ?m.130677

α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
⊢ ℝ

α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
⊢ ℝ
α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
x : α
⊢ (if x ∈ {x | ‖f x‖ < M} then ‖f x‖ else 0) < ?m.130677

α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
⊢ ℝ

α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
⊢ ℝ
split_ifs with h
no goals
case inl
α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
x : α
h : x ∈ {x | ‖f x‖ < M}
⊢ ‖f x‖ < ?m.130677

case inr
α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
x : α
h : ¬x ∈ {x | ‖f x‖ < M}
⊢ 0 < ?m.130677

α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
⊢ ℝ

α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
⊢ ℝ
exacts [h, hMpos]
case intro.intro.intro.intro
α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (Set.indicator {x | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal δ
⊢ snorm (Set.indicator s f) p μ ≤ 2 * ENNReal.ofReal ε
case intro.intro.intro.intro
α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (Set.indicator {x | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ δ hδ,
    ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s f) p μ ≤ 2 * ENNReal.ofReal ε
refine' ⟨δ, hδpos, fun s hs hμs => _⟩
case intro.intro.intro.intro
α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (Set.indicator {x | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal δ
⊢ snorm (Set.indicator s (Set.indicator {x | M ≤ ↑‖f x‖₊} f + Set.indicator {x | ‖f x‖ < M} f)) p μ ≤
    2 * ENNReal.ofReal ε

α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (Set.indicator {x | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal δ
⊢ f = Set.indicator {x | M ≤ ↑‖f x‖₊} f + Set.indicator {x | ‖f x‖ < M} f
case intro.intro.intro.intro
α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (Set.indicator {x | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal δ
⊢ snorm (Set.indicator s f) p μ ≤ 2 * ENNReal.ofReal ε
rw [(_ : f = { x : α | M ≤ ‖f x‖₊ }.indicator f + { x : α | ‖f x‖ < M }.indicator f)]
case intro.intro.intro.intro
α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (Set.indicator {x | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal δ
⊢ snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f + Set.indicator {x | ‖f x‖ < M} f) p (Measure.restrict μ s) ≤
    2 * ENNReal.ofReal ε
case intro.intro.intro.intro
α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (Set.indicator {x | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal δ
⊢ snorm (Set.indicator s (Set.indicator {x | M ≤ ↑‖f x‖₊} f + Set.indicator {x | ‖f x‖ < M} f)) p μ ≤
    2 * ENNReal.ofReal ε
rw [snorm_indicator_eq_snorm_restrict hs]
case intro.intro.intro.intro.refine'_1
α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (Set.indicator {x | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal δ
⊢ AEStronglyMeasurable (Set.indicator {x | M ≤ ↑‖f x‖₊} f) (Measure.restrict μ s)

case intro.intro.intro.intro.refine'_2
α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (Set.indicator {x | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal δ
⊢ AEStronglyMeasurable (Set.indicator {x | ‖f x‖ < M} f) (Measure.restrict μ s)

case intro.intro.intro.intro.refine'_3
α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (Set.indicator {x | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal δ
⊢ snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p (Measure.restrict μ s) +
      snorm (Set.indicator {x | ‖f x‖ < M} f) p (Measure.restrict μ s) ≤
    2 * ENNReal.ofReal ε
case intro.intro.intro.intro
α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (Set.indicator {x | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal δ
⊢ snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f + Set.indicator {x | ‖f x‖ < M} f) p (Measure.restrict μ s) ≤
    2 * ENNReal.ofReal ε
refine' le_trans (snorm_add_le _ _ hp_one) _
no goals
case intro.intro.intro.intro.refine'_1
α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (Set.indicator {x | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal δ
⊢ AEStronglyMeasurable (Set.indicator {x | M ≤ ↑‖f x‖₊} f) (Measure.restrict μ s)
exact StronglyMeasurable.aestronglyMeasurable
  (hmeas.indicator (measurableSet_le measurable_const hmeas.nnnorm.measurable.subtype_coe))
no goals
case intro.intro.intro.intro.refine'_2
α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (Set.indicator {x | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal δ
⊢ AEStronglyMeasurable (Set.indicator {x | ‖f x‖ < M} f) (Measure.restrict μ s)
exact StronglyMeasurable.aestronglyMeasurable
  (hmeas.indicator (measurableSet_lt hmeas.nnnorm.measurable.subtype_coe measurable_const))
case intro.intro.intro.intro.refine'_3
α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (Set.indicator {x | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal δ
⊢ snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p (Measure.restrict μ s) +
      snorm (Set.indicator {x | ‖f x‖ < M} f) p (Measure.restrict μ s) ≤
    ENNReal.ofReal ε + ENNReal.ofReal ε
case intro.intro.intro.intro.refine'_3
α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (Set.indicator {x | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal δ
⊢ snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p (Measure.restrict μ s) +
      snorm (Set.indicator {x | ‖f x‖ < M} f) p (Measure.restrict μ s) ≤
    2 * ENNReal.ofReal ε
rw [two_mul]
case intro.intro.intro.intro.refine'_3
α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (Set.indicator {x | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal δ
⊢ snorm (Set.indicator {x | ‖f x‖ < M} f) p (Measure.restrict μ s) ≤ ENNReal.ofReal ε
case intro.intro.intro.intro.refine'_3
α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (Set.indicator {x | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal δ
⊢ snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p (Measure.restrict μ s) +
      snorm (Set.indicator {x | ‖f x‖ < M} f) p (Measure.restrict μ s) ≤
    ENNReal.ofReal ε + ENNReal.ofReal ε
refine' add_le_add (le_trans (snorm_mono_measure _ Measure.restrict_le_self) hM) _
case intro.intro.intro.intro.refine'_3
α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (Set.indicator {x | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal δ
⊢ snorm (Set.indicator s (Set.indicator {x | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
case intro.intro.intro.intro.refine'_3
α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (Set.indicator {x | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal δ
⊢ snorm (Set.indicator {x | ‖f x‖ < M} f) p (Measure.restrict μ s) ≤ ENNReal.ofReal ε
rw [← snorm_indicator_eq_snorm_restrict hs]
no goals
case intro.intro.intro.intro.refine'_3
α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (Set.indicator {x | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal δ
⊢ snorm (Set.indicator s (Set.indicator {x | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
exact hδ s hs hμs
case h
α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (Set.indicator {x | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal δ
x : α
⊢ f x = (Set.indicator {x | M ≤ ↑‖f x‖₊} f + Set.indicator {x | ‖f x‖ < M} f) x
α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (Set.indicator {x | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal δ
⊢ f = Set.indicator {x | M ≤ ↑‖f x‖₊} f + Set.indicator {x | ‖f x‖ < M} f
ext x
case pos
α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (Set.indicator {x | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal δ
x : α
hx : M ≤ ‖f x‖
⊢ f x = (Set.indicator {x | M ≤ ↑‖f x‖₊} f + Set.indicator {x | ‖f x‖ < M} f) x

case neg
α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (Set.indicator {x | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal δ
x : α
hx : ¬M ≤ ‖f x‖
⊢ f x = (Set.indicator {x | M ≤ ↑‖f x‖₊} f + Set.indicator {x | ‖f x‖ < M} f) x
case h
α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (Set.indicator {x | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal δ
x : α
⊢ f x = (Set.indicator {x | M ≤ ↑‖f x‖₊} f + Set.indicator {x | ‖f x‖ < M} f) x
by_cases hx : M ≤ ‖f x‖
no goals
case pos
α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (Set.indicator {x | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal δ
x : α
hx : M ≤ ‖f x‖
⊢ f x = (Set.indicator {x | M ≤ ↑‖f x‖₊} f + Set.indicator {x | ‖f x‖ < M} f) x
rw [Pi.add_apply, Set.indicator_of_mem, Set.indicator_of_not_mem, add_zero] <;> simpa
no goals
case neg
α : Type u_2
β : Type u_1
ι : Type ?u.128216
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (Set.indicator {x | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal δ
x : α
hx : ¬M ≤ ‖f x‖
⊢ f x = (Set.indicator {x | M ≤ ↑‖f x‖₊} f + Set.indicator {x | ‖f x‖ < M} f) x
rw [Pi.add_apply, Set.indicator_of_not_mem, Set.indicator_of_mem, zero_add] <;>
  simpa using hx