Lax Lean Archive

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

The finite simultaneous unary mixer estimate

Lax342547.UnaryMixers · concepts/Lax342547/UnaryMixers.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 union runs only over nonzero bounded-rank profiles, tags, and labels. All non-Z fixings are already covered by each individual bad event. The finite estimate gives a simultaneous choice whenever its explicit upper bound is below one. No unit law appears in that choice.

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

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

    1 exists_for_large_n proven

    2 exists_of_failureBound_lt_one proven

    3 exists_uniform_unary proven

    4 failureBound_le_geometric proven

    5 failureBound_lt_one proven

    6 simultaneous_failure_bound proven

    7 uniform_of_good proven

    Lean source view on GitHub

    1import Lax342547.UnaryRowLaw
    2import Lax342547.ProfileCounting
    3import Lax342547.CoordinateCounts
    4
    5/-!
    6---
    7title: The finite simultaneous unary mixer estimate
    8type: lemma
    9---
    10The union runs only over nonzero bounded-rank profiles, tags, and labels.
    11All non-Z fixings are already covered by each individual bad event.
    12The finite estimate gives a simultaneous choice whenever its explicit
    13upper bound is below one. No unit law appears in that choice.
    14-/
    15
    16namespace Lax342547.UnaryMixers
    17
    18open Lax342547.MomentSpace Lax342547.TagGeometry Lax342547.ConcreteGeometry
    19open Lax342547.ConcreteCut Lax342547.CutProfiles Lax342547.UnaryRowLaw
    20
    21abbrev Test (k n b degree K : ℕ) :=
    22 {x : Profile k n b degree // ∑ e, (x.val e).rank ≤ K} × Tag k × (Fin b → Binary)
    23
    24noncomputable instance (k n b degree K : ℕ) : Fintype (Test k n b degree K) := Fintype.ofFinite _
    25
    26def Good {k n b degree r₀ J : ℕ} {hr : 2 * r₀ ≤ n}
    27 (D : Testers (k := k) (b := b) (degree := degree) hr) (K s₀ : ℕ)
    28 (M : Index (Component (Tag k)) J → Moment k n b degree) : Prop :=
    29 ∀ x : Profile k n b degree, x ≠ 0 → (∑ e, (x.val e).rank ≤ K) →
    30 ∀ l s, ¬ UnaryBad D x l s s₀ M
    31
    32def UniformUnary {k n b degree r₀ J : ℕ} {hr : 2 * r₀ ≤ n}
    33 (D : Testers (k := k) (b := b) (degree := degree) hr) (K s₀ : ℕ)
    34 (M : Index (Component (Tag k)) J → Moment k n b degree) : Prop :=
    35 ∀ x : Profile k n b degree, x ≠ 0 → (∑ e, (x.val e).rank ≤ K) → ∀ l s,
    36 ∃ W : Submodule Binary (Module.Dual Binary (Fin n → Binary)),
    37 Module.finrank Binary W ≤ 4 * J * (2 * k) * K ∧
    38 ∀ z : Base k n → Binary, ∀ hz : ∀ i, i ∉ allowedBase k n l → z i = 0,
    39 2 * (J - s₀) ≤ (FormalQuadratic.polarMatrix (fun v =>
    40 gradient D (leftMixers M) (rightMixers M) x (UnaryMixer.atomAlongZ l s z hz v))).rank ∧
    41 ∀ u v, (∀ a ∈ W, a u = a v) →
    42 gradient D (leftMixers M) (rightMixers M) x (UnaryMixer.atomAlongZ l s z hz u) =
    43 gradient D (leftMixers M) (rightMixers M) x (UnaryMixer.atomAlongZ l s z hz v)
    44
    45noncomputable def testCountBound (k n b degree K : ℕ) : ℕ :=
    46 ((K + 1) ^ Fintype.card (Component (Tag k)) *
    47 2 ^ (Fintype.card (Coordinate k n b degree) * K + K * K)) * (2 * k + 1) * 2 ^ b
    48
    49open scoped ENNReal
    50
    51noncomputable def failureBound (k n b degree J K s₀ : ℕ) : ℝ≥0∞ :=
    52 testCountBound k n b degree K *
    53 (2 ^ (2 * J * K ^ 2 + (s₀ + 1) * (4 * J * (2 * k) * K)) / 2 ^ ((s₀ + 1) * n))
    54
    55noncomputable def threshold (k b degree J K s₀ : ℕ) : ℕ :=
    56 (K + 1) ^ Fintype.card (Component (Tag k)) * (2 * k + 1) * 2 ^ b *
    57 2 ^ ((∑ j ∈ Finset.range (degree + 1), b.choose j) * K + K * K +
    58 (2 * J * K ^ 2 + (s₀ + 1) * (4 * J * (2 * k) * K)))
    59
    60axiom failureBound_le_geometric (k n b degree J K s₀ : ℕ)
    61 (hmargin : (∑ j ∈ Finset.range (degree + 1), b.choose j) * ((2 * k + 1) ^ 2 + 3) * K ≤ s₀) :
    62 failureBound k n b degree J K s₀ ≤ (threshold k b degree J K s₀ : ℝ≥0∞) / 2 ^ n
    63
    64axiom uniform_of_good {k n b degree r₀ J K s₀ : ℕ} {hr : 2 * r₀ ≤ n}
    65 (D : Testers (k := k) (b := b) (degree := degree) hr)
    66 (M : Index (Component (Tag k)) J → Moment k n b degree)
    67 (hM : Good D K s₀ M) : UniformUnary D K s₀ M
    68
    69axiom failureBound_lt_one (k n b degree J K s₀ : ℕ)
    70 (hmargin : (∑ j ∈ Finset.range (degree + 1), b.choose j) * ((2 * k + 1) ^ 2 + 3) * K ≤ s₀)
    71 (hn : threshold k b degree J K s₀ ≤ n) :
    72 failureBound k n b degree J K s₀ < 1
    73
    74axiom simultaneous_failure_bound {k n b degree r₀ J K : ℕ} {hr : 2 * r₀ ≤ n}
    75 (hk : 0 < k) (D : Testers (k := k) (b := b) (degree := degree) hr) (s₀ : ℕ) :
    76 (PMF.uniformOfFintype (Index (Component (Tag k)) J → Moment k n b degree)).toOuterMeasure
    77 {M | ¬ Good D K s₀ M} ≤ failureBound k n b degree J K s₀
    78
    79axiom exists_of_failureBound_lt_one {k n b degree r₀ J K : ℕ} {hr : 2 * r₀ ≤ n}
    80 (hk : 0 < k) (D : Testers (k := k) (b := b) (degree := degree) hr) (s₀ : ℕ)
    81 (hsmall : failureBound k n b degree J K s₀ < 1) :
    82 ∃ M : Index (Component (Tag k)) J → Moment k n b degree, Good D K s₀ M
    83
    84axiom exists_for_large_n (k b degree J K s₀ : ℕ) (hk : 0 < k)
    85 (hmargin : (∑ j ∈ Finset.range (degree + 1), b.choose j) * ((2 * k + 1) ^ 2 + 3) * K ≤ s₀) :
    86 ∃ n₀, ∀ n, n₀ ≤ n → ∀ r₀ (hr : 2 * r₀ ≤ n)
    87 (D : Testers (k := k) (b := b) (degree := degree) hr),
    88 ∃ M : Index (Component (Tag k)) J → Moment k n b degree, Good D K s₀ M
    89
    90axiom exists_uniform_unary (k b degree J K s₀ : ℕ) (hk : 0 < k)
    91 (hmargin : (∑ j ∈ Finset.range (degree + 1), b.choose j) * ((2 * k + 1) ^ 2 + 3) * K ≤ s₀) :
    92 ∃ n₀, ∀ n, n₀ ≤ n → ∀ r₀ (hr : 2 * r₀ ≤ n)
    93 (D : Testers (k := k) (b := b) (degree := degree) hr),
    94 ∃ M : Index (Component (Tag k)) J → Moment k n b degree, UniformUnary D K s₀ M
    95
    96end Lax342547.UnaryMixers
    97
    Show ProofShow ProofShow 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…