proposition: Lemma sequence_ub_bds : ∀ (a : ℕ → ℝ) (i : has_ub a) (N : ℕ) (n : ℕ), (n ≥ N)%nat ⇒ a n ≤ sequence_ub a (i) N.
proof: Proof. Take a : (ℕ → ℝ). Assume that (has_ub a) (i). Take Nn, n : ℕ; such that (n ≥ Nn)%nat. We need to show that (a n ≤ lub (fun k ↦ (a (Nn + k)%nat), maj_ss a Nn (i))). We need to show that (a n ≤ (let (a0, _) := ub_to_lub (fun k ↦ (a (Nn + k)%nat), maj_ss a Nn (i)) in a0)). Define ii := (ub_to_lub (fun (k : ℕ) ↦ a (Nn +k)%nat) (maj_ss a Nn (i))). clear _defeq. Obtain such an M. It holds that (is_lub (EUn (fun (k : ℕ) ↦ a (Nn +k)%nat)) M). It holds that (Raxioms.is_upper_bound (EUn (fun k ↦ (a (Nn + k)%nat)), M) ∧ (for all b : ℝ, Raxioms.is_upper_bound (EUn (fun k ↦ (a (Nn + k)%nat)), b) ⇨ M ≤ b)) (iii). Because (iii) both (Raxioms.is_upper_bound (EUn (fun k ↦ (a (Nn + k)%nat)), M)) and (for all b : ℝ, Raxioms.is_upper_bound (EUn (fun k ↦ (a (Nn + k)%nat)), b) ⇨ M ≤ b) hold. It holds that (for all x : ℝ, EUn (fun k ↦ (a (Nn + k)%nat), x) ⇨ x ≤ M). It holds that (Nn + (n-Nn) = n)%nat. It suffices to show that (EUn (fun (k : ℕ) ↦ (a (Nn + k)%nat)) (a n)). We need to show that (there exists i : ℕ, a n = a (Nn + i)%nat). We need to show that (∃ i : ℕ, a n = a (Nn + i)%nat). Choose k := (n - Nn)%nat. We conclude that (& a n = a (Nn + n - Nn)%nat = a (Nn + k)%nat). 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