CumulusStarter
Examples using the public real-mathematics entry point
1-- Examples using the public real-mathematics entry point.2-- Copyright (c) 2026 Grant Passmore.3-- Released under the Apache License 2.0. See LICENSE in the repository root.4-- Authors: Grant Passmore56module CumulusStarter7import Grace.Cumulus.Real89theorem constant_integral (A B C : Real)10 requires ordered : A ≤ B11 shows ∫[A, B] constantRealFunction(C) = C * (B - A)12proof13 exact riemannIntegral.constant with ordered1415theorem integral_notation (f : Set) (A B : Real)16 shows ∫[A, B] f = riemannIntegral(f, A, B)17proof18 rfl1920theorem integral_notation_in_expression (f : Set) (A B : Real)21 shows (∫[A, B] f) + (1:R) = (riemannIntegral(f, A, B):R) + (1:R)22proof23 rfl2425theorem finite_sum_add (u v : Set, n : Nat)26 requires uReal : RealSequence(u)27 requires vReal : RealSequence(v)28 shows realPartialSum(addSequence(u, v), n) =29 (realPartialSum(u, n):R) + (realPartialSum(v, n):R)30proof31 exact realPartialSum.add with uReal, vReal3233theorem finite_sum_sub (u v : Set, n : Nat)34 requires uReal : RealSequence(u)35 requires vReal : RealSequence(v)36 shows realPartialSum(subSequence(u, v), n) =37 (realPartialSum(u, n):R) - (realPartialSum(v, n):R)38proof39 exact realPartialSum.sub with uReal, vReal4041theorem finite_sum_split (u : Set, m n : Nat)42 requires sequence : RealSequence(u)43 shows realPartialSum(u, add(m, n)) =44 (realPartialSum(u, m):R) + realPartialSum(shiftedRealSequence(u, m), n)45proof46 exact realPartialSum.split_at with sequence4748theorem geometric_series (X : Real, n : Nat)49 shows ((1:R) - X) * (realPartialSum(geometricTerms(X), n):R) =50 (1:R) - X ^ n51proof52 exact realPartialSum.geometric with assumption, assumption5354theorem geometric_series_quotient (X : Real, n : Nat)55 requires nonzero : ((1:R) - X) ≠ (0:R)56 shows realPartialSum(geometricTerms(X), n) =57 ((1:R) - X ^ n) / ((1:R) - X)58proof59 exact realPartialSum.geometric_quotient with nonzero6061theorem telescoping_sum (u : Set, n : Nat)62 requires sequence : RealSequence(u)63 shows realPartialSum(adjacentDifferences(u), n) = (u[n]:R) - (u[0]:R)64proof65 exact realPartialSum.telescoping with sequence6667theorem adjacent_product_rule (u v : Set, n : Nat)68 requires sequenceU : RealSequence(u)69 requires sequenceV : RealSequence(v)70 shows adjacentDifferences(mulSequence(u, v))[n] =71 (u[succ(n)]:R) * (adjacentDifferences(v)[n]:R) +72 (v[n]:R) * (adjacentDifferences(u)[n]:R)73proof74 exact adjacentDifferences.product with sequenceU, sequenceV7576theorem finite_product_telescoping (u v : Set, n : Nat)77 requires sequenceU : RealSequence(u)78 requires sequenceV : RealSequence(v)79 shows (realPartialSum(forwardProductIncrements(u, v), n):R) +80 (realPartialSum(backwardProductIncrements(u, v), n):R) =81 (u[n]:R) * (v[n]:R) - (u[0]:R) * (v[0]:R)82proof83 exact realPartialSum.product_telescoping with sequenceU, sequenceV8485theorem abel_summation (u v : Set, n : Nat)86 requires sequenceU : RealSequence(u)87 requires sequenceV : RealSequence(v)88 shows realPartialSum(mulSequence(u, v), n) =89 (realPartialSum(u, n):R) * (v[n]:R) -90 (realPartialSum(forwardProductIncrements(prefixSums(u), v), n):R)91proof92 exact realPartialSum.abel with sequenceU, sequenceV9394theorem polynomial_add (u v : Set, n : Nat, X : Real)95 requires uReal : RealSequence(u)96 requires vReal : RealSequence(v)97 shows polynomialEval(addSequence(u, v), n, X) =98 (polynomialEval(u, n, X):R) + (polynomialEval(v, n, X):R)99proof100 exact polynomialEval.add with uReal, vReal101102theorem polynomial_same_prefix (u v : Set, n : Nat, X : Real)103 requires uReal : RealSequence(u)104 requires vReal : RealSequence(v)105 requires equal : ∀ k ∈ ℕ, k < n → u[k] = v[k]106 shows polynomialEval(u, n, X) = polynomialEval(v, n, X)107proof108 exact polynomialEval.eq_prefix with uReal, vReal, equal109110theorem polynomial_scale (coeff : Set, n : Nat, X C : Real)111 requires coefficients : RealSequence(coeff)112 shows polynomialEval(mulSequence(constantSequence(C), coeff), n, X) =113 C * (polynomialEval(coeff, n, X):R)114proof115 exact polynomialEval.scale with coefficients116117theorem polynomial_sub (u v : Set, n : Nat, X : Real)118 requires uReal : RealSequence(u)119 requires vReal : RealSequence(v)120 shows polynomialEval(subSequence(u, v), n, X) =121 (polynomialEval(u, n, X):R) - (polynomialEval(v, n, X):R)122proof123 exact polynomialEval.sub with uReal, vReal124125theorem polynomial_at_one (coeff : Set, n : Nat)126 requires coefficients : RealSequence(coeff)127 shows polynomialEval(coeff, n, realOne) = realPartialSum(coeff, n)128proof129 exact polynomialEval.at_one with coefficients130131theorem polynomial_as_sum (coeff : Set, n : Nat, X : Real)132 requires coefficients : RealSequence(coeff)133 shows polynomialEval(coeff, n, X) = realPartialSum(polynomialTerms(coeff, X), n)134proof135 exact polynomialEval.as_sum with coefficients136137theorem polynomial_geometric (X : Real, n : Nat)138 shows ((1:R) - X) * (polynomialEval(constantSequence(realOne), n, X):R) =139 (1:R) - X ^ n140proof141 exact polynomialEval.geometric_identity with assumption, assumption142143theorem affine_polynomial (coeff : Set, X : Real)144 requires coefficients : RealSequence(coeff)145 shows polynomialEval(coeff, succ(succ(0)), X) =146 (coeff[0]:R) + (coeff[succ(0)]:R) * X147proof148 exact polynomialEval.linear with coefficients149150theorem polynomial_at_zero (coeff : Set, n : Nat)151 requires coefficients : RealSequence(coeff)152 shows polynomialEval(coeff, succ(n), realZero) = coeff[0]153proof154 exact polynomialEval.at_zero_succ with coefficients155156theorem quadratic_polynomial (coeff : Set, X : Real)157 requires coefficients : RealSequence(coeff)158 shows polynomialEval(coeff, succ(succ(succ(0))), X) =159 ((coeff[0]:R) + (coeff[succ(0)]:R) * X) +160 (coeff[succ(succ(0))]:R) * (X * X)161proof162 exact polynomialEval.quadratic with coefficients163164theorem identity_integral (A B : Real)165 requires ordered : A ≤ B166 shows riemannIntegral(constantRealFunction(realOne), A, B) = B - A167proof168 exact FTC.integral_one with ordered169