David, > On 1 Nov 2019, at 16:13, David Topham <[email protected]> wrote: > > Ok, I can work within integers for awhile! I was trying to use the general > form of the geometric progression that may involve fractions, but I can > explore whole numbers more first.
As an aside from what Roger has been trying to help with, you may also like to look at the treatment of sequences and series in the document wrk066.doc in the mathematical case studies that deals with some basic analysis. Sequences are modelled as functions ℕ → ℝ. The following function is defined to convert a sequence s into the series comprising the sequence of partial sums s_0 + s_1 + … + s_n. ⓈHOLCONST │ ⦏Sigma⦎ : (ℕ → ℝ) → (ℕ → ℝ) ├────── │ (∀s⦁ Sigma s 0 = ℕℝ 0) │ ∧ (∀s n⦁ Sigma s (n+1) = Sigma s n + s n) ■ In a similar vein, a function that maps a sequence of coefficients to the corresponding power series is defined as follows: ⓈHOLCONST │ ⦏PowerSeries⦎ : (ℕ → ℝ) → (ℕ → ℝ → ℝ) ├────── │ ∀s n⦁ PowerSeries s n = PolyEval (s To n) ■ where s To n is the list comprising the first n elements of the sequence s and PolyEval maps a list of coefficients to the corresponding polynomial function: ⓈHOLCONST │ ⦏PolyEval⦎ : ℝ LIST → (ℝ → ℝ) ├────── │ (∀x⦁ PolyEval [] x = ℕℝ 0) │∧ (∀c l x⦁ PolyEval (Cons c l) x = c + x * PolyEval l x) ■ When you are reasoning about these things, you can do induction over the index of a sequence, because that’s a natural number. The theory includes the usual results on geometric series: :) geometric_sum_thm; val it = ⊢ ∀ n x⦁ ¬ x = 1. ⇒ Sigma (𝜆 m⦁ x ^ m) (n + 1) = (1. - x ^ (n + 1)) / (1. - x): THM :) geometric_series_thm; val it = ⊢ ∀ x⦁ ~ 1. < x ∧ x < 1. ⇒ (𝜆 n⦁ PowerSeries (𝜆 m⦁ 1.) n x) -> 1. / (1. - x): THM Regards, Rob _______________________________________________ Proofpower mailing list [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
