Lax Lean Archive

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

Rank and density budgets for exact-image peeling

Lax342547.PeelingBudget · concepts/Lax342547/PeelingBudget.lean · lax-342547

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

    Compare the retained leaf mass with its absolute reference-image cap. The comparison bounds the cumulative new rank, including a single large violating tuple, and controls the cost of normalizing the leaf law.

    Concept map
    1 concept; 5 descendants hidden
    100%
    Proven claimThis conceptRelated conceptA → B: B builds on A
    Evidence

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

    1 conservative_rank_bound proven

    2 density_cost proven

    3 rank_comparison proven

    Lean source view on GitHub

    1import Mathlib.Analysis.SpecialFunctions.Pow.NNReal
    2
    3/-!
    4---
    5title: Rank and density budgets for exact-image peeling
    6type: theorem
    7---
    8Compare the retained leaf mass with its absolute reference-image cap.
    9The comparison bounds the cumulative new rank, including a single large
    10violating tuple, and controls the cost of normalizing the leaf law.
    11-/
    12
    13namespace Lax342547.PeelingBudget
    14
    15open scoped ENNReal
    16
    17axiom rank_comparison (D ζ ε : ℝ) (N u : ℕ) (hN : 0 < N) (m : ℝ≥0∞)
    18 (hlower : (2 : ℝ≥0∞) ^ (-(ζ * N)) * ((2 : ℝ≥0∞) ^ (-((1 - ζ) * N))) ^ u < m)
    19 (hupper : m ≤ (2 : ℝ≥0∞) ^ (D * N) * ((2 : ℝ≥0∞) ^ (-((1 - ε) * N))) ^ u) :
    20 (ζ - ε) * u < D + ζ
    21
    22axiom conservative_rank_bound (D ζ ε : ℝ) (u : ℕ)
    23 (hζ : 0 < ζ) (hζ₁ : ζ ≤ 1) (hε : ε ≤ ζ / 4)
    24 (h : (ζ - ε) * u < D + ζ) : (u : ℝ) < 4 * (D + 1) / ζ
    25
    26axiom density_cost (D ζ : ℝ) (N u K : ℕ) (hζ : 0 ≤ ζ) (hζ₁ : ζ ≤ 1)
    27 (hu : u ≤ K) (m : ℝ≥0∞)
    28 (hm : (2 : ℝ≥0∞) ^ (-(ζ * N)) * ((2 : ℝ≥0∞) ^ (-((1 - ζ) * N))) ^ u ≤ m) :
    29 (2 : ℝ≥0∞) ^ (D * N) / m ≤ (2 : ℝ≥0∞) ^ ((D + K + 1) * N)
    30
    31end Lax342547.PeelingBudget
    32
    Show ProofShow ProofShow Proof
    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…