α : Type u_1
E : Type u_2
F : Type ?u.8211817
G : Type ?u.8211820
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
⊢ ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n - f_lim) p μ ≤ ε
α : Type u_1
E : Type u_2
F : Type ?u.8211817
G : Type ?u.8211820
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
⊢ Tendsto (fun n => snorm (f n - f_lim) p μ) atTop (𝓝 0)
rw [ENNReal.tendsto_atTop_zero]
α : Type u_1
E : Type u_2
F : Type ?u.8211817
G : Type ?u.8211820
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n - f_lim) p μ ≤ ε
α : Type u_1
E : Type u_2
F : Type ?u.8211817
G : Type ?u.8211820
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
⊢ ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n - f_lim) p μ ≤ ε
intro ε hε
α : Type u_1
E : Type u_2
F : Type ?u.8211817
G : Type ?u.8211820
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
h_B : ∃ N, B N ≤ ε
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n - f_lim) p μ ≤ ε
α : Type u_1
E : Type u_2
F : Type ?u.8211817
G : Type ?u.8211820
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n - f_lim) p μ ≤ ε
have h_B : ∃ N : ℕ, B N ≤ ε := by
  suffices h_tendsto_zero : ∃ N : ℕ, ∀ n : ℕ, N ≤ n → B n ≤ ε
  exact ⟨h_tendsto_zero.choose, h_tendsto_zero.choose_spec _ le_rfl⟩
  exact (ENNReal.tendsto_atTop_zero.mp (ENNReal.tendsto_atTop_zero_of_tsum_ne_top hB)) ε hε
case intro
α : Type u_1
E : Type u_2
F : Type ?u.8211817
G : Type ?u.8211820
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n - f_lim) p μ ≤ ε
α : Type u_1
E : Type u_2
F : Type ?u.8211817
G : Type ?u.8211820
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
h_B : ∃ N, B N ≤ ε
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n - f_lim) p μ ≤ ε
cases' h_B with N h_B
case intro
α : Type u_1
E : Type u_2
F : Type ?u.8211817
G : Type ?u.8211820
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
n : ℕ
hn : n ≥ N
⊢ snorm (f n - f_lim) p μ ≤ ε
case intro
α : Type u_1
E : Type u_2
F : Type ?u.8211817
G : Type ?u.8211820
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → snorm (f n - f_lim) p μ ≤ ε
refine' ⟨N, fun n hn => _⟩
case intro
α : Type u_1
E : Type u_2
F : Type ?u.8211817
G : Type ?u.8211820
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
n : ℕ
hn : n ≥ N
h_sub : snorm (f n - f_lim) p μ ≤ liminf (fun m => snorm (f n - f m) p μ) atTop
⊢ snorm (f n - f_lim) p μ ≤ ε
case intro
α : Type u_1
E : Type u_2
F : Type ?u.8211817
G : Type ?u.8211820
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
n : ℕ
hn : n ≥ N
⊢ snorm (f n - f_lim) p μ ≤ ε
have h_sub : snorm (f n - f_lim) p μ ≤ atTop.liminf fun m => snorm (f n - f m) p μ := by
  refine' snorm_lim_le_liminf_snorm (fun m => (hf n).sub (hf m)) (f n - f_lim) _
  refine' h_lim.mono fun x hx => _
  simp_rw [sub_eq_add_neg]
  exact Tendsto.add tendsto_const_nhds (Tendsto.neg hx)
case intro
α : Type u_1
E : Type u_2
F : Type ?u.8211817
G : Type ?u.8211820
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
n : ℕ
hn : n ≥ N
h_sub : snorm (f n - f_lim) p μ ≤ liminf (fun m => snorm (f n - f m) p μ) atTop
⊢ liminf (fun m => snorm (f n - f m) p μ) atTop ≤ ε
case intro
α : Type u_1
E : Type u_2
F : Type ?u.8211817
G : Type ?u.8211820
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
n : ℕ
hn : n ≥ N
h_sub : snorm (f n - f_lim) p μ ≤ liminf (fun m => snorm (f n - f m) p μ) atTop
⊢ snorm (f n - f_lim) p μ ≤ ε
refine' h_sub.trans _
case intro
α : Type u_1
E : Type u_2
F : Type ?u.8211817
G : Type ?u.8211820
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
n : ℕ
hn : n ≥ N
h_sub : snorm (f n - f_lim) p μ ≤ liminf (fun m => snorm (f n - f m) p μ) atTop
⊢ ∀ (a : ℕ), ∃ b, b ≥ a ∧ snorm (f n - f b) p μ ≤ ε
case intro
α : Type u_1
E : Type u_2
F : Type ?u.8211817
G : Type ?u.8211820
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
n : ℕ
hn : n ≥ N
h_sub : snorm (f n - f_lim) p μ ≤ liminf (fun m => snorm (f n - f m) p μ) atTop
⊢ liminf (fun m => snorm (f n - f m) p μ) atTop ≤ ε
refine' liminf_le_of_frequently_le' (frequently_atTop.mpr _)
case intro
α : Type u_1
E : Type u_2
F : Type ?u.8211817
G : Type ?u.8211820
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
n : ℕ
hn : n ≥ N
h_sub : snorm (f n - f_lim) p μ ≤ liminf (fun m => snorm (f n - f m) p μ) atTop
N1 : ℕ
⊢ snorm (f n - f (max N N1)) p μ ≤ ε
case intro
α : Type u_1
E : Type u_2
F : Type ?u.8211817
G : Type ?u.8211820
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
n : ℕ
hn : n ≥ N
h_sub : snorm (f n - f_lim) p μ ≤ liminf (fun m => snorm (f n - f m) p μ) atTop
⊢ ∀ (a : ℕ), ∃ b, b ≥ a ∧ snorm (f n - f b) p μ ≤ ε
refine' fun N1 => ⟨max N N1, le_max_right _ _, _⟩
no goals
case intro
α : Type u_1
E : Type u_2
F : Type ?u.8211817
G : Type ?u.8211820
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
n : ℕ
hn : n ≥ N
h_sub : snorm (f n - f_lim) p μ ≤ liminf (fun m => snorm (f n - f m) p μ) atTop
N1 : ℕ
⊢ snorm (f n - f (max N N1)) p μ ≤ ε
exact (h_cau N n (max N N1) hn (le_max_left _ _)).le.trans h_B
α : Type u_1
E : Type u_2
F : Type ?u.8211817
G : Type ?u.8211820
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
h_tendsto_zero : ∃ N, ∀ (n : ℕ), N ≤ n → B n ≤ ε
⊢ ∃ N, B N ≤ ε

