case pos
α : Type u_2
β : Type u_1
ι : Type ?u.121470
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : M ≤ 0
⊢ ∃ δ hδ, ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s f) p μ ≤ ENNReal.ofReal ε

case neg
α : Type u_2
β : Type u_1
ι : Type ?u.121470
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : ¬M ≤ 0
⊢ ∃ δ hδ, ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s f) p μ ≤ ENNReal.ofReal ε
α : Type u_2
β : Type u_1
ι : Type ?u.121470
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
⊢ ∃ δ hδ, ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s f) p μ ≤ ENNReal.ofReal ε
by_cases hM : M ≤ 0
case neg
α : Type u_2
β : Type u_1
ι : Type ?u.121470
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
⊢ ∃ δ hδ, ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s f) p μ ≤ ENNReal.ofReal ε
case neg
α : Type u_2
β : Type u_1
ι : Type ?u.121470
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : ¬M ≤ 0
⊢ ∃ δ hδ, ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s f) p μ ≤ ENNReal.ofReal ε
rw [not_le] at hM
case neg
α : Type u_2
β : Type u_1
ι : Type ?u.121470
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : ↑↑μ s ≤ ENNReal.ofReal ((ε / M) ^ ENNReal.toReal p)
⊢ snorm (Set.indicator s f) p μ ≤ ENNReal.ofReal ε
case neg
α : Type u_2
β : Type u_1
ι : Type ?u.121470
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
⊢ ∃ δ hδ, ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s f) p μ ≤ ENNReal.ofReal ε
refine' ⟨(ε / M) ^ p.toReal, Real.rpow_pos_of_pos (div_pos hε hM) _, fun s hs hμ => _⟩
case pos
α : Type u_2
β : Type u_1
ι : Type ?u.121470
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : ↑↑μ s ≤ ENNReal.ofReal ((ε / M) ^ ENNReal.toReal p)
hp : p = 0
⊢ snorm (Set.indicator s f) p μ ≤ ENNReal.ofReal ε

case neg
α : Type u_2
β : Type u_1
ι : Type ?u.121470
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : ↑↑μ s ≤ ENNReal.ofReal ((ε / M) ^ ENNReal.toReal p)
hp : ¬p = 0
⊢ snorm (Set.indicator s f) p μ ≤ ENNReal.ofReal ε
case neg
α : Type u_2
β : Type u_1
ι : Type ?u.121470
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : ↑↑μ s ≤ ENNReal.ofReal ((ε / M) ^ ENNReal.toReal p)
⊢ snorm (Set.indicator s f) p μ ≤ ENNReal.ofReal ε
by_cases hp : p = 0
case neg
α : Type u_2
β : Type u_1
ι : Type ?u.121470
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : ↑↑μ s ≤ ENNReal.ofReal ((ε / M) ^ ENNReal.toReal p)
hp : ¬p = 0
⊢ snorm f p (Measure.restrict μ s) ≤ ENNReal.ofReal ε
case neg
α : Type u_2
β : Type u_1
ι : Type ?u.121470
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : ↑↑μ s ≤ ENNReal.ofReal ((ε / M) ^ ENNReal.toReal p)
hp : ¬p = 0
⊢ snorm (Set.indicator s f) p μ ≤ ENNReal.ofReal ε
rw [snorm_indicator_eq_snorm_restrict hs]
case neg
α : Type u_2
β : Type u_1
ι : Type ?u.121470
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : ↑↑μ s ≤ ENNReal.ofReal ((ε / M) ^ ENNReal.toReal p)
hp : ¬p = 0
haebdd : ∀ᵐ (x : α) ∂Measure.restrict μ s, ‖f x‖ ≤ M
⊢ snorm f p (Measure.restrict μ s) ≤ ENNReal.ofReal ε
case neg
α : Type u_2
β : Type u_1
ι : Type ?u.121470
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : ↑↑μ s ≤ ENNReal.ofReal ((ε / M) ^ ENNReal.toReal p)
hp : ¬p = 0
⊢ snorm f p (Measure.restrict μ s) ≤ ENNReal.ofReal ε
have haebdd : ∀ᵐ x ∂μ.restrict s, ‖f x‖ ≤ M := by
  filter_upwards
  exact fun x => (hf x).le
case neg
α : Type u_2
β : Type u_1
ι : Type ?u.121470
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : ↑↑μ s ≤ ENNReal.ofReal ((ε / M) ^ ENNReal.toReal p)
hp : ¬p = 0
haebdd : ∀ᵐ (x : α) ∂Measure.restrict μ s, ‖f x‖ ≤ M
⊢ ↑↑(Measure.restrict μ s) Set.univ ^ (ENNReal.toReal p)⁻¹ * ENNReal.ofReal M ≤ ENNReal.ofReal ε
case neg
α : Type u_2
β : Type u_1
ι : Type ?u.121470
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : ↑↑μ s ≤ ENNReal.ofReal ((ε / M) ^ ENNReal.toReal p)
hp : ¬p = 0
haebdd : ∀ᵐ (x : α) ∂Measure.restrict μ s, ‖f x‖ ≤ M
⊢ snorm f p (Measure.restrict μ s) ≤ ENNReal.ofReal ε
refine' le_trans (snorm_le_of_ae_bound haebdd) _
case neg
α : Type u_2
β : Type u_1
ι : Type ?u.121470
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : ↑↑μ s ≤ ENNReal.ofReal ((ε / M) ^ ENNReal.toReal p)
hp : ¬p = 0
haebdd : ∀ᵐ (x : α) ∂Measure.restrict μ s, ‖f x‖ ≤ M
⊢ ↑↑μ s ^ (ENNReal.toReal p)⁻¹ ≤ ENNReal.ofReal ε / ENNReal.ofReal M

