Lax Lean Archive

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

Paying the reference-image conditioning and dimension costs

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

    The finite two-endpoint cap has prefactor 16 per component and loses 2(d+h) dimensions on minus images. Both costs are paid uniformly over every positive total rank by choosing the ambient scale sufficiently large. A single scale works for every positive n and every tested rank.

    Concept map
    14 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.
    Evidence

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

    1 cost_bound proven

    2 exists_paper_scale proven

    3 exists_scale proven

    4 reference_image_cap proven

    Lean source view on GitHub

    1import Lax342547.ReferenceImages
    2import Mathlib.Analysis.SpecialFunctions.Pow.NNReal
    3
    4/-!
    5---
    6title: Paying the reference-image conditioning and dimension costs
    7type: theorem
    8---
    9The finite two-endpoint cap has prefactor 16 per component and loses
    102(d+h) dimensions on minus images. Both costs are paid uniformly over
    11every positive total rank by choosing the ambient scale sufficiently
    12large. A single scale works for every positive n and every tested rank.
    13-/
    14
    15namespace Lax342547.ImageScale
    16
    17open Lax342547.MomentSpace Lax342547.RawFrames Lax342547.ReferenceImages
    18open scoped ENNReal
    19
    20axiom cost_bound (c p N a b : ℕ) (ε : ℝ) (hε : 0 < ε)
    21 (hN : 2 * p ≤ N) (ht : 1 ≤ a + b)
    22 (hp : (4 : ℝ) * p ≤ ε * N) (hc : (8 : ℝ) * c ≤ ε * N) :
    23 (4 : ℝ≥0∞) ^ (2 * c) / 2 ^ (N * a + (N - 2 * p) * b) ≤
    24 (2 : ℝ≥0∞) ^ (-((1 - ε) * (a + b : ℕ) * N))
    25
    26axiom exists_scale (a b c : ℕ) (ε : ℝ) (hε : 0 < ε) :
    27 ∃ M : ℕ, ∀ n : ℕ, 1 ≤ n →
    28 2 * (a * n + b) + 1 ≤ M * n ∧
    29 (4 : ℝ) * (a * n + b : ℕ) ≤ ε * (M * n : ℕ) ∧
    30 (8 : ℝ) * c ≤ ε * (M * n : ℕ)
    31
    32axiom exists_paper_scale (pStar g h c : ℕ) (ε : ℝ) (hε : 0 < ε) :
    33 ∃ M : ℕ, ∀ n : ℕ, 1 ≤ n →
    34 2 * (pStar * (1 + (g * g + 3) * n) + h) + 1 ≤ M * n ∧
    35 (4 : ℝ) * (pStar * (1 + (g * g + 3) * n) + h : ℕ) ≤ ε * (M * n : ℕ) ∧
    36 (8 : ℝ) * c ≤ ε * (M * n : ℕ)
    37
    38axiom reference_image_cap {Comp B H N : Type}
    39 [Fintype Comp] [Fintype B] [Fintype H] [Fintype N]
    40 [DecidableEq Comp] [DecidableEq B] [DecidableEq H] [DecidableEq N]
    41 {K L : Comp → Type} [∀ e, Fintype (K e)] [∀ e, Fintype (L e)]
    42 {E : Matrix B B Binary} [Nonempty (Frame B H N E)]
    43 (ε : ℝ) (hε : 0 < ε)
    44 (hN : 2 * (Fintype.card B + Fintype.card H) + 1 ≤ Fintype.card N)
    45 (hp : (4 : ℝ) * (Fintype.card B + Fintype.card H : ℕ) ≤ ε * Fintype.card N)
    46 (hc : (8 : ℝ) * Fintype.card Comp ≤ ε * Fintype.card N)
    47 (C : ∀ e, Matrix (Fin 2 × (B ⊕ H)) (K e) Binary)
    48 (D : ∀ e, Matrix (Fin 2 × (B ⊕ H)) (L e) Binary)
    49 (y : ∀ e, Matrix N (K e) Binary) (z : ∀ e, Matrix N (L e) Binary)
    50 (ht : 1 ≤ (∑ e, (C e).rank) + ∑ e, (D e).rank) :
    51 (PMF.uniformOfFintype (Fin 2 → Comp → Frame B H N E)).toOuterMeasure
    52 {o | ∀ e, plusImages (C e) (fun i => o i e) = y e ∧ minusImages (D e) (fun i => o i e) = z e} ≤
    53 (2 : ℝ≥0∞) ^ (-((1 - ε) * ((∑ e, (C e).rank) + ∑ e, (D e).rank : ℕ) * Fintype.card N))
    54
    55end Lax342547.ImageScale
    56
    Show ProofShow ProofShow ProofShow Proof
    Builds on
    Used by
    From Mathlib

    Discussion

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

    Loading discussion…