case h_tendsto_zero
α : Type u_1
E : Type u_2
F : Type ?u.8211817
G : Type ?u.8211820
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
⊢ ∃ N, ∀ (n : ℕ), N ≤ n → B n ≤ ε
α : Type u_1
E : Type u_2
F : Type ?u.8211817
G : Type ?u.8211820
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
⊢ ∃ N, B N ≤ ε
suffices h_tendsto_zero : ∃ N : ℕ, ∀ n : ℕ, N ≤ n → B n ≤ ε
case h_tendsto_zero
α : Type u_1
E : Type u_2
F : Type ?u.8211817
G : Type ?u.8211820
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
⊢ ∃ N, ∀ (n : ℕ), N ≤ n → B n ≤ ε
α : Type u_1
E : Type u_2
F : Type ?u.8211817
G : Type ?u.8211820
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
h_tendsto_zero : ∃ N, ∀ (n : ℕ), N ≤ n → B n ≤ ε
⊢ ∃ N, B N ≤ ε

case h_tendsto_zero
α : Type u_1
E : Type u_2
F : Type ?u.8211817
G : Type ?u.8211820
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
⊢ ∃ N, ∀ (n : ℕ), N ≤ n → B n ≤ ε
exact ⟨h_tendsto_zero.choose, h_tendsto_zero.choose_spec _ le_rfl⟩
no goals
case h_tendsto_zero
α : Type u_1
E : Type u_2
F : Type ?u.8211817
G : Type ?u.8211820
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
⊢ ∃ N, ∀ (n : ℕ), N ≤ n → B n ≤ ε
exact (ENNReal.tendsto_atTop_zero.mp (ENNReal.tendsto_atTop_zero_of_tsum_ne_top hB)) ε hε
α : Type u_1
E : Type u_2
F : Type ?u.8211817
G : Type ?u.8211820
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
n : ℕ
hn : n ≥ N
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun n_1 => (f n - f n_1) x) atTop (𝓝 ((f n - f_lim) x))
α : Type u_1
E : Type u_2
F : Type ?u.8211817
G : Type ?u.8211820
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
n : ℕ
hn : n ≥ N
⊢ snorm (f n - f_lim) p μ ≤ liminf (fun m => snorm (f n - f m) p μ) atTop
refine' snorm_lim_le_liminf_snorm (fun m => (hf n).sub (hf m)) (f n - f_lim) _
α : Type u_1
E : Type u_2
F : Type ?u.8211817
G : Type ?u.8211820
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
n : ℕ
hn : n ≥ N
x : α
hx : Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
⊢ Tendsto (fun n_1 => (f n - f n_1) x) atTop (𝓝 ((f n - f_lim) x))
α : Type u_1
E : Type u_2
F : Type ?u.8211817
G : Type ?u.8211820
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
n : ℕ
hn : n ≥ N
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun n_1 => (f n - f n_1) x) atTop (𝓝 ((f n - f_lim) x))
refine' h_lim.mono fun x hx => _
α : Type u_1
E : Type u_2
F : Type ?u.8211817
G : Type ?u.8211820
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
n : ℕ
hn : n ≥ N
x : α
hx : Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
⊢ Tendsto (fun n_1 => (f n + -f n_1) x) atTop (𝓝 ((f n + -f_lim) x))
α : Type u_1
E : Type u_2
F : Type ?u.8211817
G : Type ?u.8211820
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
n : ℕ
hn : n ≥ N
x : α
hx : Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
⊢ Tendsto (fun n_1 => (f n - f n_1) x) atTop (𝓝 ((f n - f_lim) x))
simp_rw [sub_eq_add_neg]
no goals
α : Type u_1
E : Type u_2
F : Type ?u.8211817
G : Type ?u.8211820
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
n : ℕ
hn : n ≥ N
x : α
hx : Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
⊢ Tendsto (fun n_1 => (f n + -f n_1) x) atTop (𝓝 ((f n + -f_lim) x))
exact Tendsto.add tendsto_const_nhds (Tendsto.neg hx)