From 14146b09b6a076984d4f7b96f308312d2b98ee8a Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Mon, 5 Oct 2026 16:42:57 -0400 Subject: [PATCH 1/3] feat(Foundations): define polynomial growth and relate it to big-O --- Cslib.lean | 1 + .../Foundations/Data/Nat/PolynomialBound.lean | 76 +++++++++++++++++++ 2 files changed, 77 insertions(+) create mode 100644 Cslib/Foundations/Data/Nat/PolynomialBound.lean diff --git a/Cslib.lean b/Cslib.lean index 5cfc781da..327144257 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -128,6 +128,7 @@ public import Cslib.Foundations.Data.HasFresh public import Cslib.Foundations.Data.List.IsChainFromTo public import Cslib.Foundations.Data.Nat.Asymptotics public import Cslib.Foundations.Data.Nat.Factorial +public import Cslib.Foundations.Data.Nat.PolynomialBound public import Cslib.Foundations.Data.Nat.Segment public import Cslib.Foundations.Data.OmegaSequence.Defs public import Cslib.Foundations.Data.OmegaSequence.Flatten diff --git a/Cslib/Foundations/Data/Nat/PolynomialBound.lean b/Cslib/Foundations/Data/Nat/PolynomialBound.lean new file mode 100644 index 000000000..56c0ff670 --- /dev/null +++ b/Cslib/Foundations/Data/Nat/PolynomialBound.lean @@ -0,0 +1,76 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module + +public import Cslib.Init +public import Mathlib.Analysis.Asymptotics.Lemmas +import Mathlib.Algebra.Order.Archimedean.Real.Basic + +/-! +# Polynomial bounds on natural-valued functions + +`PolynomiallyBounded f` means that `f n ≤ n ^ d` eventually, for some fixed degree `d`. +This is equivalent to a real-valued `IsBigO` bound and to a bound `c * (n + 1) ^ d` +at every input. It is a growth condition and does not assert computability. +-/ + +@[expose] public section + +namespace Cslib + +open Asymptotics Filter + +/-- A function is polynomially bounded if a fixed power eventually bounds its values. -/ +def PolynomiallyBounded (f : ℕ → ℕ) : Prop := + ∃ d : ℕ, ∀ᶠ n in atTop, f n ≤ n ^ d + +/-- Polynomial growth is equivalent to a big-O bound after casting to the reals. -/ +theorem polynomiallyBounded_iff_isBigO {f : ℕ → ℕ} : + PolynomiallyBounded f ↔ + ∃ d : ℕ, (fun n => (f n : ℝ)) =O[atTop] (fun n => (n : ℝ) ^ d) := by + constructor + · rintro ⟨d, hd⟩ + refine ⟨d, .of_bound' ?_⟩ + filter_upwards [hd] with n hn + simpa using (show (f n : ℝ) ≤ (n : ℝ) ^ d by exact_mod_cast hn) + · rintro ⟨d, hd⟩ + obtain ⟨c, _, hc⟩ := hd.exists_pos + refine ⟨d + 1, ?_⟩ + filter_upwards [hc.bound, eventually_ge_atTop ⌈c⌉₊] with n hn hcn + have hc' : c ≤ (n : ℝ) := (Nat.le_ceil c).trans (by exact_mod_cast hcn) + have hn' : (f n : ℝ) ≤ c * (n : ℝ) ^ d := by simpa using hn + have hpow : c * (n : ℝ) ^ d ≤ (n : ℝ) ^ (d + 1) := by + rw [pow_succ'] + exact mul_le_mul_of_nonneg_right hc' (pow_nonneg (Nat.cast_nonneg n) d) + exact_mod_cast hn'.trans hpow + +/-- A polynomial bound can absorb every finite prefix into its constant factor. -/ +theorem polynomiallyBounded_iff_le {f : ℕ → ℕ} : + PolynomiallyBounded f ↔ ∃ c d : ℕ, ∀ n, f n ≤ c * (n + 1) ^ d := by + constructor + · intro hf + obtain ⟨d, hd⟩ := polynomiallyBounded_iff_isBigO.mp hf + have hshift : (fun n => (f n : ℝ)) =O[atTop] (fun n => ((n + 1 : ℕ) : ℝ) ^ d) := + hd.trans (.of_bound' (Eventually.of_forall fun n => by + simp only [norm_pow, Real.norm_natCast] + exact_mod_cast Nat.pow_le_pow_left (Nat.le_succ n) d)) + obtain ⟨c, _, hc⟩ := bound_of_isBigO_nat_atTop hshift + refine ⟨⌈c⌉₊, d, fun n => ?_⟩ + have hn : (f n : ℝ) ≤ c * ((n + 1 : ℕ) : ℝ) ^ d := by + simpa only [norm_pow, Real.norm_natCast] using hc (x := n) (by positivity) + exact_mod_cast hn.trans (mul_le_mul_of_nonneg_right (Nat.le_ceil c) (by positivity)) + · rintro ⟨c, d, hf⟩ + refine ⟨d + 1, ?_⟩ + filter_upwards [eventually_ge_atTop 1, eventually_ge_atTop (c * 2 ^ d)] with n hn hc + calc + f n ≤ c * (n + 1) ^ d := hf n + _ ≤ c * (2 * n) ^ d := by gcongr; lia + _ = (c * 2 ^ d) * n ^ d := by rw [mul_pow, mul_assoc] + _ ≤ n * n ^ d := Nat.mul_le_mul_right _ hc + _ = n ^ (d + 1) := (pow_succ' n d).symm + +end Cslib From a1bb52268a074b4315a9477ed9363691b6daab71 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Mon, 5 Oct 2026 18:50:06 -0400 Subject: [PATCH 2/3] Update Cslib/Foundations/Data/Nat/PolynomialBound.lean Co-authored-by: Thomas Krishna Waring <51426330+thomaskwaring@users.noreply.github.com> --- Cslib/Foundations/Data/Nat/PolynomialBound.lean | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/Cslib/Foundations/Data/Nat/PolynomialBound.lean b/Cslib/Foundations/Data/Nat/PolynomialBound.lean index 56c0ff670..4d61998af 100644 --- a/Cslib/Foundations/Data/Nat/PolynomialBound.lean +++ b/Cslib/Foundations/Data/Nat/PolynomialBound.lean @@ -41,12 +41,9 @@ theorem polynomiallyBounded_iff_isBigO {f : ℕ → ℕ} : obtain ⟨c, _, hc⟩ := hd.exists_pos refine ⟨d + 1, ?_⟩ filter_upwards [hc.bound, eventually_ge_atTop ⌈c⌉₊] with n hn hcn - have hc' : c ≤ (n : ℝ) := (Nat.le_ceil c).trans (by exact_mod_cast hcn) - have hn' : (f n : ℝ) ≤ c * (n : ℝ) ^ d := by simpa using hn - have hpow : c * (n : ℝ) ^ d ≤ (n : ℝ) ^ (d + 1) := by - rw [pow_succ'] - exact mul_le_mul_of_nonneg_right hc' (pow_nonneg (Nat.cast_nonneg n) d) - exact_mod_cast hn'.trans hpow + grw [Nat.le_ceil c, Real.norm_natCast, norm_pow, Real.norm_natCast, hcn] at hn + have hn' : f n ≤ n * n ^ d := by exact_mod_cast hn + rwa [pow_succ'] /-- A polynomial bound can absorb every finite prefix into its constant factor. -/ theorem polynomiallyBounded_iff_le {f : ℕ → ℕ} : From 0cb778d4a020b5c9e8d464957f5b12f77bf5bfef Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Mon, 5 Oct 2026 18:50:14 -0400 Subject: [PATCH 3/3] Update Cslib/Foundations/Data/Nat/PolynomialBound.lean Co-authored-by: Thomas Krishna Waring <51426330+thomaskwaring@users.noreply.github.com> --- .../Foundations/Data/Nat/PolynomialBound.lean | 19 ++++++++----------- 1 file changed, 8 insertions(+), 11 deletions(-) diff --git a/Cslib/Foundations/Data/Nat/PolynomialBound.lean b/Cslib/Foundations/Data/Nat/PolynomialBound.lean index 4d61998af..b80556046 100644 --- a/Cslib/Foundations/Data/Nat/PolynomialBound.lean +++ b/Cslib/Foundations/Data/Nat/PolynomialBound.lean @@ -49,17 +49,14 @@ theorem polynomiallyBounded_iff_isBigO {f : ℕ → ℕ} : theorem polynomiallyBounded_iff_le {f : ℕ → ℕ} : PolynomiallyBounded f ↔ ∃ c d : ℕ, ∀ n, f n ≤ c * (n + 1) ^ d := by constructor - · intro hf - obtain ⟨d, hd⟩ := polynomiallyBounded_iff_isBigO.mp hf - have hshift : (fun n => (f n : ℝ)) =O[atTop] (fun n => ((n + 1 : ℕ) : ℝ) ^ d) := - hd.trans (.of_bound' (Eventually.of_forall fun n => by - simp only [norm_pow, Real.norm_natCast] - exact_mod_cast Nat.pow_le_pow_left (Nat.le_succ n) d)) - obtain ⟨c, _, hc⟩ := bound_of_isBigO_nat_atTop hshift - refine ⟨⌈c⌉₊, d, fun n => ?_⟩ - have hn : (f n : ℝ) ≤ c * ((n + 1 : ℕ) : ℝ) ^ d := by - simpa only [norm_pow, Real.norm_natCast] using hc (x := n) (by positivity) - exact_mod_cast hn.trans (mul_le_mul_of_nonneg_right (Nat.le_ceil c) (by positivity)) + · simp_rw [PolynomiallyBounded, EventuallyLE, eventually_atTop] + intro ⟨d, m, h⟩ + have ⟨c, hc⟩ := (Set.finite_Iio m).image f |>.exists_le + use c + 1, d + intro n + obtain (hn | hn) := n.lt_or_ge m + · grw [hc _ ⟨n, hn, rfl⟩, c.le_add_right 1, ← d.one_le_pow' n, mul_one] + · grw [h n hn, n.le_add_right 1, ← Nat.le_add_left 1 c, one_mul] · rintro ⟨c, d, hf⟩ refine ⟨d + 1, ?_⟩ filter_upwards [eventually_ge_atTop 1, eventually_ge_atTop (c * 2 ^ d)] with n hn hc