α : Type u_2
β : Type u_1
ι : Type ?u.497069
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), Memℒp (f n) p
hf_tendsto : Tendsto (fun n => snorm (f n) p μ) atTop (𝓝 0)
ε : ℝ
hε : 0 < ε
⊢ ∃ δ x,
    ∀ (i : ℕ) (s : Set α),
      MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε
α : Type u_2
β : Type u_1
ι : Type ?u.497069
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), Memℒp (f n) p
hf_tendsto : Tendsto (fun n => snorm (f n) p μ) atTop (𝓝 0)
⊢ UnifIntegrable f p μ
intro ε hε
α : Type u_2
β : Type u_1
ι : Type ?u.497069
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), Memℒp (f n) p
hf_tendsto : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n) p μ ≤ ε
ε : ℝ
hε : 0 < ε
⊢ ∃ δ x,
    ∀ (i : ℕ) (s : Set α),
      MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε
α : Type u_2
β : Type u_1
ι : Type ?u.497069
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), Memℒp (f n) p
hf_tendsto : Tendsto (fun n => snorm (f n) p μ) atTop (𝓝 0)
ε : ℝ
hε : 0 < ε
⊢ ∃ δ x,
    ∀ (i : ℕ) (s : Set α),
      MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε
rw [ENNReal.tendsto_atTop_zero] at hf_tendsto
case intro
α : Type u_2
β : Type u_1
ι : Type ?u.497069
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), Memℒp (f n) p
hf_tendsto : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n) p μ ≤ ε
ε : ℝ
hε : 0 < ε
N : ℕ
hN : ∀ (n : ℕ), n ≥ N → snorm (f n) p μ ≤ ENNReal.ofReal ε
⊢ ∃ δ x,
    ∀ (i : ℕ) (s : Set α),
      MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε
α : Type u_2
β : Type u_1
ι : Type ?u.497069
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), Memℒp (f n) p
hf_tendsto : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n) p μ ≤ ε
ε : ℝ
hε : 0 < ε
⊢ ∃ δ x,
    ∀ (i : ℕ) (s : Set α),
      MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε
obtain ⟨N, hN⟩ := hf_tendsto (ENNReal.ofReal ε) (by simpa)
case intro
α : Type u_2
β : Type u_1
ι : Type ?u.497069
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), Memℒp (f n) p
hf_tendsto : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n) p μ ≤ ε
ε : ℝ
hε : 0 < ε
N : ℕ
hN : ∀ (n : ℕ), n ≥ N → snorm (f n) p μ ≤ ENNReal.ofReal ε
F : Fin N → α → β := fun n => f ↑n
⊢ ∃ δ x,
    ∀ (i : ℕ) (s : Set α),
      MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε
case intro
α : Type u_2
β : Type u_1
ι : Type ?u.497069
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), Memℒp (f n) p
hf_tendsto : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n) p μ ≤ ε
ε : ℝ
hε : 0 < ε
N : ℕ
hN : ∀ (n : ℕ), n ≥ N → snorm (f n) p μ ≤ ENNReal.ofReal ε
⊢ ∃ δ x,
    ∀ (i : ℕ) (s : Set α),
      MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε
let F : Fin N → α → β := fun n => f n
case intro
α : Type u_2
β : Type u_1
ι : Type ?u.497069
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), Memℒp (f n) p
hf_tendsto : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n) p μ ≤ ε
ε : ℝ
hε : 0 < ε
N : ℕ
hN : ∀ (n : ℕ), n ≥ N → snorm (f n) p μ ≤ ENNReal.ofReal ε
F : Fin N → α → β := fun n => f ↑n
hF : ∀ (n : Fin N), Memℒp (F n) p
⊢ ∃ δ x,
    ∀ (i : ℕ) (s : Set α),
      MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε
case intro
α : Type u_2
β : Type u_1
ι : Type ?u.497069
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), Memℒp (f n) p
hf_tendsto : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n) p μ ≤ ε
ε : ℝ
hε : 0 < ε
N : ℕ
hN : ∀ (n : ℕ), n ≥ N → snorm (f n) p μ ≤ ENNReal.ofReal ε
F : Fin N → α → β := fun n => f ↑n
⊢ ∃ δ x,
    ∀ (i : ℕ) (s : Set α),
      MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε
