Lax Lean Archive

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

Peeling with bounded new rank and normalized leaf laws

Lax342547.BoundedPeeling · concepts/Lax342547/BoundedPeeling.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

    Lemma

    The finite partition construction is quantitative under an absolute reference image cap. It preserves initial pins, bounds only the added rank, and records both conditional image probabilities and density costs.

    Concept map
    7 concepts; 4 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax342547.LeafPartition
    2import Lax342547.PeelingBudget
    3import Lax342547.Conditioning
    4
    5/-!
    6---
    7title: Peeling with bounded new rank and normalized leaf laws
    8type: lemma
    9---
    10The finite partition construction is quantitative under an absolute
    11reference image cap. It preserves initial pins, bounds only the added
    12rank, and records both conditional image probabilities and density costs.
    13-/
    14
    15namespace Lax342547.BoundedPeeling
    16
    17open Lax342547.MomentSpace Lax342547.ExactPins Lax342547.LeafPartition
    18open scoped ENNReal
    19
    20def LawBound {Ω Axis I N : Type} [Fintype Axis] (p μ : PMF Ω)
    21 (A : Ω → Axis → (I → Binary) →ₗ[Binary] (N → Binary))
    22 (P : Pin Axis I N) (S : Set Ω) (α c : ℝ≥0∞) : Prop :=
    23 ∃ hS : ∃ o ∈ S, o ∈ p.support,
    24 (∀ Q : Pin Axis I N, 1 ≤ P.relativeRank Q →
    25 (p.filter S hS).toOuterMeasure (Q.event A) ≤ α ^ (P.relativeRank Q)) ∧
    26 (∀ o, (p.filter S hS) o ≤ c * μ o) ∧
    27 ∀ o, p.toOuterMeasure S * (p.filter S hS) o = S.indicator p o
    28
    29axiom bounded_partition {Ω Axis I N : Type}
    30 [Fintype Ω] [DecidableEq Ω] [Fintype Axis] [Fintype I] [Fintype N]
    31 (p μ : PMF Ω) (A : Ω → Axis → (I → Binary) →ₗ[Binary] (N → Binary))
    32 (P₀ : Pin Axis I N) (R : Finset Ω) (hR : (R : Set Ω) ⊆ P₀.event A)
    33 (D ζ ε : ℝ) (n K : ℕ) (hn : 0 < n)
    34 (hζ : 0 < ζ) (hζ₁ : ζ ≤ 1) (hε : ε ≤ ζ / 4) (hK : 4 * (D + 1) / ζ ≤ K)
    35 (hdensity : ∀ o, p o ≤ (2 : ℝ≥0∞) ^ (D * n) * μ o)
    36 (hreference : ∀ P : Pin Axis I N,
    37 μ.toOuterMeasure (P.event A) ≤ (2 : ℝ≥0∞) ^ (-((1 - ε) * P.rank * n))) :
    38 ∃ L : Finset (Finset Ω × Pin Axis I N),
    39 Partition p A P₀ R ((2 : ℝ≥0∞) ^ (-(ζ * n))) ((2 : ℝ≥0∞) ^ (-((1 - ζ) * n))) L ∧
    40 ∀ z ∈ L, z.2.rank - P₀.rank ≤ K ∧
    41 LawBound p μ A z.2 z.1 ((2 : ℝ≥0∞) ^ (-((1 - ζ) * n)))
    42 ((2 : ℝ≥0∞) ^ ((D + K + 1) * n))
    43
    44end Lax342547.BoundedPeeling
    45
    Show Proof
    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…