ClassicalResultsStarter

Four classical results in use: induction, root two, the mean inequality, digit sums

Open in Workbench View on GitHub

1-- Four classical results in use: induction, root two, the mean inequality, digit sums2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module ClassicalResultsStarter8import Grace.Cumulus.NumberTheory9import Grace.Cumulus.Real1011-- The principle of induction as a theorem about subsets of ℕ.12theorem naturals_in_closed_set (S : Set)13  requires base : 0 ∈ S14  requires step : ∀ n ∈ ℕ, n ∈ S → n + 1 ∈ S15  shows 5 ∈ S16proof17  have fiveNat : Nat(5) by typecheck18  have five := nat.omega.forward with fiveNat19  exact natural.induction at S with *, 5, five2021-- √2 is not 7/5, or any other ratio of naturals.22theorem root_two_not_seven_fifths23  shows √2 ≠ realNat(7) / realNat(5)24proof25  have fiveNonzero : 5 ≠ 026    intro zero27    have positive : 0 < 5 by arith28    rw zero at positive29    exact Less.irreflexive with *, positive30  exact sqrtTwo.ne_quotient at 7, 5 with *3132-- The arithmetic mean dominates the geometric mean.33theorem mean_bound (a b : Real)34  requires nonnegativeA : 0 ≤ a35  requires nonnegativeB : 0 ≤ b36  shows √(a * b) ≤ (a + b) / 237proof38  exact sqrt.le_mean at a, b with *3940-- 123 written by its digits, least significant first, and its digit sum.41theorem one_two_three42  shows digitsValue([3, 2, 1]) = 12343proof44  compute4546theorem one_two_three.digit_sum47  shows digitSum([3, 2, 1]) = 648proof49  compute5051theorem one_two_three.divisible52  shows 3 ∣ digitsValue([3, 2, 1])53proof54  have digits : 3 ∣ digitSum([3, 2, 1])55    have sum := one_two_three.digit_sum56    rw sum57    unfold Divides58    witness 259    compute60  exact digitsValue.three_divides_iff.backward at [3, 2, 1] with *61