α : Type u_2
β : Type u_1
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f g : α → β
hp : 1 ≤ p
hp_ne_top : p ≠ ⊤
hg : Memℒp g p
ε : ℝ
hε : 0 < ε
⊢ ∃ δ x,
    ∀ (i : ι) (s : Set α),
      MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s ((fun x => g) i)) p μ ≤ ENNReal.ofReal ε
α : Type u_2
β : Type u_1
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f g : α → β
hp : 1 ≤ p
hp_ne_top : p ≠ ⊤
hg : Memℒp g p
⊢ UnifIntegrable (fun x => g) p μ
intro ε hε
case intro.intro
α : Type u_2
β : Type u_1
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f g : α → β
hp : 1 ≤ p
hp_ne_top : p ≠ ⊤
hg : Memℒp g p
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ_pos : 0 < δ
hgδ : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s g) p μ ≤ ENNReal.ofReal ε
⊢ ∃ δ x,
    ∀ (i : ι) (s : Set α),
      MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s ((fun x => g) i)) p μ ≤ ENNReal.ofReal ε
α : Type u_2
β : Type u_1
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f g : α → β
hp : 1 ≤ p
hp_ne_top : p ≠ ⊤
hg : Memℒp g p
ε : ℝ
hε : 0 < ε
⊢ ∃ δ x,
    ∀ (i : ι) (s : Set α),
      MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s ((fun x => g) i)) p μ ≤ ENNReal.ofReal ε
obtain ⟨δ, hδ_pos, hgδ⟩ := hg.snorm_indicator_le μ hp hp_ne_top hε
no goals
case intro.intro
α : Type u_2
β : Type u_1
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f g : α → β
hp : 1 ≤ p
hp_ne_top : p ≠ ⊤
hg : Memℒp g p
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ_pos : 0 < δ
hgδ : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s g) p μ ≤ ENNReal.ofReal ε
⊢ ∃ δ x,
    ∀ (i : ι) (s : Set α),
      MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s ((fun x => g) i)) p μ ≤ ENNReal.ofReal ε
exact ⟨δ, hδ_pos, fun _ => hgδ⟩