Lax Lean Archive

Computable Bounds

Lax496464.WH_A6_ComputableBounds · concepts/Lax496464/WH_A6_ComputableBounds.lean · lax-496464

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    The time factor and the parameter bound of an fpt-reduction must be computable. The bounds that occur in practice are built from constants and the parameter by sums, products, powers and exponentials, and all of them are computable. Every computable f ⁣:N→Nf\colon\mathbb N\to\mathbb N is bounded by the computable nondecreasing function k↦∑i≤kf(i)k \mapsto \sum_{i \le k} f(i), which is what allows bounds to be composed.

    Concept map
    1 concept
    100%
    Proven claimThis concept
    Evidence

    This concept declares 6 statements. Each proof establishes one of them relative to its assumptions.

    1 computable_add proven

    2 computable_exp proven

    3 computable_mul proven

    4 computable_polynomial proven

    5 computable_pow proven

    6 exists_monotone_bound proven

    Lean source view on GitHub

    1import Mathlib.Computability.Partrec
    2import Mathlib.Algebra.Polynomial.Eval.Defs
    3
    4/-!
    5---
    6title: Computable Bounds
    7type: theorem
    8---
    9The time factor and the parameter bound of an fpt-reduction must be computable. The bounds that
    10occur in practice are built from constants and the parameter by sums, products, powers and
    11exponentials, and all of them are computable. Every computable f ⁣:N→Nf\colon\mathbb N\to\mathbb N is
    12bounded by the computable nondecreasing function k↦∑i≤kf(i)k \mapsto \sum_{i \le k} f(i), which is what
    13allows bounds to be composed.
    14
    15# Formalization Notes
    16
    17Computability is Mathlib's `Computable`. Together with `Computable.const`, `Computable.id` and
    18`Computable.comp`, these statements show a bound such as (k+1)2(k+1)^2 or 2k⋅k2^k \cdot k computable by
    19combining them.
    20-/
    21
    22namespace Lax496464.WH_A6_ComputableBounds
    23
    24/-- Sums of computable functions are computable. -/
    25axiom computable_add {f g : ℕ → ℕ} :
    26 Computable f → Computable g → Computable fun k => f k + g k
    27
    28/-- Products of computable functions are computable. -/
    29axiom computable_mul {f g : ℕ → ℕ} :
    30 Computable f → Computable g → Computable fun k => f k * g k
    31
    32/-- Fixed powers of computable functions are computable. -/
    33axiom computable_pow {f : ℕ → ℕ} (e : ℕ) : Computable f → Computable fun k => f k ^ e
    34
    35/-- Exponentials `b ^ f(k)` of computable functions are computable. -/
    36axiom computable_exp (b : ℕ) {f : ℕ → ℕ} : Computable f → Computable fun k => b ^ f k
    37
    38/-- Polynomials with natural coefficients are computable. -/
    39axiom computable_polynomial (p : Polynomial ℕ) : Computable fun k => p.eval k
    40
    41/-- Every computable function is bounded by a computable nondecreasing function. -/
    42axiom exists_monotone_bound {f : ℕ → ℕ} :
    43 Computable f → ∃ g : ℕ → ℕ, Computable g ∧ Monotone g ∧ ∀ k, f k ≤ g k
    44
    45end Lax496464.WH_A6_ComputableBounds
    46
    Show ProofShow ProofShow ProofShow ProofShow ProofShow Proof
    Formalization Notes

    Computability is Mathlib's ComputableComputable. Together with Computable.constComputable.const, Computable.idComputable.id and Computable.compComputable.comp, these statements show a bound such as (k+1)2(k+1)^2 or 2k⋅k2^k \cdot k computable by combining them.

    Builds on

    none

    Used by

    none

    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…