α : Type u_2
β : Type u_1
ι : Type ?u.121470
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : ↑↑μ s ≤ ENNReal.ofReal ((ε / M) ^ ENNReal.toReal p)
hp : ¬p = 0
haebdd : ∀ᵐ (x : α) ∂Measure.restrict μ s, ‖f x‖ ≤ M
⊢ ENNReal.ofReal M ≠ 0
case neg
α : Type u_2
β : Type u_1
ι : Type ?u.121470
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : ↑↑μ s ≤ ENNReal.ofReal ((ε / M) ^ ENNReal.toReal p)
hp : ¬p = 0
haebdd : ∀ᵐ (x : α) ∂Measure.restrict μ s, ‖f x‖ ≤ M
⊢ ↑↑(Measure.restrict μ s) Set.univ ^ (ENNReal.toReal p)⁻¹ * ENNReal.ofReal M ≤ ENNReal.ofReal ε
rw [Measure.restrict_apply MeasurableSet.univ, Set.univ_inter,
  ← ENNReal.le_div_iff_mul_le (Or.inl _) (Or.inl ENNReal.ofReal_ne_top)]
case pos
α : Type u_2
β : Type u_1
ι : Type ?u.121470
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : M ≤ 0
s : Set α
x✝¹ : MeasurableSet s
x✝ : ↑↑μ s ≤ ENNReal.ofReal 1
⊢ snorm (Set.indicator s f) p μ ≤ ENNReal.ofReal ε
case pos
α : Type u_2
β : Type u_1
ι : Type ?u.121470
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : M ≤ 0
⊢ ∃ δ hδ, ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s f) p μ ≤ ENNReal.ofReal ε
refine' ⟨1, zero_lt_one, fun s _ _ => _⟩
case pos
α : Type u_2
β : Type u_1
ι : Type ?u.121470
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : M ≤ 0
s : Set α
x✝¹ : MeasurableSet s
x✝ : ↑↑μ s ≤ ENNReal.ofReal 1
⊢ snorm (Set.indicator s 0) p μ ≤ ENNReal.ofReal ε

