-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem completeSpace_lp_of_cauchy_complete_eLpNorm [hp : Fact (1 ≤ p)]
    (H :
      ∀ (f : ℕ → α → E) (_ : ∀ n, MemLp (f n) p μ) (B : ℕ → ℝ≥0∞) (_ : ∑' i, B i < ∞)
        (_ : ∀ N n m : ℕ, N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N),
        ∃ (f_lim : α → E), MemLp f_lim p μ ∧
          atTop.Tendsto (fun n => eLpNorm (f n - f_lim) p μ) (𝓝 0)) :
    CompleteSpace (Lp E p μ)

Proof state:
case intro
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        ∑' (i : ℕ), B i < ⊤ →
          (∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N) →
            ∃ f_lim, MemLp f_lim p μ ∧ Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : ℕ → ℝ := fun n => (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
M : ℝ
hB : HasSum B M
B1 : ℕ → ℝ≥0∞ := fun n => ENNReal.ofReal (B n)
hB1_has : HasSum B1 (ENNReal.ofReal M)
hB1 : ∑' (i : ℕ), B1 i < ⊤
f1 : ℕ → α → E := fun n => ↑↑(f n)
N n m : ℕ
hn : N ≤ n
hm : N ≤ m
hf : (eLpNorm (↑↑(f n) - ↑↑(f m)) p μ).toReal < B N
⊢ eLpNorm (↑↑(f n) - ↑↑(f m)) p μ ≠ ⊤

Tactic:
rw [eLpNorm_congr_ae (Lp.coeFn_sub _ _).symm]

Result:
case intro
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        ∑' (i : ℕ), B i < ⊤ →
          (∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N) →
            ∃ f_lim, MemLp f_lim p μ ∧ Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : ℕ → ℝ := fun n => (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
M : ℝ
hB : HasSum B M
B1 : ℕ → ℝ≥0∞ := fun n => ENNReal.ofReal (B n)
hB1_has : HasSum B1 (ENNReal.ofReal M)
hB1 : ∑' (i : ℕ), B1 i < ⊤
f1 : ℕ → α → E := fun n => ↑↑(f n)
N n m : ℕ
hn : N ≤ n
hm : N ≤ m
hf : (eLpNorm (↑↑(f n) - ↑↑(f m)) p μ).toReal < B N
⊢ eLpNorm (↑↑(f n - f m)) p μ ≠ ⊤

Proof state:
case intro
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        ∑' (i : ℕ), B i < ⊤ →
          (∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N) →
            ∃ f_lim, MemLp f_lim p μ ∧ Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : ℕ → ℝ := fun n => (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
hf : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) < B N
M : ℝ
hB : HasSum B M
B1 : ℕ → ℝ≥0∞ := fun n => ENNReal.ofReal (B n)
⊢ ∃ f_lim, MemLp f_lim p μ ∧ Tendsto (fun n => eLpNorm (↑↑(f n) - f_lim) p μ) atTop (𝓝 0)

Tactic:
have hB1_has : HasSum B1 (ENNReal.ofReal M) := by
  have h_tsum_B1 : ∑' i, B1 i = ENNReal.ofReal M := by
    change (∑' n : ℕ, ENNReal.ofReal (B n)) = ENNReal.ofReal M
    rw [← hB.tsum_eq]
    exact (ENNReal.ofReal_tsum_of_nonneg (fun n => le_of_lt (hB_pos n)) hB.summable).symm
  have h_sum := (@ENNReal.summable _ B1).hasSum
  rwa [h_tsum_B1] at h_sum

Result:
case intro
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        ∑' (i : ℕ), B i < ⊤ →
          (∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N) →
            ∃ f_lim, MemLp f_lim p μ ∧ Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : ℕ → ℝ := fun n => (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
hf : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) < B N
M : ℝ
hB : HasSum B M
B1 : ℕ → ℝ≥0∞ := fun n => ENNReal.ofReal (B n)
hB1_has : HasSum B1 (ENNReal.ofReal M)
⊢ ∃ f_lim, MemLp f_lim p μ ∧ Tendsto (fun n => eLpNorm (↑↑(f n) - f_lim) p μ) atTop (𝓝 0)

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        ∑' (i : ℕ), B i < ⊤ →
          (∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N) →
            ∃ f_lim, MemLp f_lim p μ ∧ Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : ℕ → ℝ := fun n => (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
hf : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) < B N
M : ℝ
hB : HasSum B M
B1 : ℕ → ℝ≥0∞ := fun n => ENNReal.ofReal (B n)
⊢ ∑' (n : ℕ), ENNReal.ofReal (B n) = ENNReal.ofReal (∑' (b : ℕ), B b)

Tactic:
exact (ENNReal.ofReal_tsum_of_nonneg (fun n => le_of_lt (hB_pos n)) hB.summable).symm

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        ∑' (i : ℕ), B i < ⊤ →
          (∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N) →
            ∃ f_lim, MemLp f_lim p μ ∧ Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : ℕ → ℝ := fun n => (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
hf : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) < B N
f_lim : α → E
hf_lim_meas : MemLp f_lim p μ
h_tendsto : Tendsto (fun n => eLpNorm (↑↑(f n) - f_lim) p μ) atTop (𝓝 0)
⊢ ∃ x, Tendsto f atTop (𝓝 x)

Tactic:
exact ⟨hf_lim_meas.toLp f_lim, tendsto_Lp_of_tendsto_eLpNorm f_lim hf_lim_meas h_tendsto⟩

Result:
no goals

Proof state:
case intro
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        ∑' (i : ℕ), B i < ⊤ →
          (∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N) →
            ∃ f_lim, MemLp f_lim p μ ∧ Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : ℕ → ℝ := fun n => (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
M : ℝ
hB : HasSum B M
B1 : ℕ → ℝ≥0∞ := fun n => ENNReal.ofReal (B n)
hB1_has : HasSum B1 (ENNReal.ofReal M)
hB1 : ∑' (i : ℕ), B1 i < ⊤
f1 : ℕ → α → E := fun n => ↑↑(f n)
N n m : ℕ
hn : N ≤ n
hm : N ≤ m
hf : (eLpNorm (↑↑(f n) - ↑↑(f m)) p μ).toReal < B N
⊢ eLpNorm (f1 n - f1 m) p μ < B1 N

Tactic:
dsimp only [f1]

Result:
case intro
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        ∑' (i : ℕ), B i < ⊤ →
          (∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N) →
            ∃ f_lim, MemLp f_lim p μ ∧ Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : ℕ → ℝ := fun n => (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
M : ℝ
hB : HasSum B M
B1 : ℕ → ℝ≥0∞ := fun n => ENNReal.ofReal (B n)
hB1_has : HasSum B1 (ENNReal.ofReal M)
hB1 : ∑' (i : ℕ), B1 i < ⊤
f1 : ℕ → α → E := fun n => ↑↑(f n)
N n m : ℕ
hn : N ≤ n
hm : N ≤ m
hf : (eLpNorm (↑↑(f n) - ↑↑(f m)) p μ).toReal < B N
⊢ eLpNorm (↑↑(f n) - ↑↑(f m)) p μ < B1 N