α : Type u_2
E : Type u_1
F : Type ?u.8218613
G : Type ?u.8218616
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), Memℒp (f n) p
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : Tendsto (fun n => snorm (f n - f_lim) p μ) atTop (𝓝 0)
⊢ snorm f_lim p μ < ⊤
α : Type u_2
E : Type u_1
F : Type ?u.8218613
G : Type ?u.8218616
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), Memℒp (f n) p
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : Tendsto (fun n => snorm (f n - f_lim) p μ) atTop (𝓝 0)
⊢ Memℒp f_lim p
refine' ⟨h_lim_meas, _⟩
α : Type u_2
E : Type u_1
F : Type ?u.8218613
G : Type ?u.8218616
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), Memℒp (f n) p
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n - f_lim) p μ ≤ ε
⊢ snorm f_lim p μ < ⊤
α : Type u_2
E : Type u_1
F : Type ?u.8218613
G : Type ?u.8218616
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), Memℒp (f n) p
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : Tendsto (fun n => snorm (f n - f_lim) p μ) atTop (𝓝 0)
⊢ snorm f_lim p μ < ⊤
rw [ENNReal.tendsto_atTop_zero] at h_tendsto
case intro
α : Type u_2
E : Type u_1
F : Type ?u.8218613
G : Type ?u.8218616
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), Memℒp (f n) p
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : ∀ (n : ℕ), n ≥ N → snorm (f n - f_lim) p μ ≤ 1
⊢ snorm f_lim p μ < ⊤
α : Type u_2
E : Type u_1
F : Type ?u.8218613
G : Type ?u.8218616
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), Memℒp (f n) p
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n - f_lim) p μ ≤ ε
⊢ snorm f_lim p μ < ⊤
cases' h_tendsto 1 zero_lt_one with N h_tendsto_1
case intro
α : Type u_2
E : Type u_1
F : Type ?u.8218613
G : Type ?u.8218616
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), Memℒp (f n) p
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : snorm (f N - f_lim) p μ ≤ 1
⊢ snorm f_lim p μ < ⊤
case intro
α : Type u_2
E : Type u_1
F : Type ?u.8218613
G : Type ?u.8218616
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), Memℒp (f n) p
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : ∀ (n : ℕ), n ≥ N → snorm (f n - f_lim) p μ ≤ 1
⊢ snorm f_lim p μ < ⊤
specialize h_tendsto_1 N (le_refl N)
case intro
α : Type u_2
E : Type u_1
F : Type ?u.8218613
G : Type ?u.8218616
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), Memℒp (f n) p
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : snorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
⊢ snorm f_lim p μ < ⊤
case intro
α : Type u_2
E : Type u_1
F : Type ?u.8218613
G : Type ?u.8218616
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), Memℒp (f n) p
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : snorm (f N - f_lim) p μ ≤ 1
⊢ snorm f_lim p μ < ⊤
have h_add : f_lim = f_lim - f N + f N := by abel
case intro
α : Type u_2
E : Type u_1
F : Type ?u.8218613
G : Type ?u.8218616
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), Memℒp (f n) p
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : snorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
⊢ snorm (f_lim - f N + f N) p μ < ⊤
case intro
α : Type u_2
E : Type u_1
F : Type ?u.8218613
G : Type ?u.8218616
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), Memℒp (f n) p
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : snorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
⊢ snorm f_lim p μ < ⊤
rw [h_add]
case intro
α : Type u_2
E : Type u_1
F : Type ?u.8218613
G : Type ?u.8218616
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), Memℒp (f n) p
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : snorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
⊢ snorm (f_lim - f N) p μ + snorm (f N) p μ < ⊤
case intro
α : Type u_2
E : Type u_1
F : Type ?u.8218613
G : Type ?u.8218616
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), Memℒp (f n) p
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : snorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
⊢ snorm (f_lim - f N + f N) p μ < ⊤
refine' lt_of_le_of_lt (snorm_add_le (h_lim_meas.sub (hf N).1) (hf N).1 hp) _
case intro
α : Type u_2
E : Type u_1
F : Type ?u.8218613
G : Type ?u.8218616
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), Memℒp (f n) p
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : snorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
⊢ snorm (f_lim - f N) p μ < ⊤ ∧ snorm (f N) p μ < ⊤
case intro
α : Type u_2
E : Type u_1
F : Type ?u.8218613
G : Type ?u.8218616
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), Memℒp (f n) p
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : snorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
⊢ snorm (f_lim - f N) p μ + snorm (f N) p μ < ⊤
rw [ENNReal.add_lt_top]
case intro.left
α : Type u_2
E : Type u_1
F : Type ?u.8218613
G : Type ?u.8218616
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), Memℒp (f n) p
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : snorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
⊢ snorm (f_lim - f N) p μ < ⊤

case intro.right
α : Type u_2
E : Type u_1
F : Type ?u.8218613
G : Type ?u.8218616
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), Memℒp (f n) p
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : snorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
⊢ snorm (f N) p μ < ⊤
case intro
α : Type u_2
E : Type u_1
F : Type ?u.8218613
G : Type ?u.8218616
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), Memℒp (f n) p
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : snorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
⊢ snorm (f_lim - f N) p μ < ⊤ ∧ snorm (f N) p μ < ⊤
constructor
no goals
α : Type u_2
E : Type u_1
F : Type ?u.8218613
G : Type ?u.8218616
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), Memℒp (f n) p
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : snorm (f N - f_lim) p μ ≤ 1
⊢ f_lim = f_lim - f N + f N
abel
case intro.left
α : Type u_2
E : Type u_1
F : Type ?u.8218613
G : Type ?u.8218616
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), Memℒp (f n) p
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : snorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
⊢ snorm (f_lim - f N) p μ ≤ 1
case intro.left
α : Type u_2
E : Type u_1
F : Type ?u.8218613
G : Type ?u.8218616
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), Memℒp (f n) p
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : snorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
⊢ snorm (f_lim - f N) p μ < ⊤
refine' lt_of_le_of_lt _ ENNReal.one_lt_top
case intro.left
α : Type u_2
E : Type u_1
F : Type ?u.8218613
G : Type ?u.8218616
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), Memℒp (f n) p
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : snorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
h_neg : f_lim - f N = -(f N - f_lim)
⊢ snorm (f_lim - f N) p μ ≤ 1
case intro.left
α : Type u_2
E : Type u_1
F : Type ?u.8218613
G : Type ?u.8218616
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), Memℒp (f n) p
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : snorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
⊢ snorm (f_lim - f N) p μ ≤ 1
have h_neg : f_lim - f N = -(f N - f_lim) := by simp
no goals
case intro.left
α : Type u_2
E : Type u_1
F : Type ?u.8218613
G : Type ?u.8218616
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), Memℒp (f n) p
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : snorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
h_neg : f_lim - f N = -(f N - f_lim)
⊢ snorm (f_lim - f N) p μ ≤ 1
rwa [h_neg, snorm_neg]
no goals
α : Type u_2
E : Type u_1
F : Type ?u.8218613
G : Type ?u.8218616
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), Memℒp (f n) p
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : snorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
⊢ f_lim - f N = -(f N - f_lim)
simp
no goals
case intro.right
α : Type u_2
E : Type u_1
F : Type ?u.8218613
G : Type ?u.8218616
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), Memℒp (f n) p
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : snorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
⊢ snorm (f N) p μ < ⊤
exact (hf N).2