case inl
α : Type u_1
E : Type u_2
F : Type ?u.670345
G : Type ?u.670348
m m0 : MeasurableSpace α
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
hp : 0 ≠ ⊤
⊢ ∃ η, 0 < η ∧ ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun x => c) 0 μ ≤ ε

case inr
α : Type u_1
E : Type u_2
F : Type ?u.670345
G : Type ?u.670348
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
⊢ ∃ η, 0 < η ∧ ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun x => c) p μ ≤ ε
α : Type u_1
E : Type u_2
F : Type ?u.670345
G : Type ?u.670348
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ η, 0 < η ∧ ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun x => c) p μ ≤ ε
rcases eq_or_ne p 0 with (rfl | h'p)
case inr
α : Type u_1
E : Type u_2
F : Type ?u.670345
G : Type ?u.670348
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
⊢ ∃ η, 0 < η ∧ ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun x => c) p μ ≤ ε
case inr
α : Type u_1
E : Type u_2
F : Type ?u.670345
G : Type ?u.670348
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
⊢ ∃ η, 0 < η ∧ ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun x => c) p μ ≤ ε
have hp₀ : 0 < p := bot_lt_iff_ne_bot.2 h'p
case inr
α : Type u_1
E : Type u_2
F : Type ?u.670345
G : Type ?u.670348
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / ENNReal.toReal p
⊢ ∃ η, 0 < η ∧ ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun x => c) p μ ≤ ε
case inr
α : Type u_1
E : Type u_2
F : Type ?u.670345
G : Type ?u.670348
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
⊢ ∃ η, 0 < η ∧ ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun x => c) p μ ≤ ε
have hp₀' : 0 ≤ 1 / p.toReal := div_nonneg zero_le_one ENNReal.toReal_nonneg
case inr
α : Type u_1
E : Type u_2
F : Type ?u.670345
G : Type ?u.670348
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / ENNReal.toReal p
hp₀'' : 0 < ENNReal.toReal p
⊢ ∃ η, 0 < η ∧ ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun x => c) p μ ≤ ε
case inr
α : Type u_1
E : Type u_2
F : Type ?u.670345
G : Type ?u.670348
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / ENNReal.toReal p
⊢ ∃ η, 0 < η ∧ ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun x => c) p μ ≤ ε
have hp₀'' : 0 < p.toReal := by
  simpa [← ENNReal.toReal_lt_toReal ENNReal.zero_ne_top hp] using hp₀
