case pos
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : p = 0
⊢ ∃ M, snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε

case neg
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
⊢ ∃ M, snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
⊢ ∃ M, snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
by_cases hp_ne_zero : p = 0
case pos
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : p = ⊤
⊢ ∃ M, snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε

case neg
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
⊢ ∃ M, snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
case neg
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
⊢ ∃ M, snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
by_cases hp_ne_top : p = ∞
case neg.intro.intro
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x‖₊ ∂μ) ≤
    ENNReal.ofReal (ε ^ ENNReal.toReal p)
⊢ ∃ M, snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
case neg
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
⊢ ∃ M, snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
obtain ⟨M, hM', hM⟩ := Memℒp.integral_indicator_norm_ge_nonneg_le
  (μ := μ) (hf.norm_rpow hp_ne_zero hp_ne_top) (Real.rpow_pos_of_pos hε p.toReal)
case neg.intro.intro
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x‖₊ ∂μ) ≤
    ENNReal.ofReal (ε ^ ENNReal.toReal p)
⊢ snorm (Set.indicator {x | M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
case neg.intro.intro
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x‖₊ ∂μ) ≤
    ENNReal.ofReal (ε ^ ENNReal.toReal p)
⊢ ∃ M, snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
refine' ⟨M ^ (1 / p.toReal), _⟩
case neg.intro.intro
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x‖₊ ∂μ) ≤
    ENNReal.ofReal (ε ^ ENNReal.toReal p)
⊢ (∫⁻ (x : α), ↑‖Set.indicator {x | M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊} f x‖₊ ^ ENNReal.toReal p ∂μ) ^
      (1 / ENNReal.toReal p) ≤
    ENNReal.ofReal ε ^ 1
case neg.intro.intro
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x‖₊ ∂μ) ≤
    ENNReal.ofReal (ε ^ ENNReal.toReal p)
⊢ snorm (Set.indicator {x | M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
rw [snorm_eq_lintegral_rpow_nnnorm hp_ne_zero hp_ne_top, ← ENNReal.rpow_one (ENNReal.ofReal ε)]
case neg.intro.intro
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x‖₊ ∂μ) ≤
    ENNReal.ofReal (ε ^ ENNReal.toReal p)
⊢ (∫⁻ (x : α), ↑‖Set.indicator {x | M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊} f x‖₊ ^ ENNReal.toReal p ∂μ) ^
      (1 / ENNReal.toReal p) ≤
    ENNReal.ofReal ε ^ (ENNReal.toReal p * (1 / ENNReal.toReal p))
case neg.intro.intro
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x‖₊ ∂μ) ≤
    ENNReal.ofReal (ε ^ ENNReal.toReal p)
⊢ (∫⁻ (x : α), ↑‖Set.indicator {x | M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊} f x‖₊ ^ ENNReal.toReal p ∂μ) ^
      (1 / ENNReal.toReal p) ≤
    ENNReal.ofReal ε ^ 1
conv_rhs => rw [← mul_one_div_cancel (ENNReal.toReal_pos hp_ne_zero hp_ne_top).ne.symm]
case neg.intro.intro
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x‖₊ ∂μ) ≤
    ENNReal.ofReal (ε ^ ENNReal.toReal p)
⊢ (∫⁻ (x : α), ↑‖Set.indicator {x | M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊} f x‖₊ ^ ENNReal.toReal p ∂μ) ≤
    ENNReal.ofReal (ε ^ ENNReal.toReal p)
case neg.intro.intro
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x‖₊ ∂μ) ≤
    ENNReal.ofReal (ε ^ ENNReal.toReal p)
⊢ (∫⁻ (x : α), ↑‖Set.indicator {x | M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊} f x‖₊ ^ ENNReal.toReal p ∂μ) ^
      (1 / ENNReal.toReal p) ≤
    ENNReal.ofReal ε ^ (ENNReal.toReal p * (1 / ENNReal.toReal p))
rw [ENNReal.rpow_mul,
  ENNReal.rpow_le_rpow_iff (one_div_pos.2 <| ENNReal.toReal_pos hp_ne_zero hp_ne_top),
  ENNReal.ofReal_rpow_of_pos hε]
case h.e'_3.h.e'_4.h
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x‖₊ ∂μ) ≤
    ENNReal.ofReal (ε ^ ENNReal.toReal p)
x✝ : α
⊢ ↑‖Set.indicator {x | M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊} f x✝‖₊ ^ ENNReal.toReal p =
    ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x✝‖₊
case neg.intro.intro
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x‖₊ ∂μ) ≤
    ENNReal.ofReal (ε ^ ENNReal.toReal p)
⊢ (∫⁻ (x : α), ↑‖Set.indicator {x | M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊} f x‖₊ ^ ENNReal.toReal p ∂μ) ≤
    ENNReal.ofReal (ε ^ ENNReal.toReal p)
