case pos
α : Type u_2
E : Type u_1
F : Type ?u.8203466
G : Type ?u.8203469
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
hp_top : p = ⊤
⊢ ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) atTop (𝓝 l)

case neg
α : Type u_2
E : Type u_1
F : Type ?u.8203466
G : Type ?u.8203469
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
hp_top : ¬p = ⊤
⊢ ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) atTop (𝓝 l)
α : Type u_2
E : Type u_1
F : Type ?u.8203466
G : Type ?u.8203469
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
⊢ ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) atTop (𝓝 l)
by_cases hp_top : p = ∞
case neg
α : Type u_2
E : Type u_1
F : Type ?u.8203466
G : Type ?u.8203469
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
hp_top : ¬p = ⊤
hp1 : 1 ≤ ENNReal.toReal p
⊢ ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) atTop (𝓝 l)
case neg
α : Type u_2
E : Type u_1
F : Type ?u.8203466
G : Type ?u.8203469
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
hp_top : ¬p = ⊤
⊢ ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) atTop (𝓝 l)
have hp1 : 1 ≤ p.toReal := by
  rw [← ENNReal.ofReal_le_iff_le_toReal hp_top, ENNReal.ofReal_one]
  exact hp
case neg
α : Type u_2
E : Type u_1
F : Type ?u.8203466
G : Type ?u.8203469
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
hp_top : ¬p = ⊤
hp1 : 1 ≤ ENNReal.toReal p
h_cau' : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm' (f n - f m) (ENNReal.toReal p) μ < B N
⊢ ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) atTop (𝓝 l)
case neg
α : Type u_2
E : Type u_1
F : Type ?u.8203466
G : Type ?u.8203469
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
hp_top : ¬p = ⊤
hp1 : 1 ≤ ENNReal.toReal p
⊢ ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) atTop (𝓝 l)
have h_cau' : ∀ N n m : ℕ, N ≤ n → N ≤ m → snorm' (f n - f m) p.toReal μ < B N := by
  intro N n m hn hm
  specialize h_cau N n m hn hm
  rwa [snorm_eq_snorm' (zero_lt_one.trans_le hp).ne.symm hp_top] at h_cau
no goals
case neg
α : Type u_2
E : Type u_1
F : Type ?u.8203466
G : Type ?u.8203469
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
hp_top : ¬p = ⊤
hp1 : 1 ≤ ENNReal.toReal p
h_cau' : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm' (f n - f m) (ENNReal.toReal p) μ < B N
⊢ ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) atTop (𝓝 l)
exact ae_tendsto_of_cauchy_snorm' hf hp1 hB h_cau'
case pos
α : Type u_2
E : Type u_1
F : Type ?u.8203466
G : Type ?u.8203469
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
hp : True
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) ⊤ μ < B N
hp_top : True
⊢ ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) atTop (𝓝 l)
case pos
α : Type u_2
E : Type u_1
F : Type ?u.8203466
G : Type ?u.8203469
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
hp_top : p = ⊤
⊢ ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) atTop (𝓝 l)
simp_rw [hp_top] at *
case pos
α : Type u_2
E : Type u_1
F : Type ?u.8203466
G : Type ?u.8203469
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
hp : True
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) ⊤ μ < B N
hp_top : True
h_cau_ae : ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ↑‖(f n - f m) x‖₊ < B N
⊢ ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) atTop (𝓝 l)
case pos
α : Type u_2
E : Type u_1
F : Type ?u.8203466
G : Type ?u.8203469
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
hp : True
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) ⊤ μ < B N
hp_top : True
⊢ ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) atTop (𝓝 l)
have h_cau_ae : ∀ᵐ x ∂μ, ∀ N n m, N ≤ n → N ≤ m → (‖(f n - f m) x‖₊ : ℝ≥0∞) < B N := by
  simp_rw [ae_all_iff]
  exact fun N n m hnN hmN => ae_lt_of_essSup_lt (h_cau N n m hnN hmN)
