tendsto_tsum_of_monotone_convergence_nhdsGT_one

lemma tendsto_tsum_of_monotone_convergence_nhdsGT_one    {F : ℝ → ℕ → ℝ}    (hF_nonneg : ∀ σ n, 0 ≤ F σ n)    (hF_antitone : ∀ n, AntitoneOn (fun σ : ℝ => F σ n) (Set.Ioi (1 : ℝ)))    (hF_tend : ∀ n, Tendsto (fun σ : ℝ => F σ n) (𝓝[>] (1 : ℝ)) (𝓝 (F 1 n)))    (hSumm : ∀ σ, 1 < σ → Summable (fun n : ℕ => F σ n))    (hbounded :      BoundedAtFilter (𝓝[>] (1 : ℝ)) (fun σ : ℝ => (∑' n : ℕ, F σ n))) :    Tendsto (fun σ : ℝ => ∑' n : ℕ, F σ n) (𝓝[>] (1 : ℝ)) (𝓝 (∑' n : ℕ, F 1 n)) := by  let T : ℝ → ℝ := fun σ => ∑' n : ℕ, F σ n  have hT_antitone : AntitoneOn T (Set.Ioi (1 : ℝ)) := fun a ha b hb hab ↦    (hSumm b hb).tsum_le_tsum_of_inj (fun n ↦ n) (fun _ _ h ↦ h) (fun c hc ↦ (hc ⟨c, rfl⟩).elim)      (fun n ↦ hF_antitone n ha hb hab) (hSumm a ha)  have hT_bdd : BddAbove (T '' Set.Ioi (1 : ℝ)) := by    obtain ⟨C, hC⟩ := isBigO_iff.1 hbounded    have hC' : ∀ᶠ σ : ℝ in 𝓝[>] (1 : ℝ), T σ ≤ C := by      filter_upwards [hC] with σ hσ      calc T σ ≤ |T σ| := le_abs_self _        _ = ‖T σ‖ := (Real.norm_eq_abs _).symm        _ ≤ C * ‖(1 : ℝ → ℝ) σ‖ := hσ        _ = C := by simp    obtain ⟨U, hU, V, hV, hUV⟩ := Filter.mem_inf_iff_superset.1 hC'    obtain ⟨ε, hε, hball⟩ := Metric.mem_nhds_iff.1 hU    have hIoi_sub : Set.Ioi (1 : ℝ) ⊆ V := Filter.mem_principal.mp hV    have hUsub : U ∩ Set.Ioi (1 : ℝ) ⊆ {σ : ℝ | T σ ≤ C} := fun σ hσ ↦ hUV ⟨hσ.1, hIoi_sub hσ.2⟩    have hσ0_Ioi : 1 + ε / 2 ∈ Set.Ioi (1 : ℝ) := by simp [half_pos hε]    have hσ0_leC : T (1 + ε / 2) ≤ C :=      hUsub ⟨hball (by simp only [Metric.mem_ball, Real.dist_eq, add_sub_cancel_left,        abs_of_pos (half_pos hε)]; exact half_lt_self hε), hσ0_Ioi⟩    refine ⟨C, ?_⟩    rintro _ ⟨σ, hσIoi, rfl⟩    by_cases hσlt : σ < 1 + ε / 2    · exact hUsub ⟨hball (by        simp only [Metric.mem_ball, Real.dist_eq]        rw [abs_of_pos (sub_pos.2 (Set.mem_Ioi.mp hσIoi))]        linarith [half_lt_self hε]), hσIoi⟩    · exact (hT_antitone hσ0_Ioi hσIoi (le_of_not_gt hσlt)).trans hσ0_leC  have hT_tend_sup : Tendsto T (𝓝[>] (1 : ℝ)) (𝓝 (sSup (T '' Set.Ioi (1 : ℝ)))) :=    hT_antitone.tendsto_nhdsGT hT_bdd  let σseq : ℕ → ℝ := fun k => 1 + 1 / (k + 1 : ℝ)  have hσseq_mem (k) : σseq k ∈ Set.Ioi (1 : ℝ) := by    simp only [σseq, Set.mem_Ioi, lt_add_iff_pos_right]    positivity  have hσseq_tend_nhds : Tendsto σseq atTop (𝓝 (1 : ℝ)) := by    have : Tendsto (fun k : ℕ => (1 : ℝ) + ((k + 1 : ℕ) : ℝ)⁻¹) atTop (𝓝 ((1 : ℝ) + 0)) :=      tendsto_const_nhds.add (tendsto_inv_atTop_nhds_zero_nat.comp (tendsto_add_atTop_nat 1))    simp only [add_zero] at this    convert this using 1; ext k; simp [σseq, one_div]  have hσseq_tend_nhdsWithin : Tendsto σseq atTop (𝓝[>] (1 : ℝ)) :=    tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ hσseq_tend_nhds      (.of_forall hσseq_mem)  have hσseq_antitone : Antitone σseq := fun k₁ k₂ hk ↦ by simp only [σseq]; gcongr  have hmono_seq (n) : Monotone (fun k => F (σseq k) n) := fun k₁ k₂ hk ↦    hF_antitone n (hσseq_mem k₂) (hσseq_mem k₁) (hσseq_antitone hk)  have htend_seq (n) : Tendsto (fun k => F (σseq k) n) atTop (𝓝 (F 1 n)) :=    (hF_tend n).comp hσseq_tend_nhdsWithin  have hTseq : Tendsto (fun k : ℕ => T (σseq k)) atTop (𝓝 (T 1)) := by    have hsum1 : Summable (fun n : ℕ => F (1 : ℝ) n) := by      obtain ⟨C, hC⟩ := hT_bdd      refine summable_of_sum_range_le (hF_nonneg 1) fun m ↦ le_of_tendsto        (tendsto_finsetSum _ fun i _ ↦ hF_tend i)        (eventually_of_mem self_mem_nhdsWithin fun σ hσ ↦          ((hSumm σ hσ).sum_le_tsum _ (fun n _ ↦ hF_nonneg σ n)).trans (hC ⟨σ, hσ, rfl⟩))    have hg_ne_top : (∑' n : ℕ, ENNReal.ofReal (F 1 n)) ≠ ⊤ := hsum1.tsum_ofReal_ne_top    have hENN : Tendsto (fun k => ∑' n, ENNReal.ofReal (F (σseq k) n)) atTop        (𝓝 (∑' n, ENNReal.ofReal (F 1 n))) :=      tendsto_tsum_of_monotone_convergence (fun n _ _ hk ↦ ENNReal.ofReal_le_ofReal (hmono_seq n hk))        (fun n ↦ ENNReal.tendsto_ofReal (htend_seq n))    have hrew (σ) : (∑' n, ENNReal.ofReal (F σ n)).toReal = ∑' n, F σ n := by      rw [ENNReal.tsum_toReal_eq (fun n ↦ by simp)]      exact tsum_congr fun n ↦ by simp [hF_nonneg σ n]    simp only [T, ← hrew]; exact (ENNReal.tendsto_toReal hg_ne_top).comp hENN  have hsSup_eq : sSup (T '' Set.Ioi (1 : ℝ)) = T 1 :=    tendsto_nhds_unique (hT_tend_sup.comp hσseq_tend_nhdsWithin) hTseq  simpa [T, hsSup_eq] using hT_tend_sup