convert hM
case h.e'_3.h.e'_4.h
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x‖₊ ∂μ) ≤
    ENNReal.ofReal (ε ^ ENNReal.toReal p)
x : α
⊢ ↑‖Set.indicator {x | M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊} f x‖₊ ^ ENNReal.toReal p =
    ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x‖₊
case h.e'_3.h.e'_4.h
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x‖₊ ∂μ) ≤
    ENNReal.ofReal (ε ^ ENNReal.toReal p)
x✝ : α
⊢ ↑‖Set.indicator {x | M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊} f x✝‖₊ ^ ENNReal.toReal p =
    ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x✝‖₊
rename_i x
case h.e'_3.h.e'_4.h
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x‖₊ ∂μ) ≤
    ENNReal.ofReal (ε ^ ENNReal.toReal p)
x : α
⊢ ↑(Set.indicator {x | M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊} (fun a => ‖f a‖₊) x ^ ENNReal.toReal p) =
    ↑(Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun a => ‖‖f a‖ ^ ENNReal.toReal p‖₊) x)
case h.e'_3.h.e'_4.h
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x‖₊ ∂μ) ≤
    ENNReal.ofReal (ε ^ ENNReal.toReal p)
x : α
⊢ ↑‖Set.indicator {x | M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊} f x‖₊ ^ ENNReal.toReal p =
    ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x‖₊
rw [ENNReal.coe_rpow_of_nonneg _ ENNReal.toReal_nonneg, nnnorm_indicator_eq_indicator_nnnorm,
  nnnorm_indicator_eq_indicator_nnnorm]
case h.e'_3.h.e'_4.h
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x‖₊ ∂μ) ≤
    ENNReal.ofReal (ε ^ ENNReal.toReal p)
x : α
hiff : M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊ ↔ M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊
⊢ ↑(Set.indicator {x | M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊} (fun a => ‖f a‖₊) x ^ ENNReal.toReal p) =
    ↑(Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun a => ‖‖f a‖ ^ ENNReal.toReal p‖₊) x)
case h.e'_3.h.e'_4.h
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x‖₊ ∂μ) ≤
    ENNReal.ofReal (ε ^ ENNReal.toReal p)
x : α
⊢ ↑(Set.indicator {x | M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊} (fun a => ‖f a‖₊) x ^ ENNReal.toReal p) =
    ↑(Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun a => ‖‖f a‖ ^ ENNReal.toReal p‖₊) x)
have hiff : M ^ (1 / p.toReal) ≤ ‖f x‖₊ ↔ M ≤ ‖‖f x‖ ^ p.toReal‖₊ := by
  rw [coe_nnnorm, coe_nnnorm, Real.norm_rpow_of_nonneg (norm_nonneg _), norm_norm,
    ← Real.rpow_le_rpow_iff hM' (Real.rpow_nonneg_of_nonneg (norm_nonneg _) _)
      (one_div_pos.2 <| ENNReal.toReal_pos hp_ne_zero hp_ne_top), ← Real.rpow_mul (norm_nonneg _),
    mul_one_div_cancel (ENNReal.toReal_pos hp_ne_zero hp_ne_top).ne.symm, Real.rpow_one]
case pos
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x‖₊ ∂μ) ≤
    ENNReal.ofReal (ε ^ ENNReal.toReal p)
x : α
hiff : M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊ ↔ M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊
hx : x ∈ {x | M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊}
⊢ ↑(Set.indicator {x | M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊} (fun a => ‖f a‖₊) x ^ ENNReal.toReal p) =
    ↑(Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun a => ‖‖f a‖ ^ ENNReal.toReal p‖₊) x)

case neg
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x‖₊ ∂μ) ≤
    ENNReal.ofReal (ε ^ ENNReal.toReal p)
x : α
hiff : M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊ ↔ M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊
hx : ¬x ∈ {x | M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊}
⊢ ↑(Set.indicator {x | M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊} (fun a => ‖f a‖₊) x ^ ENNReal.toReal p) =
    ↑(Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun a => ‖‖f a‖ ^ ENNReal.toReal p‖₊) x)
case h.e'_3.h.e'_4.h
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x‖₊ ∂μ) ≤
    ENNReal.ofReal (ε ^ ENNReal.toReal p)
x : α
hiff : M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊ ↔ M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊
⊢ ↑(Set.indicator {x | M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊} (fun a => ‖f a‖₊) x ^ ENNReal.toReal p) =
    ↑(Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun a => ‖‖f a‖ ^ ENNReal.toReal p‖₊) x)