case pos
α : Type u_2
E : Type u_1
F : Type ?u.8203466
G : Type ?u.8203469
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
hp hp_top : True
h_cau_ae : ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ↑‖(f n - f m) x‖₊ < B N
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → essSup (fun x => ↑‖(f n - f m) x‖₊) μ < B N
⊢ ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) atTop (𝓝 l)
case pos
α : Type u_2
E : Type u_1
F : Type ?u.8203466
G : Type ?u.8203469
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
hp : True
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) ⊤ μ < B N
hp_top : True
h_cau_ae : ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ↑‖(f n - f m) x‖₊ < B N
⊢ ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) atTop (𝓝 l)
simp_rw [snorm_exponent_top, snormEssSup] at h_cau
case pos
α : Type u_2
E : Type u_1
F : Type ?u.8203466
G : Type ?u.8203469
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
hp hp_top : True
h_cau_ae : ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ↑‖(f n - f m) x‖₊ < B N
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → essSup (fun x => ↑‖(f n - f m) x‖₊) μ < B N
x : α
hx : ∀ (N n m : ℕ), N ≤ n → N ≤ m → ↑‖(f n - f m) x‖₊ < B N
⊢ CauchySeq fun n => f n x
case pos
α : Type u_2
E : Type u_1
F : Type ?u.8203466
G : Type ?u.8203469
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
hp hp_top : True
h_cau_ae : ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ↑‖(f n - f m) x‖₊ < B N
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → essSup (fun x => ↑‖(f n - f m) x‖₊) μ < B N
⊢ ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) atTop (𝓝 l)
refine' h_cau_ae.mono fun x hx => cauchySeq_tendsto_of_complete _
case pos.refine'_1
α : Type u_2
E : Type u_1
F : Type ?u.8203466
G : Type ?u.8203469
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
hp hp_top : True
h_cau_ae : ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ↑‖(f n - f m) x‖₊ < B N
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → essSup (fun x => ↑‖(f n - f m) x‖₊) μ < B N
x : α
hx : ∀ (N n m : ℕ), N ≤ n → N ≤ m → ↑‖(f n - f m) x‖₊ < B N
⊢ ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n x) (f m x) ≤ (fun n => ENNReal.toReal (B n)) N

case pos.refine'_2
α : Type u_2
E : Type u_1
F : Type ?u.8203466
G : Type ?u.8203469
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
hp hp_top : True
h_cau_ae : ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ↑‖(f n - f m) x‖₊ < B N
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → essSup (fun x => ↑‖(f n - f m) x‖₊) μ < B N
x : α
hx : ∀ (N n m : ℕ), N ≤ n → N ≤ m → ↑‖(f n - f m) x‖₊ < B N
⊢ Tendsto (fun n => ENNReal.toReal (B n)) atTop (𝓝 0)
case pos
α : Type u_2
E : Type u_1
F : Type ?u.8203466
G : Type ?u.8203469
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
hp hp_top : True
h_cau_ae : ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ↑‖(f n - f m) x‖₊ < B N
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → essSup (fun x => ↑‖(f n - f m) x‖₊) μ < B N
x : α
hx : ∀ (N n m : ℕ), N ≤ n → N ≤ m → ↑‖(f n - f m) x‖₊ < B N
⊢ CauchySeq fun n => f n x
refine' cauchySeq_of_le_tendsto_0 (fun n => (B n).toReal) _ _
α : Type u_2
E : Type u_1
F : Type ?u.8203466
G : Type ?u.8203469
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
hp : True
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) ⊤ μ < B N
hp_top : True
⊢ ∀ (i i_1 i_2 : ℕ), i ≤ i_1 → i ≤ i_2 → ∀ᵐ (a : α) ∂μ, ↑‖(f i_1 - f i_2) a‖₊ < B i
α : Type u_2
E : Type u_1
F : Type ?u.8203466
G : Type ?u.8203469
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
hp : True
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) ⊤ μ < B N
hp_top : True
⊢ ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ↑‖(f n - f m) x‖₊ < B N
simp_rw [ae_all_iff]
no goals
α : Type u_2
E : Type u_1
F : Type ?u.8203466
G : Type ?u.8203469
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
hp : True
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) ⊤ μ < B N
hp_top : True
⊢ ∀ (i i_1 i_2 : ℕ), i ≤ i_1 → i ≤ i_2 → ∀ᵐ (a : α) ∂μ, ↑‖(f i_1 - f i_2) a‖₊ < B i
exact fun N n m hnN hmN => ae_lt_of_essSup_lt (h_cau N n m hnN hmN)
case pos.refine'_1
α : Type u_2
E : Type u_1
F : Type ?u.8203466
G : Type ?u.8203469
m✝ m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
hp hp_top : True
h_cau_ae : ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ↑‖(f n - f m) x‖₊ < B N
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → essSup (fun x => ↑‖(f n - f m) x‖₊) μ < B N
x : α
hx : ∀ (N n m : ℕ), N ≤ n → N ≤ m → ↑‖(f n - f m) x‖₊ < B N
n m N : ℕ
hnN : N ≤ n
hmN : N ≤ m
⊢ dist (f n x) (f m x) ≤ (fun n => ENNReal.toReal (B n)) N
case pos.refine'_1
α : Type u_2
E : Type u_1
F : Type ?u.8203466
G : Type ?u.8203469
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
hp hp_top : True
h_cau_ae : ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ↑‖(f n - f m) x‖₊ < B N
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → essSup (fun x => ↑‖(f n - f m) x‖₊) μ < B N
x : α
hx : ∀ (N n m : ℕ), N ≤ n → N ≤ m → ↑‖(f n - f m) x‖₊ < B N
⊢ ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n x) (f m x) ≤ (fun n => ENNReal.toReal (B n)) N
intro n m N hnN hmN
case pos.refine'_1
α : Type u_2
E : Type u_1
F : Type ?u.8203466
G : Type ?u.8203469
m✝ m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
hp hp_top : True
h_cau_ae : ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ↑‖(f n - f m) x‖₊ < B N
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → essSup (fun x => ↑‖(f n - f m) x‖₊) μ < B N
x : α
n m N : ℕ
hnN : N ≤ n
hmN : N ≤ m
hx : ↑‖(f n - f m) x‖₊ < B N
⊢ dist (f n x) (f m x) ≤ (fun n => ENNReal.toReal (B n)) N
case pos.refine'_1
α : Type u_2
E : Type u_1
F : Type ?u.8203466
G : Type ?u.8203469
m✝ m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
hp hp_top : True
h_cau_ae : ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ↑‖(f n - f m) x‖₊ < B N
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → essSup (fun x => ↑‖(f n - f m) x‖₊) μ < B N
x : α
hx : ∀ (N n m : ℕ), N ≤ n → N ≤ m → ↑‖(f n - f m) x‖₊ < B N
n m N : ℕ
hnN : N ≤ n
hmN : N ≤ m
⊢ dist (f n x) (f m x) ≤ (fun n => ENNReal.toReal (B n)) N
specialize hx N n m hnN hmN
case pos.refine'_1
α : Type u_2
E : Type u_1
F : Type ?u.8203466
G : Type ?u.8203469
m✝ m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
hp hp_top : True
h_cau_ae : ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ↑‖(f n - f m) x‖₊ < B N
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → essSup (fun x => ↑‖(f n - f m) x‖₊) μ < B N
x : α
n m N : ℕ
hnN : N ≤ n
hmN : N ≤ m
hx : ↑‖(f n - f m) x‖₊ < B N
⊢ ENNReal.ofReal ‖f n x - f m x‖ ≤ B N
case pos.refine'_1
α : Type u_2
E : Type u_1
F : Type ?u.8203466
G : Type ?u.8203469
m✝ m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
hp hp_top : True
h_cau_ae : ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ↑‖(f n - f m) x‖₊ < B N
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → essSup (fun x => ↑‖(f n - f m) x‖₊) μ < B N
x : α
n m N : ℕ
hnN : N ≤ n
hmN : N ≤ m
hx : ↑‖(f n - f m) x‖₊ < B N
⊢ dist (f n x) (f m x) ≤ (fun n => ENNReal.toReal (B n)) N
rw [dist_eq_norm, ← ENNReal.toReal_ofReal (norm_nonneg _),
  ENNReal.toReal_le_toReal ENNReal.ofReal_ne_top (ENNReal.ne_top_of_tsum_ne_top hB N)]
