proposition: Lemma exists_almost_lim_sup : ∀ (a : ℕ → ℝ) (i : has_ub a) (ii : has_lb (sequence_ub a (i))) (m : ℕ) (N : ℕ), ∃ k : ℕ, (N ≤ k)%nat ∧ a k > proj1_sig(_,_,lim_sup_bdd a (i) (ii)) - 1 / (INR(m) + 1).
proof: Proof. Take a : (ℕ → ℝ). Assume that (has_ub a) (i). Assume that (has_lb (sequence_ub a (i))) (ii). Take m, Nn : ℕ. By exists_almost_lim_sup_aux it holds that (∃ n : ℕ, (n ≥ Nn)%nat ∧ a n > sequence_ub a (i) Nn - 1 / (INR(m) + 1)). Obtain such an n. It holds that ((n ≥ Nn)%nat ∧ a n > sequence_ub a (i) Nn - 1 / (INR(m) + 1)) (iii). Choose k := n. We show both statements. - We need to show that (Nn ≤ k)%nat. We conclude that (Nn <= k)%nat. - We need to show that (a k > proj1_sig(_,_,lim_sup_bdd a (i) (ii)) - 1 / (m + 1)). We claim that (proj1_sig(_,_,lim_sup_bdd a (i) (ii)) ≤ sequence_ub a (i) Nn). { We need to show that (proj1_sig(_, _, decreasing_cv (sequence_ub a (i), (Wn_decreasing a (i)), (ii))) ≤ sequence_ub a (i) Nn). Define v := (decreasing_cv (sequence_ub a (i)) (Wn_decreasing a (i)) (ii)). clear _defeq0. Obtain such an l. We need to show that (l ≤ sequence_ub a (i) Nn). By Wn_decreasing it holds that (Un_decreasing (sequence_ub a (i))). By decreasing_ineq we conclude that (l <= sequence_ub a (i) Nn). } Because (iii) both (n ≥ Nn)%nat and (a n > sequence_ub a i Nn - 1 / (m + 1)) hold. It holds that (proj1_sig(_, _, lim_sup_bdd a (i) (ii)) - 1 / (m + 1) ≤ a n) (v). We need to show that (proj1_sig(_, _, lim_sup_bdd a (i) (ii)) - 1 / (m + 1) < a k). We conclude that (& proj1_sig(_, _, lim_sup_bdd a (i) (ii)) - 1 / (m + 1) < a n = a k). 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