proposition: Lemma is_bounded_equivalence : ∀ (a : ℕ → ℝ), is_bounded a ⇔ is_bounded_equivalent a.
proof: Proof. Take a : (ℕ → ℝ). We show both directions. - We need to show that (is_bounded a ⇨ is_bounded_equivalent a). Assume that (is_bounded a). It holds that (there exists q : R, there exists M1 : R, M1 > 0 ∧ (for all n : ℕ, | a n - q | ≤ M1)). Obtain such a q. It holds that (there exists M1 : R, M1 > 0 ∧ (for all n : ℕ, | a n - q | ≤ M1)). Obtain such an M1. It holds that (M1 > 0 ∧ (for all n : ℕ, | a n - q | ≤ M1)) (i). Because (i) both (M1 > 0) and (for all n : ℕ, | a n - q | ≤ M1). We need to show that ( there exists M : ℝ , M > 0 ∧ (for all n : ℕ, | a n | ≤ M)). Choose M := (M1 + |q|). We show both statements. + We need to show that (M > 0). It holds that (0 ≤ |q|). It suffices to show that (0 <= M). We conclude that (& 0 <= (M1 + |q|) = M). + We need to show that ( for all n : ℕ, | a n | ≤ M ). Take n : ℕ. By Rabs_triang it holds that (|a n - q + q| ≤ |a n - q| + |q|). We conclude that (& |a n| = |a n - q + q| <= (|a n - q| + |q|) <= (M1 + |q|) = M). - We need to show that ( is_bounded_equivalent a ⇨ is_bounded a). Assume that (there exists M1 : ℝ, M1 > 0 ∧ ∀ n : ℕ, |a n| ≤ M1). Obtain such an M1. It holds that (M1 > 0 ∧ ∀ n : ℕ, |a n| ≤ M1) (i). Because (i) both (M1 > 0) and (for all n : ℕ, | a n | ≤ M1) hold. We need to show that ( there exists q M : ℝ , M > 0 ∧ (for all n : ℕ, | a n - q | ≤ M) ). Choose q := 0. Choose M := M1. We show both statements. + We need to show that (M > 0). It follows that (M > 0). + We need to show that ( for all n : ℕ, | a n - q | ≤ M ). Take n : ℕ. We conclude that (& |a n - q| = |a n| <= M). Qed.
imports: Coq.Reals.Reals Lra Classical Classical_Pred_Type ClassicalChoice Tactics Automation Libs.Reals Notations