case pos.refine'_1
α : Type u_2
E : Type u_1
F : Type ?u.8203466
G : Type ?u.8203469
m✝ m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
hp hp_top : True
h_cau_ae : ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ↑‖(f n - f m) x‖₊ < B N
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → essSup (fun x => ↑‖(f n - f m) x‖₊) μ < B N
x : α
n m N : ℕ
hnN : N ≤ n
hmN : N ≤ m
hx : ENNReal.ofReal ‖(f n - f m) x‖ < B N
⊢ ENNReal.ofReal ‖f n x - f m x‖ ≤ B N
case pos.refine'_1
α : Type u_2
E : Type u_1
F : Type ?u.8203466
G : Type ?u.8203469
m✝ m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
hp hp_top : True
h_cau_ae : ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ↑‖(f n - f m) x‖₊ < B N
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → essSup (fun x => ↑‖(f n - f m) x‖₊) μ < B N
x : α
n m N : ℕ
hnN : N ≤ n
hmN : N ≤ m
hx : ↑‖(f n - f m) x‖₊ < B N
⊢ ENNReal.ofReal ‖f n x - f m x‖ ≤ B N
rw [← ofReal_norm_eq_coe_nnnorm] at hx
no goals
case pos.refine'_1
α : Type u_2
E : Type u_1
F : Type ?u.8203466
G : Type ?u.8203469
m✝ m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
hp hp_top : True
h_cau_ae : ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ↑‖(f n - f m) x‖₊ < B N
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → essSup (fun x => ↑‖(f n - f m) x‖₊) μ < B N
x : α
n m N : ℕ
hnN : N ≤ n
hmN : N ≤ m
hx : ENNReal.ofReal ‖(f n - f m) x‖ < B N
⊢ ENNReal.ofReal ‖f n x - f m x‖ ≤ B N
exact hx.le
case pos.refine'_2
α : Type u_2
E : Type u_1
F : Type ?u.8203466
G : Type ?u.8203469
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
hp hp_top : True
h_cau_ae : ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ↑‖(f n - f m) x‖₊ < B N
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → essSup (fun x => ↑‖(f n - f m) x‖₊) μ < B N
x : α
hx : ∀ (N n m : ℕ), N ≤ n → N ≤ m → ↑‖(f n - f m) x‖₊ < B N
⊢ Tendsto (fun n => ENNReal.toReal (B n)) atTop (𝓝 (ENNReal.toReal 0))
case pos.refine'_2
α : Type u_2
E : Type u_1
F : Type ?u.8203466
G : Type ?u.8203469
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
hp hp_top : True
h_cau_ae : ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ↑‖(f n - f m) x‖₊ < B N
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → essSup (fun x => ↑‖(f n - f m) x‖₊) μ < B N
x : α
hx : ∀ (N n m : ℕ), N ≤ n → N ≤ m → ↑‖(f n - f m) x‖₊ < B N
⊢ Tendsto (fun n => ENNReal.toReal (B n)) atTop (𝓝 0)
rw [← ENNReal.zero_toReal]
no goals
case pos.refine'_2
α : Type u_2
E : Type u_1
F : Type ?u.8203466
G : Type ?u.8203469
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
hp hp_top : True
h_cau_ae : ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ↑‖(f n - f m) x‖₊ < B N
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → essSup (fun x => ↑‖(f n - f m) x‖₊) μ < B N
x : α
hx : ∀ (N n m : ℕ), N ≤ n → N ≤ m → ↑‖(f n - f m) x‖₊ < B N
⊢ Tendsto (fun n => ENNReal.toReal (B n)) atTop (𝓝 (ENNReal.toReal 0))
exact
  Tendsto.comp (g := ENNReal.toReal) (ENNReal.tendsto_toReal ENNReal.zero_ne_top)
    (ENNReal.tendsto_atTop_zero_of_tsum_ne_top hB)
