Scalar cauchy to limit

theorem scalar_cauchy_to_limit    [SecondCountableTopology E] [CompleteSpace E]    {p : ℝ≥0∞} (hp1 : 1 ≤ p) (hp_top : p ≠ ⊤)    {f : ℕ → α → E}    (hf_memLp : ∀ n, MemLp (f n) p μ)    (hf_cauchy : Tendsto (fun nm : ℕ × ℕ =>      eLpNorm (f nm.1 - f nm.2) p μ) atTop (nhds 0)) :    ∃ g : α → E,      MemLp g p μ ∧      Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (nhds 0) := by  let _ := hp_top  -- Same approach as exists_pi_limit_of_cauchy_eLpNorm:  -- extract controlled Cauchy subsequence → cauchy_complete_eLpNorm → upgrade convergence  have hp : p ≠ 0 := ne_of_gt (lt_of_lt_of_le (by simp : (0 : ℝ≥0∞) < 1) hp1)  -- Step A: pair-Cauchy → controlled bound for each ε = (2⁻¹)^(k+1)  have hpair : ∀ k : ℕ, ∃ M : ℕ, ∀ n m, M ≤ n → M ≤ m →      eLpNorm (f n - f m) p μ ≤ (2⁻¹ : ℝ≥0∞) ^ (k + 1) := by    intro k    have hε : (0 : ℝ≥0∞) < (2⁻¹ : ℝ≥0∞) ^ (k + 1) := ENNReal.pow_pos (by norm_num) _    obtain ⟨⟨N₁, N₂⟩, hNM⟩ := (ENNReal.tendsto_atTop_zero.mp hf_cauchy _ hε)    exact ⟨max N₁ N₂, fun n m hn hm => hNM ⟨n, m⟩      ⟨le_trans (le_max_left _ _) hn, le_trans (le_max_right _ _) hm⟩⟩  -- Step B: Make bounds nondecreasing  choose M_raw hM_raw using hpair  let M : ℕ → ℕ := fun k => (Finset.range (k + 1)).sup M_raw  have hM_ge : ∀ k, M_raw k ≤ M k :=    fun k => Finset.le_sup (f := M_raw) (Finset.mem_range.mpr (Nat.lt_succ_of_le le_rfl))  have hM_mono : Monotone M :=    fun _ _ hab => Finset.sup_mono (Finset.range_mono (Nat.add_le_add_right hab 1))  -- Step C: Controlled Cauchy bound  let f_sub : ℕ → α → E := fun k => f (M k)  have hf_sub_memLp : ∀ k, MemLp (f_sub k) p μ := fun k => hf_memLp (M k)  have hf_sub_cau : ∀ K n m, K ≤ n → K ≤ m →      eLpNorm (f_sub n - f_sub m) p μ < (2⁻¹ : ℝ≥0∞) ^ K := by    intro K n m hn hm    calc eLpNorm (f_sub n - f_sub m) p μ        ≤ (2⁻¹ : ℝ≥0∞) ^ (K + 1) :=          hM_raw K (M n) (M m) (le_trans (hM_ge K) (hM_mono hn))            (le_trans (hM_ge K) (hM_mono hm))      _ < (2⁻¹ : ℝ≥0∞) ^ K := by          rw [pow_succ']          calc (2⁻¹ : ℝ≥0∞) * (2⁻¹ : ℝ≥0∞) ^ K              < 1 * (2⁻¹ : ℝ≥0∞) ^ K :=                ENNReal.mul_lt_mul_left                  (ENNReal.pow_pos (by norm_num : (0 : ℝ≥0∞) < 2⁻¹) K).ne'                  (by simp : (2⁻¹ : ℝ≥0∞) ^ K ≠ ⊤)                  (by norm_num : (2⁻¹ : ℝ≥0∞) < 1)            _ = (2⁻¹ : ℝ≥0∞) ^ K := one_mul _  -- Step D: Apply cauchy_complete_eLpNorm  have hB_sum : ∑' k, (2⁻¹ : ℝ≥0∞) ^ k ≠ ⊤ := by    simp  have ⟨g_lim, hg_lim_memLp, hg_lim_tendsto_sub⟩ :=    MeasureTheory.Lp.cauchy_complete_eLpNorm hp1 hf_sub_memLp hB_sum hf_sub_cau  -- Step E: Full convergence (same as exists_pi_limit_of_cauchy_eLpNorm)  refine ⟨g_lim, hg_lim_memLp, ?_⟩  rw [ENNReal.tendsto_atTop_zero]  intro ε hε  obtain ⟨K₁, hK₁⟩ := ENNReal.tendsto_atTop_zero.mp hg_lim_tendsto_sub (ε / 2)    (ENNReal.half_pos hε.ne')  obtain ⟨K₂, hK₂⟩ := ENNReal.tendsto_atTop_zero.mp    (ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one (by norm_num : (2⁻¹ : ℝ≥0∞) < 1))    (ε / 2) (ENNReal.half_pos hε.ne')  let K := max K₁ K₂  refine ⟨M K, fun n hn => ?_⟩  have hn_ge : M_raw K ≤ n := le_trans (hM_ge K) hn  have hMK_ge : M_raw K ≤ M K := hM_ge K  calc eLpNorm (f n - g_lim) p μ      = eLpNorm ((f n - f (M K)) + (f_sub K - g_lim)) p μ := by        congr 1; ext x; simp [f_sub, sub_add_sub_cancel]    _ ≤ eLpNorm (f n - f (M K)) p μ + eLpNorm (f_sub K - g_lim) p μ :=        eLpNorm_add_le ((hf_memLp n).sub (hf_memLp (M K))).aestronglyMeasurable          ((hf_sub_memLp K).sub hg_lim_memLp).aestronglyMeasurable          hp1    _ ≤ ε / 2 + ε / 2 := by        gcongr        · calc eLpNorm (f n - f (M K)) p μ              ≤ (2⁻¹ : ℝ≥0∞) ^ (K + 1) := hM_raw K n (M K) hn_ge hMK_ge            _ ≤ ε / 2 := hK₂ (K + 1) (Nat.le_add_right K₂ 1 |>.trans                (Nat.add_le_add_right (le_max_right K₁ K₂) 1))        · exact hK₁ K (le_max_left K₁ K₂)    _ = ε := ENNReal.add_halves ε