α : Type u_2
β : Type u_1
ι : Type ?u.121470
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : M ≤ 0
s : Set α
x✝¹ : MeasurableSet s
x✝ : ↑↑μ s ≤ ENNReal.ofReal 1
⊢ f = 0
case pos
α : Type u_2
β : Type u_1
ι : Type ?u.121470
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : M ≤ 0
s : Set α
x✝¹ : MeasurableSet s
x✝ : ↑↑μ s ≤ ENNReal.ofReal 1
⊢ snorm (Set.indicator s f) p μ ≤ ENNReal.ofReal ε
rw [(_ : f = 0)]
no goals
case pos
α : Type u_2
β : Type u_1
ι : Type ?u.121470
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : M ≤ 0
s : Set α
x✝¹ : MeasurableSet s
x✝ : ↑↑μ s ≤ ENNReal.ofReal 1
⊢ snorm (Set.indicator s 0) p μ ≤ ENNReal.ofReal ε
simp [hε.le]
case h
α : Type u_2
β : Type u_1
ι : Type ?u.121470
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : M ≤ 0
s : Set α
x✝¹ : MeasurableSet s
x✝ : ↑↑μ s ≤ ENNReal.ofReal 1
x : α
⊢ f x = OfNat.ofNat 0 x
α : Type u_2
β : Type u_1
ι : Type ?u.121470
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : M ≤ 0
s : Set α
x✝¹ : MeasurableSet s
x✝ : ↑↑μ s ≤ ENNReal.ofReal 1
⊢ f = 0
ext x
case h
α : Type u_2
β : Type u_1
ι : Type ?u.121470
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : M ≤ 0
s : Set α
x✝¹ : MeasurableSet s
x✝ : ↑↑μ s ≤ ENNReal.ofReal 1
x : α
⊢ ‖f x‖ ≤ 0
case h
α : Type u_2
β : Type u_1
ι : Type ?u.121470
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : M ≤ 0
s : Set α
x✝¹ : MeasurableSet s
x✝ : ↑↑μ s ≤ ENNReal.ofReal 1
x : α
⊢ f x = OfNat.ofNat 0 x
rw [Pi.zero_apply, ← norm_le_zero_iff]
no goals
case h
α : Type u_2
β : Type u_1
ι : Type ?u.121470
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : M ≤ 0
s : Set α
x✝¹ : MeasurableSet s
x✝ : ↑↑μ s ≤ ENNReal.ofReal 1
x : α
⊢ ‖f x‖ ≤ 0
exact (lt_of_lt_of_le (hf x) hM).le
no goals
case pos
α : Type u_2
β : Type u_1
ι : Type ?u.121470
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : ↑↑μ s ≤ ENNReal.ofReal ((ε / M) ^ ENNReal.toReal p)
hp : p = 0
⊢ snorm (Set.indicator s f) p μ ≤ ENNReal.ofReal ε
simp [hp]
case h
α : Type u_2
β : Type u_1
ι : Type ?u.121470
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : ↑↑μ s ≤ ENNReal.ofReal ((ε / M) ^ ENNReal.toReal p)
hp : ¬p = 0
⊢ ∀ (a : α), ‖f a‖ ≤ M
α : Type u_2
β : Type u_1
ι : Type ?u.121470
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : ↑↑μ s ≤ ENNReal.ofReal ((ε / M) ^ ENNReal.toReal p)
hp : ¬p = 0
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ s, ‖f x‖ ≤ M
filter_upwards
no goals
case h
α : Type u_2
β : Type u_1
ι : Type ?u.121470
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : ↑↑μ s ≤ ENNReal.ofReal ((ε / M) ^ ENNReal.toReal p)
hp : ¬p = 0
⊢ ∀ (a : α), ‖f a‖ ≤ M
exact fun x => (hf x).le
case neg
α : Type u_2
β : Type u_1
ι : Type ?u.121470
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : ↑↑μ s ≤ ENNReal.ofReal ((ε / M) ^ ENNReal.toReal p)
hp : ¬p = 0
haebdd : ∀ᵐ (x : α) ∂Measure.restrict μ s, ‖f x‖ ≤ M
⊢ ↑↑μ s ≤ (ENNReal.ofReal ε / ENNReal.ofReal M) ^ ENNReal.toReal p
case neg
α : Type u_2
β : Type u_1
ι : Type ?u.121470
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : ↑↑μ s ≤ ENNReal.ofReal ((ε / M) ^ ENNReal.toReal p)
hp : ¬p = 0
haebdd : ∀ᵐ (x : α) ∂Measure.restrict μ s, ‖f x‖ ≤ M
⊢ ↑↑μ s ^ (ENNReal.toReal p)⁻¹ ≤ ENNReal.ofReal ε / ENNReal.ofReal M
rw [← one_div, ENNReal.rpow_one_div_le_iff (ENNReal.toReal_pos hp hp_top)]
case neg
α : Type u_2
β : Type u_1
ι : Type ?u.121470
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : ↑↑μ s ≤ ENNReal.ofReal ((ε / M) ^ ENNReal.toReal p)
hp : ¬p = 0
haebdd : ∀ᵐ (x : α) ∂Measure.restrict μ s, ‖f x‖ ≤ M
⊢ ENNReal.ofReal ((ε / M) ^ ENNReal.toReal p) ≤ (ENNReal.ofReal ε / ENNReal.ofReal M) ^ ENNReal.toReal p
case neg
α : Type u_2
β : Type u_1
ι : Type ?u.121470
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : ↑↑μ s ≤ ENNReal.ofReal ((ε / M) ^ ENNReal.toReal p)
hp : ¬p = 0
haebdd : ∀ᵐ (x : α) ∂Measure.restrict μ s, ‖f x‖ ≤ M
⊢ ↑↑μ s ≤ (ENNReal.ofReal ε / ENNReal.ofReal M) ^ ENNReal.toReal p
refine' le_trans hμ _
no goals
case neg
α : Type u_2
β : Type u_1
ι : Type ?u.121470
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : ↑↑μ s ≤ ENNReal.ofReal ((ε / M) ^ ENNReal.toReal p)
hp : ¬p = 0
haebdd : ∀ᵐ (x : α) ∂Measure.restrict μ s, ‖f x‖ ≤ M
⊢ ENNReal.ofReal ((ε / M) ^ ENNReal.toReal p) ≤ (ENNReal.ofReal ε / ENNReal.ofReal M) ^ ENNReal.toReal p
rw [← ENNReal.ofReal_rpow_of_pos (div_pos hε hM),
  ENNReal.rpow_le_rpow_iff (ENNReal.toReal_pos hp hp_top), ENNReal.ofReal_div_of_pos hM]
no goals
α : Type u_2
β : Type u_1
ι : Type ?u.121470
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ⊤
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : ↑↑μ s ≤ ENNReal.ofReal ((ε / M) ^ ENNReal.toReal p)
hp : ¬p = 0
haebdd : ∀ᵐ (x : α) ∂Measure.restrict μ s, ‖f x‖ ≤ M
⊢ ENNReal.ofReal M ≠ 0
simpa only [ENNReal.ofReal_eq_zero, not_le, Ne.def]