Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

The quasipolynomial approximation bound

Lax263307.QPTASRuntime · concepts/Lax263307/QPTASRuntime.lean · lax-263307

definition

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

    Definition

    For fixed positive integers c,dc,d, the running-time bound is

    2c(⌈1/ε⌉(1+⌊log⁡2(n+2)⌋))d+c(ℓ+1)d.2^{c(\lceil1/\varepsilon\rceil(1+\lfloor\log_2(n+2)\rfloor))^d} +c(\ell+1)^d.

    Here nn is the graph order, ε\varepsilon is the requested accuracy, and ℓ\ell is the binary length of the rational weights and accuracy.

    Concept map
    1 concept; 2 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Mathlib.Data.Rat.Floor
    2import Mathlib.Data.Nat.Log
    3
    4/-!
    5---
    6title: The quasipolynomial approximation bound
    7type: definition
    8---
    9For fixed positive integers c,dc,d, the running-time bound is
    102c(⌈1/ε⌉(1+⌊log⁡2(n+2)⌋))d+c(ℓ+1)d.2^{c(\lceil1/\varepsilon\rceil(1+\lfloor\log_2(n+2)\rfloor))^d} +c(\ell+1)^d.
    11
    12Here nn is the graph order, ε\varepsilon is the requested accuracy, and
    13ℓ\ell is the binary length of the rational weights and accuracy.
    14
    15# Formalization notes
    16
    17The natural-number formula includes small and empty graphs. The constants
    18are fixed for the graph class before the input is supplied. Polynomial
    19overheads can be absorbed by increasing them, while preserving the
    20additive polynomial dependence on ℓ\ell.
    21-/
    22
    23namespace Lax263307.QPTASRuntime
    24
    25/-- The explicit time and sufficient word-width bound used by `HasQPTAS`. -/
    26def timeBound (c d n ℓ : ℕ) (ε : ℚ) : ℕ :=
    27 2 ^ (c * (⌈ε⁻¹⌉₊ * (Nat.log2 (n + 2) + 1)) ^ d) + c * (ℓ + 1) ^ d
    28
    29end Lax263307.QPTASRuntime
    30
    Formalization notes

    The natural-number formula includes small and empty graphs. The constants are fixed for the graph class before the input is supplied. Polynomial overheads can be absorbed by increasing them, while preserving the additive polynomial dependence on ℓ\ell.

    Builds on

    none

    Used by
    From Mathlib

    Discussion

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

    Loading discussion…