Lax Lean Archive

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

Exponential bound for the raw intersection exception

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

    A fixed-size kernel certificate describes any large collection of common primal images. The reference image cap and a joint density bound give an explicit exceptional probability after paying the coefficient count.

    Concept map
    22 concepts; 1 descendant hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

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

    1 capped_intersection_bound proven

    2 exists_intersection_scale proven

    3 exists_paper_intersection_scale proven

    4 intersection_kernel_bound proven

    5 reference_kernel_bound proven

    Lean source view on GitHub

    1import Lax342547.ImageScale
    2import Lax342547.TensorIntersections
    3import Lax342547.KernelWitness
    4
    5/-!
    6---
    7title: Exponential bound for the raw intersection exception
    8type: lemma
    9---
    10A fixed-size kernel certificate describes any large collection of common
    11primal images. The reference image cap and a joint density bound give an
    12explicit exceptional probability after paying the coefficient count.
    13-/
    14
    15namespace Lax342547.RawIntersections
    16
    17open Lax342547.MomentSpace Lax342547.RawFrames Lax342547.FrameSymmetry
    18open Lax342547.ProductImages Lax342547.TensorIntersections
    19open scoped ENNReal
    20
    21variable {Comp B H N : Type} [Fintype Comp] [Fintype B] [Fintype H] [Fintype N]
    22
    23def jointPlus {E : Matrix B B Binary} (o : Fin 2 → Comp → Frame B H N E) (e : Comp) :
    24 Matrix N (Fin 2 × (B ⊕ H)) Binary := jointMatrix (fun i => (plus (o i e)).val)
    25
    26noncomputable def intersectionDimension {E : Matrix B B Binary}
    27 (o : Fin 2 → Comp → Frame B H N E) : ℕ :=
    28 ∑ e, Module.finrank Binary (intersectionSpace (o 0 e).P (o 1 e).P)
    29
    30axiom intersection_kernel_bound {E : Matrix B B Binary}
    31 (o : Fin 2 → Comp → Frame B H N E) :
    32 intersectionDimension o ≤ ∑ e, Module.finrank Binary (LinearMap.ker (jointPlus o e).mulVecLin)
    33
    34axiom reference_kernel_bound
    35 [DecidableEq Comp] [DecidableEq B] [DecidableEq H] [DecidableEq N]
    36 {E : Matrix B B Binary} [Nonempty (Frame B H N E)]
    37 (q : ℕ) (hq : 1 ≤ q)
    38 (hN : 2 * (Fintype.card B + Fintype.card H) + 1 ≤ Fintype.card N)
    39 (hp : (4 : ℝ) * (Fintype.card B + Fintype.card H : ℕ) ≤ (1 / 4 : ℝ) * Fintype.card N)
    40 (hc : (8 : ℝ) * Fintype.card Comp ≤ (1 / 4 : ℝ) * Fintype.card N) :
    41 (PMF.uniformOfFintype (Fin 2 → Comp → Frame B H N E)).toOuterMeasure
    42 {o | q ≤ intersectionDimension o} ≤
    43 (2 : ℝ≥0∞) ^ (Fintype.card Comp * (2 * (Fintype.card B + Fintype.card H)) * q) *
    44 (2 : ℝ≥0∞) ^ (-((3 / 4 : ℝ) * q * Fintype.card N))
    45
    46axiom capped_intersection_bound
    47 [DecidableEq Comp] [DecidableEq B] [DecidableEq H] [DecidableEq N]
    48 {E : Matrix B B Binary} [Nonempty (Frame B H N E)]
    49 (D : ℕ) (hD : 1 ≤ D)
    50 (hN : 2 * (Fintype.card B + Fintype.card H) + 1 ≤ Fintype.card N)
    51 (hp : (4 : ℝ) * (Fintype.card B + Fintype.card H : ℕ) ≤ (1 / 4 : ℝ) * Fintype.card N)
    52 (hc : (8 : ℝ) * Fintype.card Comp ≤ (1 / 4 : ℝ) * Fintype.card N)
    53 (hcount : (Fintype.card Comp * (2 * (Fintype.card B + Fintype.card H)) * (2 * D) : ℕ) ≤
    54 (D : ℝ) * Fintype.card N / 4)
    55 (σ : PMF (Fin 2 → Comp → Frame B H N E))
    56 (hσ : ∀ o, σ o ≤ (2 : ℝ≥0∞) ^ (D * Fintype.card N) * PMF.uniformOfFintype _ o) :
    57 σ.toOuterMeasure {o | 2 * D < intersectionDimension o} ≤
    58 (2 : ℝ≥0∞) ^ (-((D : ℝ) * Fintype.card N / 4))
    59
    60axiom exists_intersection_scale (a b c : ℕ) :
    61 ∃ M : ℕ, ∀ n : ℕ, 1 ≤ n →
    62 2 * (a * n + b) + 1 ≤ M * n ∧
    63 (4 : ℝ) * (a * n + b : ℕ) ≤ (1 / 4 : ℝ) * (M * n : ℕ) ∧
    64 (8 : ℝ) * c ≤ (1 / 4 : ℝ) * (M * n : ℕ) ∧
    65 ∀ D : ℕ, (c * (2 * (a * n + b)) * (2 * D) : ℕ) ≤ (D : ℝ) * (M * n : ℕ) / 4
    66
    67axiom exists_paper_intersection_scale (pStar g h c : ℕ) :
    68 ∃ M : ℕ, ∀ n : ℕ, 1 ≤ n →
    69 2 * (pStar * (1 + (g * g + 3) * n) + h) + 1 ≤ M * n ∧
    70 (4 : ℝ) * (pStar * (1 + (g * g + 3) * n) + h : ℕ) ≤ (1 / 4 : ℝ) * (M * n : ℕ) ∧
    71 (8 : ℝ) * c ≤ (1 / 4 : ℝ) * (M * n : ℕ) ∧
    72 ∀ D : ℕ, (c * (2 * (pStar * (1 + (g * g + 3) * n) + h)) * (2 * D) : ℕ) ≤
    73 (D : ℝ) * (M * n : ℕ) / 4
    74
    75end Lax342547.RawIntersections
    76
    Show ProofShow ProofShow ProofShow ProofShow 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…