α : Type u_2
E : Type u_1
F : Type ?u.8203466
G : Type ?u.8203469
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
hp_top : ¬p = ⊤
⊢ 1 ≤ p
α : Type u_2
E : Type u_1
F : Type ?u.8203466
G : Type ?u.8203469
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
hp_top : ¬p = ⊤
⊢ 1 ≤ ENNReal.toReal p
rw [← ENNReal.ofReal_le_iff_le_toReal hp_top, ENNReal.ofReal_one]
no goals
α : Type u_2
E : Type u_1
F : Type ?u.8203466
G : Type ?u.8203469
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
hp_top : ¬p = ⊤
⊢ 1 ≤ p
exact hp
α : Type u_2
E : Type u_1
F : Type ?u.8203466
G : Type ?u.8203469
m✝ m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
hp_top : ¬p = ⊤
hp1 : 1 ≤ ENNReal.toReal p
N n m : ℕ
hn : N ≤ n
hm : N ≤ m
⊢ snorm' (f n - f m) (ENNReal.toReal p) μ < B N
α : Type u_2
E : Type u_1
F : Type ?u.8203466
G : Type ?u.8203469
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
hp_top : ¬p = ⊤
hp1 : 1 ≤ ENNReal.toReal p
⊢ ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm' (f n - f m) (ENNReal.toReal p) μ < B N
intro N n m hn hm
α : Type u_2
E : Type u_1
F : Type ?u.8203466
G : Type ?u.8203469
m✝ m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
hp_top : ¬p = ⊤
hp1 : 1 ≤ ENNReal.toReal p
N n m : ℕ
hn : N ≤ n
hm : N ≤ m
h_cau : snorm (f n - f m) p μ < B N
⊢ snorm' (f n - f m) (ENNReal.toReal p) μ < B N
α : Type u_2
E : Type u_1
F : Type ?u.8203466
G : Type ?u.8203469
m✝ m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → snorm (f n - f m) p μ < B N
hp_top : ¬p = ⊤
hp1 : 1 ≤ ENNReal.toReal p
N n m : ℕ
hn : N ≤ n
hm : N ≤ m
⊢ snorm' (f n - f m) (ENNReal.toReal p) μ < B N
specialize h_cau N n m hn hm
no goals
α : Type u_2
E : Type u_1
F : Type ?u.8203466
G : Type ?u.8203469
m✝ m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hp : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : (∑' (i : ℕ), B i) ≠ ⊤
hp_top : ¬p = ⊤
hp1 : 1 ≤ ENNReal.toReal p
N n m : ℕ
hn : N ≤ n
hm : N ≤ m
h_cau : snorm (f n - f m) p μ < B N
⊢ snorm' (f n - f m) (ENNReal.toReal p) μ < B N
rwa [snorm_eq_snorm' (zero_lt_one.trans_le hp).ne.symm hp_top] at h_cau