Lax Lean Archive

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

Geometric contraction with an additive rounding error

Lax235315.ContractionRecurrence · concepts/Lax235315/ContractionRecurrence.lean · lax-235315

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

    Lemma

    If the size after a round is at most half the preceding size plus q, then after i rounds it is at most the initial size divided by 2^i, plus 2q. This accommodates the ceiling in Algorithm 1's sample size, with q = c².

    Concept map
    1 concept
    100%
    Proven claimThis concept
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Mathlib.Data.Nat.Log
    2
    3/-!
    4---
    5title: Geometric contraction with an additive rounding error
    6type: lemma
    7---
    8If the size after a round is at most half the preceding size plus q, then
    9after i rounds it is at most the initial size divided by 2^i, plus 2q.
    10This accommodates the ceiling in Algorithm 1's sample size, with q = c².
    11
    12# Formalization notes
    13
    14All divisions are natural-number divisions. This arithmetic statement is
    15separate from proving that the actual twin-partition rounds satisfy its
    16hypothesis. The later stopping proof must also use the algorithm's threshold
    17and handle input sizes zero and one.
    18-/
    19
    20namespace Lax235315.ContractionRecurrence
    21
    22/-- Iterated halving accumulates less than twice the per-round additive error. -/
    23axiom size_after_rounds (a : ℕ → ℕ) (q : ℕ)
    24 (step : ∀ i, a (i + 1) ≤ a i / 2 + q) (i : ℕ) :
    25 a i ≤ a 0 / 2 ^ i + 2 * q
    26
    27end Lax235315.ContractionRecurrence
    28
    Show Proof
    Formalization notes

    All divisions are natural-number divisions. This arithmetic statement is separate from proving that the actual twin-partition rounds satisfy its hypothesis. The later stopping proof must also use the algorithm's threshold and handle input sizes zero and one.

    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…