have hF : ∀ n, Memℒp (F n) p μ := fun n => hf n
case intro.intro.intro
α : Type u_2
β : Type u_1
ι : Type ?u.497069
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), Memℒp (f n) p
hf_tendsto : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n) p μ ≤ ε
ε : ℝ
hε : 0 < ε
N : ℕ
hN : ∀ (n : ℕ), n ≥ N → snorm (f n) p μ ≤ ENNReal.ofReal ε
F : Fin N → α → β := fun n => f ↑n
hF : ∀ (n : Fin N), Memℒp (F n) p
δ₁ : ℝ
hδpos₁ : 0 < δ₁
hδ₁ :
  ∀ (i : Fin N) (s : Set α),
    MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₁ → snorm (Set.indicator s ((fun i => F i) i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ δ x,
    ∀ (i : ℕ) (s : Set α),
      MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε
case intro
α : Type u_2
β : Type u_1
ι : Type ?u.497069
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), Memℒp (f n) p
hf_tendsto : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n) p μ ≤ ε
ε : ℝ
hε : 0 < ε
N : ℕ
hN : ∀ (n : ℕ), n ≥ N → snorm (f n) p μ ≤ ENNReal.ofReal ε
F : Fin N → α → β := fun n => f ↑n
hF : ∀ (n : Fin N), Memℒp (F n) p
⊢ ∃ δ x,
    ∀ (i : ℕ) (s : Set α),
      MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε
obtain ⟨δ₁, hδpos₁, hδ₁⟩ := unifIntegrable_fin μ hp hp' hF hε
case intro.intro.intro
α : Type u_2
β : Type u_1
ι : Type ?u.497069
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), Memℒp (f n) p
hf_tendsto : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n) p μ ≤ ε
ε : ℝ
hε : 0 < ε
N : ℕ
hN : ∀ (n : ℕ), n ≥ N → snorm (f n) p μ ≤ ENNReal.ofReal ε
F : Fin N → α → β := fun n => f ↑n
hF : ∀ (n : Fin N), Memℒp (F n) p
δ₁ : ℝ
hδpos₁ : 0 < δ₁
hδ₁ :
  ∀ (i : Fin N) (s : Set α),
    MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₁ → snorm (Set.indicator s ((fun i => F i) i)) p μ ≤ ENNReal.ofReal ε
n : ℕ
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal δ₁
⊢ snorm (Set.indicator s (f n)) p μ ≤ ENNReal.ofReal ε
case intro.intro.intro
α : Type u_2
β : Type u_1
ι : Type ?u.497069
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), Memℒp (f n) p
hf_tendsto : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n) p μ ≤ ε
ε : ℝ
hε : 0 < ε
N : ℕ
hN : ∀ (n : ℕ), n ≥ N → snorm (f n) p μ ≤ ENNReal.ofReal ε
F : Fin N → α → β := fun n => f ↑n
hF : ∀ (n : Fin N), Memℒp (F n) p
δ₁ : ℝ
hδpos₁ : 0 < δ₁
hδ₁ :
  ∀ (i : Fin N) (s : Set α),
    MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₁ → snorm (Set.indicator s ((fun i => F i) i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ δ x,
    ∀ (i : ℕ) (s : Set α),
      MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε
refine' ⟨δ₁, hδpos₁, fun n s hs hμs => _⟩
case pos
α : Type u_2
β : Type u_1
ι : Type ?u.497069
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), Memℒp (f n) p
hf_tendsto : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n) p μ ≤ ε
ε : ℝ
hε : 0 < ε
N : ℕ
hN : ∀ (n : ℕ), n ≥ N → snorm (f n) p μ ≤ ENNReal.ofReal ε
F : Fin N → α → β := fun n => f ↑n
hF : ∀ (n : Fin N), Memℒp (F n) p
δ₁ : ℝ
hδpos₁ : 0 < δ₁
hδ₁ :
  ∀ (i : Fin N) (s : Set α),
    MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₁ → snorm (Set.indicator s ((fun i => F i) i)) p μ ≤ ENNReal.ofReal ε