by_cases hx : x ∈ { x : α | M ^ (1 / p.toReal) ≤ ‖f x‖₊ }
case pos
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : p = 0
⊢ snorm (Set.indicator {x | 1 ≤ ↑‖f x‖₊} f) 0 μ ≤ ENNReal.ofReal ε
case pos
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : p = 0
⊢ ∃ M, snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
refine' ⟨1, hp_ne_zero.symm ▸ _⟩
no goals
case pos
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : p = 0
⊢ snorm (Set.indicator {x | 1 ≤ ↑‖f x‖₊} f) 0 μ ≤ ENNReal.ofReal ε
simp [snorm_exponent_zero]
case pos
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hf : Memℒp f ⊤
hp_ne_zero : ¬⊤ = 0
⊢ ∃ M, snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) ⊤ μ ≤ ENNReal.ofReal ε
case pos
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : p = ⊤
⊢ ∃ M, snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) p μ ≤ ENNReal.ofReal ε
subst hp_ne_top
case pos.intro
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hf : Memℒp f ⊤
hp_ne_zero : ¬⊤ = 0
M : ℝ
hM : snormEssSup (Set.indicator {x | M ≤ ↑‖f x‖₊} f) μ = 0
⊢ ∃ M, snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) ⊤ μ ≤ ENNReal.ofReal ε
case pos
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hf : Memℒp f ⊤
hp_ne_zero : ¬⊤ = 0
⊢ ∃ M, snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) ⊤ μ ≤ ENNReal.ofReal ε
obtain ⟨M, hM⟩ := hf.snormEssSup_indicator_norm_ge_eq_zero μ hmeas
case pos.intro
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hf : Memℒp f ⊤
hp_ne_zero : ¬⊤ = 0
M : ℝ
hM : snormEssSup (Set.indicator {x | M ≤ ↑‖f x‖₊} f) μ = 0
⊢ snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) ⊤ μ ≤ ENNReal.ofReal ε
case pos.intro
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hf : Memℒp f ⊤
hp_ne_zero : ¬⊤ = 0
M : ℝ
hM : snormEssSup (Set.indicator {x | M ≤ ↑‖f x‖₊} f) μ = 0
⊢ ∃ M, snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) ⊤ μ ≤ ENNReal.ofReal ε
refine' ⟨M, _⟩
no goals
case pos.intro
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hf : Memℒp f ⊤
hp_ne_zero : ¬⊤ = 0
M : ℝ
hM : snormEssSup (Set.indicator {x | M ≤ ↑‖f x‖₊} f) μ = 0
⊢ snorm (Set.indicator {x | M ≤ ↑‖f x‖₊} f) ⊤ μ ≤ ENNReal.ofReal ε
simp only [snorm_exponent_top, hM, zero_le]
no goals
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x‖₊ ∂μ) ≤
    ENNReal.ofReal (ε ^ ENNReal.toReal p)
x : α
⊢ M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊ ↔ M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊
rw [coe_nnnorm, coe_nnnorm, Real.norm_rpow_of_nonneg (norm_nonneg _), norm_norm,
  ← Real.rpow_le_rpow_iff hM' (Real.rpow_nonneg_of_nonneg (norm_nonneg _) _)
    (one_div_pos.2 <| ENNReal.toReal_pos hp_ne_zero hp_ne_top), ← Real.rpow_mul (norm_nonneg _),
  mul_one_div_cancel (ENNReal.toReal_pos hp_ne_zero hp_ne_top).ne.symm, Real.rpow_one]
case pos
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x‖₊ ∂μ) ≤
    ENNReal.ofReal (ε ^ ENNReal.toReal p)
x : α
hiff : M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊ ↔ M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊
hx : x ∈ {x | M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊}
⊢ ↑(‖f x‖₊ ^ ENNReal.toReal p) = ↑{ val := ‖f x‖ ^ ENNReal.toReal p, property := ?pos✝ }

case pos
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x‖₊ ∂μ) ≤
    ENNReal.ofReal (ε ^ ENNReal.toReal p)
x : α
hiff : M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊ ↔ M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊
hx : x ∈ {x | M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊}
⊢ 0 ≤ ‖f x‖ ^ ENNReal.toReal p

case pos.h
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x‖₊ ∂μ) ≤
    ENNReal.ofReal (ε ^ ENNReal.toReal p)
x : α
hiff : M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊ ↔ M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊
hx : x ∈ {x | M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊}
⊢ x ∈ {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊}
case pos
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x‖₊ ∂μ) ≤
    ENNReal.ofReal (ε ^ ENNReal.toReal p)
x : α
hiff : M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊ ↔ M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊
hx : x ∈ {x | M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊}
⊢ ↑(Set.indicator {x | M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊} (fun a => ‖f a‖₊) x ^ ENNReal.toReal p) =
    ↑(Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun a => ‖‖f a‖ ^ ENNReal.toReal p‖₊) x)
