proposition: Theorem Bolzano_Weierstrass_gen : ∀ (a : ℕ → ℝ) (i : has_ub a) (ii : has_lb (sequence_ub a (i))), ∃ (n : ℕ → ℕ), is_index_seq n ∧ Un_cv (fun (k : ℕ) ↦ a (n k)) (proj1_sig(_,_,lim_sup_bdd a (i) (ii))).
proof: Proof. Take a : (ℕ → ℝ). Assume that (has_ub a) (i). Assume that (has_lb (sequence_ub a (i))) (ii). Define L_with_proof := (lim_sup_bdd a (i) (ii)). Define L := (proj1_sig L_with_proof). Define sequence_ub_cv_to_L := (proj2_sig L_with_proof). We claim that (∃ m : ℕ → ℕ, is_index_seq m ∧ ∀ k : ℕ, a (m k) > L - 1 / (INR(k) + 1)). { By exists_subseq_to_limsup_bdd it holds that (there exists n : ℕ ⇨ ℕ, is_index_seq n ∧ (for all k : ℕ, a (n k) > proj1_sig(_,_,lim_sup_bdd a (i) (ii)) - 1 / (k + 1))). Obtain such an m_seq. It holds that (is_index_seq m_seq ∧ (for all k : ℕ, a (m_seq k) > proj1_sig(_,_,lim_sup_bdd a i ii) - 1 / (k + 1))) (v). Because (v) both (is_index_seq m_seq) and (for all k : ℕ, a (m_seq k) > proj1_sig(_,_,lim_sup_bdd a (i) (ii)) - 1 / (k + 1)) (vi) hold. Choose m := m_seq. We show both statements. - We need to show that (is_index_seq m). We conclude that (is_index_seq m). - We need to show that (for all k : ℕ, a (m k) > L - 1 / (k + 1)). By (vi) we conclude that (∀ k : ℕ, a (m k) > L - 1 / (INR(k) + 1)). } Obtain such an m. It holds that (is_index_seq m ∧ (for all k : ℕ, a (m k) > L - 1 / (k + 1))) (iv). Because (iv) both (is_index_seq m) (v) and (for all k : ℕ, a (m k) > L - 1 / (k + 1)) (vi) hold. Choose n := m. We need to show that (is_index_seq m ∧ Un_cv (fun k ↦ a(m(k)), L)). We show both statements. - We need to show that (is_index_seq m). It suffices to show that (is_index_seq n). By (v) we conclude that (is_index_seq n). - We need to show that (Un_cv (fun k ↦ a(n(k)), L)). apply (squeeze_theorem (fun (k : ℕ) ↦ L - 1 / (INR k + 1)) (fun (k : ℕ) ↦ (a (n k))) (sequence_ub a (i))). + Take k : ℕ. We show both statements. * We need to show that (L - 1 / (k + 1) ≤ a (n k)). By (vi) it holds that (a (m k) > L - 1 / (k+1)). We conclude that (L - 1 / (k + 1) ≤ a (n k)). * We need to show that (a (n k) ≤ sequence_ub a (i) k). By index_seq_grows_0 it holds that (m k ≥ k)%nat. By sequence_ub_bds we conclude that (a (n k) ≤ sequence_ub a (i) k). + We need to show that (Un_cv (fun k ↦ (L - 1 / (k + 1))) L). By lim_const_min_1_over_n_plus_1 we conclude that (Un_cv (fun k ↦ L - 1 / (k + 1), L)). + By sequence_ub_cv_to_L we conclude that (sequence_ub a (i) ⟶ L). Qed.
imports: Coq.Reals.Reals Lra Classical Classical_Pred_Type Automation Libs.Analysis.Sequences Libs.Analysis.Subsequences Libs.Analysis.SupAndInf Libs.Analysis.SequentialAccumulationPoints Notations Tactics