case inr.intro.intro
α : Type u_1
E : Type u_2
F : Type ?u.670345
G : Type ?u.670348
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / ENNReal.toReal p
hp₀'' : 0 < ENNReal.toReal p
η : ℝ≥0
hη_pos : 0 < η
hη_le : ↑‖c‖₊ * ↑η ^ (1 / ENNReal.toReal p) ≤ ε
⊢ ∃ η, 0 < η ∧ ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun x => c) p μ ≤ ε
case inr
α : Type u_1
E : Type u_2
F : Type ?u.670345
G : Type ?u.670348
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / ENNReal.toReal p
hp₀'' : 0 < ENNReal.toReal p
⊢ ∃ η, 0 < η ∧ ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun x => c) p μ ≤ ε
obtain ⟨η, hη_pos, hη_le⟩ :
    ∃ η : ℝ≥0, 0 < η ∧ (‖c‖₊ : ℝ≥0∞) * (η : ℝ≥0∞) ^ (1 / p.toReal) ≤ ε := by
  have :
    Filter.Tendsto (fun x : ℝ≥0 => ((‖c‖₊ * x ^ (1 / p.toReal) : ℝ≥0) : ℝ≥0∞)) (𝓝 0)
      (𝓝 (0 : ℝ≥0)) := by
    rw [ENNReal.tendsto_coe]
    convert(NNReal.continuousAt_rpow_const (Or.inr hp₀')).tendsto.const_mul _
    simp [hp₀''.ne']
  have hε' : 0 < ε := hε.bot_lt
  obtain ⟨δ, hδ, hδε'⟩ :=
    NNReal.nhds_zero_basis.eventually_iff.mp (eventually_le_of_tendsto_lt hε' this)
  obtain ⟨η, hη, hηδ⟩ := exists_between hδ
  refine' ⟨η, hη, _⟩
  rw [ENNReal.coe_rpow_of_nonneg _ hp₀', ← ENNReal.coe_mul]
  exact hδε' hηδ
case inr.intro.intro
α : Type u_1
E : Type u_2
F : Type ?u.670345
G : Type ?u.670348
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s✝ : Set α
hs✝ : MeasurableSet s✝
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / ENNReal.toReal p
hp₀'' : 0 < ENNReal.toReal p
η : ℝ≥0
hη_pos : 0 < η
hη_le : ↑‖c‖₊ * ↑η ^ (1 / ENNReal.toReal p) ≤ ε
s : Set α
hs : ↑↑μ s ≤ ↑η
⊢ snorm (Set.indicator s fun x => c) p μ ≤ ε
case inr.intro.intro
α : Type u_1
E : Type u_2
F : Type ?u.670345
G : Type ?u.670348
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / ENNReal.toReal p
hp₀'' : 0 < ENNReal.toReal p
η : ℝ≥0
hη_pos : 0 < η
hη_le : ↑‖c‖₊ * ↑η ^ (1 / ENNReal.toReal p) ≤ ε
⊢ ∃ η, 0 < η ∧ ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun x => c) p μ ≤ ε
refine' ⟨η, hη_pos, fun s hs => _⟩
case inr.intro.intro
α : Type u_1
E : Type u_2
F : Type ?u.670345
G : Type ?u.670348
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s✝ : Set α
hs✝ : MeasurableSet s✝
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / ENNReal.toReal p
hp₀'' : 0 < ENNReal.toReal p
η : ℝ≥0
hη_pos : 0 < η
hη_le : ↑‖c‖₊ * ↑η ^ (1 / ENNReal.toReal p) ≤ ε
s : Set α
hs : ↑↑μ s ≤ ↑η
⊢ ↑‖c‖₊ * ↑↑μ s ^ (1 / ENNReal.toReal p) ≤ ↑‖c‖₊ * ↑η ^ (1 / ENNReal.toReal p)
case inr.intro.intro
α : Type u_1
E : Type u_2
F : Type ?u.670345
G : Type ?u.670348
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s✝ : Set α
hs✝ : MeasurableSet s✝
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / ENNReal.toReal p
hp₀'' : 0 < ENNReal.toReal p
η : ℝ≥0
hη_pos : 0 < η
hη_le : ↑‖c‖₊ * ↑η ^ (1 / ENNReal.toReal p) ≤ ε
s : Set α
hs : ↑↑μ s ≤ ↑η
⊢ snorm (Set.indicator s fun x => c) p μ ≤ ε
refine' (snorm_indicator_const_le _ _).trans (le_trans _ hη_le)
no goals
case inr.intro.intro
α : Type u_1
E : Type u_2
F : Type ?u.670345
G : Type ?u.670348
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s✝ : Set α
hs✝ : MeasurableSet s✝
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / ENNReal.toReal p
hp₀'' : 0 < ENNReal.toReal p
η : ℝ≥0
hη_pos : 0 < η
hη_le : ↑‖c‖₊ * ↑η ^ (1 / ENNReal.toReal p) ≤ ε
s : Set α
hs : ↑↑μ s ≤ ↑η
⊢ ↑‖c‖₊ * ↑↑μ s ^ (1 / ENNReal.toReal p) ≤ ↑‖c‖₊ * ↑η ^ (1 / ENNReal.toReal p)
exact mul_le_mul_left' (ENNReal.rpow_le_rpow hs hp₀') _
no goals
case inl
α : Type u_1
E : Type u_2
F : Type ?u.670345
G : Type ?u.670348
m m0 : MeasurableSpace α
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
hp : 0 ≠ ⊤
⊢ ∃ η, 0 < η ∧ ∀ (s : Set α), ↑↑μ s ≤ ↑η → snorm (Set.indicator s fun x => c) 0 μ ≤ ε
exact ⟨1, zero_lt_one, fun s _ => by simp⟩
no goals
α : Type u_1
E : Type u_2
F : Type ?u.670345
G : Type ?u.670348
m m0 : MeasurableSpace α
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s✝ : Set α
hs : MeasurableSet s✝
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
hp : 0 ≠ ⊤
s : Set α
x✝ : ↑↑μ s ≤ ↑1
⊢ snorm (Set.indicator s fun x => c) 0 μ ≤ ε
simp
no goals
α : Type u_1
E : Type u_2
F : Type ?u.670345
G : Type ?u.670348
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / ENNReal.toReal p
⊢ 0 < ENNReal.toReal p
simpa [← ENNReal.toReal_lt_toReal ENNReal.zero_ne_top hp] using hp₀
α : Type u_1
E : Type u_2
F : Type ?u.670345
G : Type ?u.670348
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / ENNReal.toReal p
hp₀'' : 0 < ENNReal.toReal p
this : Tendsto (fun x => ↑(‖c‖₊ * x ^ (1 / ENNReal.toReal p))) (𝓝 0) (𝓝 ↑0)
⊢ ∃ η, 0 < η ∧ ↑‖c‖₊ * ↑η ^ (1 / ENNReal.toReal p) ≤ ε
α : Type u_1
E : Type u_2
F : Type ?u.670345
G : Type ?u.670348
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / ENNReal.toReal p
hp₀'' : 0 < ENNReal.toReal p
⊢ ∃ η, 0 < η ∧ ↑‖c‖₊ * ↑η ^ (1 / ENNReal.toReal p) ≤ ε
have :
  Filter.Tendsto (fun x : ℝ≥0 => ((‖c‖₊ * x ^ (1 / p.toReal) : ℝ≥0) : ℝ≥0∞)) (𝓝 0)
    (𝓝 (0 : ℝ≥0)) := by
  rw [ENNReal.tendsto_coe]
  convert(NNReal.continuousAt_rpow_const (Or.inr hp₀')).tendsto.const_mul _
  simp [hp₀''.ne']
α : Type u_1
E : Type u_2
F : Type ?u.670345
G : Type ?u.670348
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / ENNReal.toReal p
hp₀'' : 0 < ENNReal.toReal p
this : Tendsto (fun x => ↑(‖c‖₊ * x ^ (1 / ENNReal.toReal p))) (𝓝 0) (𝓝 ↑0)
hε' : 0 < ε
⊢ ∃ η, 0 < η ∧ ↑‖c‖₊ * ↑η ^ (1 / ENNReal.toReal p) ≤ ε
α : Type u_1
E : Type u_2
F : Type ?u.670345
G : Type ?u.670348
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / ENNReal.toReal p
hp₀'' : 0 < ENNReal.toReal p
this : Tendsto (fun x => ↑(‖c‖₊ * x ^ (1 / ENNReal.toReal p))) (𝓝 0) (𝓝 ↑0)
⊢ ∃ η, 0 < η ∧ ↑‖c‖₊ * ↑η ^ (1 / ENNReal.toReal p) ≤ ε
have hε' : 0 < ε := hε.bot_lt
case intro.intro
α : Type u_1
E : Type u_2
F : Type ?u.670345
G : Type ?u.670348
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / ENNReal.toReal p
hp₀'' : 0 < ENNReal.toReal p
this : Tendsto (fun x => ↑(‖c‖₊ * x ^ (1 / ENNReal.toReal p))) (𝓝 0) (𝓝 ↑0)
hε' : 0 < ε
δ : ℝ≥0
hδ : 0 < δ
hδε' : ∀ ⦃x : ℝ≥0⦄, x ∈ Set.Iio δ → ↑(‖c‖₊ * x ^ (1 / ENNReal.toReal p)) ≤ ε
⊢ ∃ η, 0 < η ∧ ↑‖c‖₊ * ↑η ^ (1 / ENNReal.toReal p) ≤ ε
α : Type u_1
E : Type u_2
F : Type ?u.670345
G : Type ?u.670348
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / ENNReal.toReal p
hp₀'' : 0 < ENNReal.toReal p
this : Tendsto (fun x => ↑(‖c‖₊ * x ^ (1 / ENNReal.toReal p))) (𝓝 0) (𝓝 ↑0)
hε' : 0 < ε
⊢ ∃ η, 0 < η ∧ ↑‖c‖₊ * ↑η ^ (1 / ENNReal.toReal p) ≤ ε
obtain ⟨δ, hδ, hδε'⟩ :=
  NNReal.nhds_zero_basis.eventually_iff.mp (eventually_le_of_tendsto_lt hε' this)
case intro.intro.intro.intro
α : Type u_1
E : Type u_2
F : Type ?u.670345
G : Type ?u.670348
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / ENNReal.toReal p
hp₀'' : 0 < ENNReal.toReal p
this : Tendsto (fun x => ↑(‖c‖₊ * x ^ (1 / ENNReal.toReal p))) (𝓝 0) (𝓝 ↑0)
hε' : 0 < ε
δ : ℝ≥0
hδ : 0 < δ
hδε' : ∀ ⦃x : ℝ≥0⦄, x ∈ Set.Iio δ → ↑(‖c‖₊ * x ^ (1 / ENNReal.toReal p)) ≤ ε
η : ℝ≥0
hη : 0 < η
hηδ : η < δ
⊢ ∃ η, 0 < η ∧ ↑‖c‖₊ * ↑η ^ (1 / ENNReal.toReal p) ≤ ε
case intro.intro
α : Type u_1
E : Type u_2
F : Type ?u.670345
G : Type ?u.670348
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / ENNReal.toReal p
hp₀'' : 0 < ENNReal.toReal p
this : Tendsto (fun x => ↑(‖c‖₊ * x ^ (1 / ENNReal.toReal p))) (𝓝 0) (𝓝 ↑0)
hε' : 0 < ε
δ : ℝ≥0
hδ : 0 < δ
hδε' : ∀ ⦃x : ℝ≥0⦄, x ∈ Set.Iio δ → ↑(‖c‖₊ * x ^ (1 / ENNReal.toReal p)) ≤ ε
⊢ ∃ η, 0 < η ∧ ↑‖c‖₊ * ↑η ^ (1 / ENNReal.toReal p) ≤ ε
obtain ⟨η, hη, hηδ⟩ := exists_between hδ
case intro.intro.intro.intro
α : Type u_1
E : Type u_2
F : Type ?u.670345
G : Type ?u.670348
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / ENNReal.toReal p
hp₀'' : 0 < ENNReal.toReal p
this : Tendsto (fun x => ↑(‖c‖₊ * x ^ (1 / ENNReal.toReal p))) (𝓝 0) (𝓝 ↑0)
hε' : 0 < ε
δ : ℝ≥0
hδ : 0 < δ
hδε' : ∀ ⦃x : ℝ≥0⦄, x ∈ Set.Iio δ → ↑(‖c‖₊ * x ^ (1 / ENNReal.toReal p)) ≤ ε
η : ℝ≥0
hη : 0 < η
hηδ : η < δ
⊢ ↑‖c‖₊ * ↑η ^ (1 / ENNReal.toReal p) ≤ ε
case intro.intro.intro.intro
α : Type u_1
E : Type u_2
F : Type ?u.670345
G : Type ?u.670348
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / ENNReal.toReal p
hp₀'' : 0 < ENNReal.toReal p
this : Tendsto (fun x => ↑(‖c‖₊ * x ^ (1 / ENNReal.toReal p))) (𝓝 0) (𝓝 ↑0)
hε' : 0 < ε
δ : ℝ≥0
hδ : 0 < δ
hδε' : ∀ ⦃x : ℝ≥0⦄, x ∈ Set.Iio δ → ↑(‖c‖₊ * x ^ (1 / ENNReal.toReal p)) ≤ ε
η : ℝ≥0
hη : 0 < η
hηδ : η < δ
⊢ ∃ η, 0 < η ∧ ↑‖c‖₊ * ↑η ^ (1 / ENNReal.toReal p) ≤ ε
refine' ⟨η, hη, _⟩
case intro.intro.intro.intro
α : Type u_1
E : Type u_2
F : Type ?u.670345
G : Type ?u.670348
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / ENNReal.toReal p
hp₀'' : 0 < ENNReal.toReal p
this : Tendsto (fun x => ↑(‖c‖₊ * x ^ (1 / ENNReal.toReal p))) (𝓝 0) (𝓝 ↑0)
hε' : 0 < ε
δ : ℝ≥0
hδ : 0 < δ
hδε' : ∀ ⦃x : ℝ≥0⦄, x ∈ Set.Iio δ → ↑(‖c‖₊ * x ^ (1 / ENNReal.toReal p)) ≤ ε
η : ℝ≥0
hη : 0 < η
hηδ : η < δ
⊢ ↑(‖c‖₊ * η ^ (1 / ENNReal.toReal p)) ≤ ε
case intro.intro.intro.intro
α : Type u_1
E : Type u_2
F : Type ?u.670345
G : Type ?u.670348
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / ENNReal.toReal p
hp₀'' : 0 < ENNReal.toReal p
this : Tendsto (fun x => ↑(‖c‖₊ * x ^ (1 / ENNReal.toReal p))) (𝓝 0) (𝓝 ↑0)
hε' : 0 < ε
δ : ℝ≥0
hδ : 0 < δ
hδε' : ∀ ⦃x : ℝ≥0⦄, x ∈ Set.Iio δ → ↑(‖c‖₊ * x ^ (1 / ENNReal.toReal p)) ≤ ε
η : ℝ≥0
hη : 0 < η
hηδ : η < δ
⊢ ↑‖c‖₊ * ↑η ^ (1 / ENNReal.toReal p) ≤ ε
rw [ENNReal.coe_rpow_of_nonneg _ hp₀', ← ENNReal.coe_mul]
no goals
case intro.intro.intro.intro
α : Type u_1
E : Type u_2
F : Type ?u.670345
G : Type ?u.670348
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / ENNReal.toReal p
hp₀'' : 0 < ENNReal.toReal p
this : Tendsto (fun x => ↑(‖c‖₊ * x ^ (1 / ENNReal.toReal p))) (𝓝 0) (𝓝 ↑0)
hε' : 0 < ε
δ : ℝ≥0
hδ : 0 < δ
hδε' : ∀ ⦃x : ℝ≥0⦄, x ∈ Set.Iio δ → ↑(‖c‖₊ * x ^ (1 / ENNReal.toReal p)) ≤ ε
η : ℝ≥0
hη : 0 < η
hηδ : η < δ
⊢ ↑(‖c‖₊ * η ^ (1 / ENNReal.toReal p)) ≤ ε
exact hδε' hηδ
α : Type u_1
E : Type u_2
F : Type ?u.670345
G : Type ?u.670348
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / ENNReal.toReal p
hp₀'' : 0 < ENNReal.toReal p
⊢ Tendsto (fun x => ‖c‖₊ * x ^ (1 / ENNReal.toReal p)) (𝓝 0) (𝓝 0)
α : Type u_1
E : Type u_2
F : Type ?u.670345
G : Type ?u.670348
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / ENNReal.toReal p
hp₀'' : 0 < ENNReal.toReal p
⊢ Tendsto (fun x => ↑(‖c‖₊ * x ^ (1 / ENNReal.toReal p))) (𝓝 0) (𝓝 ↑0)
rw [ENNReal.tendsto_coe]
case h.e'_5.h.e'_3
α : Type u_1
E : Type u_2
F : Type ?u.670345
G : Type ?u.670348
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / ENNReal.toReal p
hp₀'' : 0 < ENNReal.toReal p
⊢ 0 = ‖c‖₊ * 0 ^ (1 / ENNReal.toReal p)
α : Type u_1
E : Type u_2
F : Type ?u.670345
G : Type ?u.670348
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / ENNReal.toReal p
hp₀'' : 0 < ENNReal.toReal p
⊢ Tendsto (fun x => ‖c‖₊ * x ^ (1 / ENNReal.toReal p)) (𝓝 0) (𝓝 0)
convert(NNReal.continuousAt_rpow_const (Or.inr hp₀')).tendsto.const_mul _
no goals
case h.e'_5.h.e'_3
α : Type u_1
E : Type u_2
F : Type ?u.670345
G : Type ?u.670348
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
c✝ : E
f : α → E
hf : AEStronglyMeasurable f μ
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / ENNReal.toReal p
hp₀'' : 0 < ENNReal.toReal p
⊢ 0 = ‖c‖₊ * 0 ^ (1 / ENNReal.toReal p)
simp [hp₀''.ne']