rw [Set.indicator_of_mem hx, Set.indicator_of_mem, Real.nnnorm_of_nonneg]
case pos.h
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x‖₊ ∂μ) ≤
    ENNReal.ofReal (ε ^ ENNReal.toReal p)
x : α
hiff : M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊ ↔ M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊
hx : x ∈ {x | M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊}
⊢ x ∈ {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊}
case pos
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x‖₊ ∂μ) ≤
    ENNReal.ofReal (ε ^ ENNReal.toReal p)
x : α
hiff : M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊ ↔ M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊
hx : x ∈ {x | M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊}
⊢ ↑(‖f x‖₊ ^ ENNReal.toReal p) = ↑{ val := ‖f x‖ ^ ENNReal.toReal p, property := ?pos✝ }

case pos
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x‖₊ ∂μ) ≤
    ENNReal.ofReal (ε ^ ENNReal.toReal p)
x : α
hiff : M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊ ↔ M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊
hx : x ∈ {x | M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊}
⊢ 0 ≤ ‖f x‖ ^ ENNReal.toReal p

case pos.h
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x‖₊ ∂μ) ≤
    ENNReal.ofReal (ε ^ ENNReal.toReal p)
x : α
hiff : M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊ ↔ M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊
hx : x ∈ {x | M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊}
⊢ x ∈ {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊}
rfl
case pos.h
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x‖₊ ∂μ) ≤
    ENNReal.ofReal (ε ^ ENNReal.toReal p)
x : α
hiff : M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊ ↔ M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊
hx : x ∈ {x | M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊}
⊢ M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊
case pos.h
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x‖₊ ∂μ) ≤
    ENNReal.ofReal (ε ^ ENNReal.toReal p)
x : α
hiff : M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊ ↔ M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊
hx : x ∈ {x | M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊}
⊢ x ∈ {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊}
rw [Set.mem_setOf_eq]
no goals
case pos.h
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x‖₊ ∂μ) ≤
    ENNReal.ofReal (ε ^ ENNReal.toReal p)
x : α
hiff : M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊ ↔ M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊
hx : x ∈ {x | M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊}
⊢ M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊
rwa [← hiff]
case neg
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x‖₊ ∂μ) ≤
    ENNReal.ofReal (ε ^ ENNReal.toReal p)
x : α
hiff : M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊ ↔ M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊
hx : ¬x ∈ {x | M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊}
⊢ ↑(0 ^ ENNReal.toReal p) = ↑0

case neg.h
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x‖₊ ∂μ) ≤
    ENNReal.ofReal (ε ^ ENNReal.toReal p)
x : α
hiff : M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊ ↔ M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊
hx : ¬x ∈ {x | M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊}
⊢ ¬x ∈ {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊}
case neg
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x‖₊ ∂μ) ≤
    ENNReal.ofReal (ε ^ ENNReal.toReal p)
x : α
hiff : M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊ ↔ M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊
hx : ¬x ∈ {x | M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊}
⊢ ↑(Set.indicator {x | M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊} (fun a => ‖f a‖₊) x ^ ENNReal.toReal p) =
    ↑(Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun a => ‖‖f a‖ ^ ENNReal.toReal p‖₊) x)
rw [Set.indicator_of_not_mem hx, Set.indicator_of_not_mem]
no goals
case neg
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x‖₊ ∂μ) ≤
    ENNReal.ofReal (ε ^ ENNReal.toReal p)
x : α
hiff : M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊ ↔ M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊
hx : ¬x ∈ {x | M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊}
⊢ ↑(0 ^ ENNReal.toReal p) = ↑0
simp [(ENNReal.toReal_pos hp_ne_zero hp_ne_top).ne.symm]
case neg.h
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x‖₊ ∂μ) ≤
    ENNReal.ofReal (ε ^ ENNReal.toReal p)
x : α
hiff : M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊ ↔ M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊
hx : ¬x ∈ {x | M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊}
⊢ ¬M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊
case neg.h
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x‖₊ ∂μ) ≤
    ENNReal.ofReal (ε ^ ENNReal.toReal p)
x : α
hiff : M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊ ↔ M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊
hx : ¬x ∈ {x | M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊}
⊢ ¬x ∈ {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊}
rw [Set.mem_setOf_eq]
no goals
case neg.h
α : Type u_2
β : Type u_1
ι : Type ?u.99807
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f p
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ⊤
M : ℝ
hM' : 0 ≤ M
hM :
  (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊} (fun x => ‖f x‖ ^ ENNReal.toReal p) x‖₊ ∂μ) ≤
    ENNReal.ofReal (ε ^ ENNReal.toReal p)
x : α
hiff : M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊ ↔ M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊
hx : ¬x ∈ {x | M ^ (1 / ENNReal.toReal p) ≤ ↑‖f x‖₊}
⊢ ¬M ≤ ↑‖‖f x‖ ^ ENNReal.toReal p‖₊
rwa [← hiff]