n : ℕ
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal δ₁
hn : n < N
⊢ snorm (Set.indicator s (f n)) p μ ≤ ENNReal.ofReal ε

case neg
α : Type u_2
β : Type u_1
ι : Type ?u.497069
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), Memℒp (f n) p
hf_tendsto : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n) p μ ≤ ε
ε : ℝ
hε : 0 < ε
N : ℕ
hN : ∀ (n : ℕ), n ≥ N → snorm (f n) p μ ≤ ENNReal.ofReal ε
F : Fin N → α → β := fun n => f ↑n
hF : ∀ (n : Fin N), Memℒp (F n) p
δ₁ : ℝ
hδpos₁ : 0 < δ₁
hδ₁ :
  ∀ (i : Fin N) (s : Set α),
    MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₁ → snorm (Set.indicator s ((fun i => F i) i)) p μ ≤ ENNReal.ofReal ε
n : ℕ
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal δ₁
hn : ¬n < N
⊢ snorm (Set.indicator s (f n)) p μ ≤ ENNReal.ofReal ε
case intro.intro.intro
α : Type u_2
β : Type u_1
ι : Type ?u.497069
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), Memℒp (f n) p
hf_tendsto : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n) p μ ≤ ε
ε : ℝ
hε : 0 < ε
N : ℕ
hN : ∀ (n : ℕ), n ≥ N → snorm (f n) p μ ≤ ENNReal.ofReal ε
F : Fin N → α → β := fun n => f ↑n
hF : ∀ (n : Fin N), Memℒp (F n) p
δ₁ : ℝ
hδpos₁ : 0 < δ₁
hδ₁ :
  ∀ (i : Fin N) (s : Set α),
    MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₁ → snorm (Set.indicator s ((fun i => F i) i)) p μ ≤ ENNReal.ofReal ε
n : ℕ
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal δ₁
⊢ snorm (Set.indicator s (f n)) p μ ≤ ENNReal.ofReal ε
by_cases hn : n < N
no goals
α : Type u_2
β : Type u_1
ι : Type ?u.497069
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), Memℒp (f n) p
hf_tendsto : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n) p μ ≤ ε
ε : ℝ
hε : 0 < ε
⊢ ENNReal.ofReal ε > 0
simpa
no goals
case pos
α : Type u_2
β : Type u_1
ι : Type ?u.497069
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), Memℒp (f n) p
hf_tendsto : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n) p μ ≤ ε
ε : ℝ
hε : 0 < ε
N : ℕ
hN : ∀ (n : ℕ), n ≥ N → snorm (f n) p μ ≤ ENNReal.ofReal ε
F : Fin N → α → β := fun n => f ↑n
hF : ∀ (n : Fin N), Memℒp (F n) p
δ₁ : ℝ
hδpos₁ : 0 < δ₁
hδ₁ :
  ∀ (i : Fin N) (s : Set α),
    MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₁ → snorm (Set.indicator s ((fun i => F i) i)) p μ ≤ ENNReal.ofReal ε
n : ℕ
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal δ₁
hn : n < N
⊢ snorm (Set.indicator s (f n)) p μ ≤ ENNReal.ofReal ε
exact hδ₁ ⟨n, hn⟩ s hs hμs
no goals
case neg
α : Type u_2
β : Type u_1
ι : Type ?u.497069
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), Memℒp (f n) p
hf_tendsto : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n) p μ ≤ ε
ε : ℝ
hε : 0 < ε
N : ℕ
hN : ∀ (n : ℕ), n ≥ N → snorm (f n) p μ ≤ ENNReal.ofReal ε
F : Fin N → α → β := fun n => f ↑n
hF : ∀ (n : Fin N), Memℒp (F n) p
δ₁ : ℝ
hδpos₁ : 0 < δ₁
hδ₁ :
  ∀ (i : Fin N) (s : Set α),
    MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ₁ → snorm (Set.indicator s ((fun i => F i) i)) p μ ≤ ENNReal.ofReal ε
n : ℕ
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal δ₁
hn : ¬n < N
⊢ snorm (Set.indicator s (f n)) p μ ≤ ENNReal.ofReal ε
exact (snorm_indicator_le _).trans (hN n (not_lt.1 hn))