Lax Lean Archive

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

Simultaneous binary mixer estimates for all labels and flavors

Lax342547.BinaryMixers · concepts/Lax342547/BinaryMixers.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 good events quantify over every pair of distinct selector labels and every nonzero ordered parity. Finite unions give a failure bound tending to zero with n. The rank condition is n ≤ 5r, avoiding any rounding of the paper's n/5 threshold.

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

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

    1 mixer_failure_bound proven

    2 sharp_failure_bound proven

    3 uniform_of_restrictions proven

    Lean source view on GitHub

    1import Lax342547.BinaryMixer
    2
    3/-!
    4---
    5title: Simultaneous binary mixer estimates for all labels and flavors
    6type: lemma
    7---
    8The good events quantify over every pair of distinct selector labels and
    9every nonzero ordered parity. Finite unions give a failure bound tending
    10to zero with n. The rank condition is n ≤ 5r, avoiding any rounding of
    11the paper's n/5 threshold.
    12-/
    13
    14namespace Lax342547.BinaryMixers
    15
    16open Lax342547.MomentSpace Lax342547.TagGeometry Lax342547.ConcreteGeometry
    17open Lax342547.Atoms Lax342547.AtomDirections Lax342547.BinaryMixer
    18
    19def MixerGood {k n b degree : ℕ} {F : Type} [Fintype F]
    20 (L : F → Moment k n b degree) : Prop :=
    21 ∀ s t : Fin b → Binary, s ≠ t → ∀ a b' : F → Binary,
    22 (∃ j, a j ≠ 0 ∨ b' j ≠ 0) →
    23 n ≤ 5 * (OrderedMixerLaw.familyParity (blockDirections s free)
    24 (blockDirections t free) a b' L).rank
    25
    26def SharpGood {n b : ℕ} (M : Fin b → Matrix (Fin n) (Fin n) Binary) : Prop :=
    27 ∀ s t : Fin b → Binary, s ≠ t → ∀ c d : Binary, (c ≠ 0 ∨ d ≠ 0) →
    28 n ≤ 5 * (c • SharpMixerLaw.weighted (fun a => s a + t a) M +
    29 d • (SharpMixerLaw.weighted (fun a => s a + t a) M).transpose).rank
    30
    31def UniformBinary {k n b degree r : ℕ} {F : Type} [Fintype F]
    32 (hr : 2 * r ≤ n) (hd : 1 ≤ degree)
    33 (L : F → Moment k n b degree) (M : Fin b → Matrix (Fin n) (Fin n) Binary) : Prop :=
    34 ∀ s t : Fin b → Binary, s ≠ t → ∀ l m : Tag k, ∀ f g : Flavor k,
    35 ∀ a b' : F → Binary, ∀ c d : Binary,
    36 ((∃ j, a j ≠ 0 ∨ b' j ≠ 0) ∨ c ≠ 0 ∨ d ≠ 0) →
    37 n ≤ 5 * (bilinearPart (ambientParity L a b' (selfGram hr hd M) c d) s t l m f g).rank
    38
    39abbrev MixerTest (b : ℕ) (F : Type) :=
    40 (Fin b → Binary) × (Fin b → Binary) × (F → Binary) × (F → Binary)
    41
    42abbrev SharpTest (b : ℕ) := (Fin b → Binary) × (Fin b → Binary) × Binary × Binary
    43
    44open scoped ENNReal
    45
    46noncomputable def failureBound (b m n : ℕ) : ℝ≥0∞ := 2 ^ (2 * b + 2 * m) / 2 ^ n
    47
    48axiom uniform_of_restrictions {k n b degree r : ℕ} {F : Type} [Fintype F]
    49 (hr : 2 * r ≤ n) (hd : 1 ≤ degree)
    50 (L : F → Moment k n b degree) (M : Fin b → Matrix (Fin n) (Fin n) Binary)
    51 (hL : MixerGood L) (hM : SharpGood M) : UniformBinary hr hd L M
    52
    53axiom mixer_failure_bound {k n b degree : ℕ} {F : Type} [Fintype F] [DecidableEq F]
    54 (hd : 1 ≤ degree) (hn : 50 ≤ n) :
    55 (PMF.uniformOfFintype (F → Moment k n b degree)).toOuterMeasure
    56 {L | ¬ MixerGood L} ≤ failureBound b (Fintype.card F) n
    57
    58axiom sharp_failure_bound {n b : ℕ} (hn : 50 ≤ n) :
    59 (PMF.uniformOfFintype (Fin b → Matrix (Fin n) (Fin n) Binary)).toOuterMeasure
    60 {M | ¬ SharpGood M} ≤ failureBound b 1 n
    61
    62end Lax342547.BinaryMixers
    63
    Show 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…