Lax Lean Archive

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

Boolean polynomial nonvanishing and exactification

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

    Finite differences of the actual bounded-degree selector span prove its uniform nonzero mass, exactification below that threshold, and recovery across excluded labels.

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

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

    1 constant_weight proven

    2 derivative_degree proven

    3 derivative_monomial proven

    4 derivative_weight proven

    5 excluded_labels_exactification proven

    6 flip_twice proven

    7 invariant_constant proven

    8 nonzero_weight proven

    9 uniform_error_exactification proven

    10 uniform_nonzero_mass proven

    Lean source view on GitHub

    1import Lax342547.SelectorInterpolation
    2import Lax342547.Walsh
    3import Lax342547.FiniteSampling
    4
    5/-!
    6---
    7title: Boolean polynomial nonvanishing and exactification
    8type: lemma
    9---
    10Finite differences of the actual bounded-degree selector span prove its uniform nonzero mass, exactification below that threshold, and recovery across excluded labels.
    11-/
    12
    13namespace Lax342547.BooleanWeight
    14
    15open Lax342547.MomentSpace Lax342547.SelectorInterpolation
    16open scoped BigOperators
    17
    18noncomputable def flip {b : ℕ} (i : Fin b) (x : Fin b → Binary) : Fin b → Binary :=
    19 Function.update x i (x i+1)
    20
    21noncomputable def derivative {b : ℕ} (i : Fin b) (f : (Fin b → Binary) → Binary) :
    22 (Fin b → Binary) → Binary := fun x => f x+f (flip i x)
    23
    24noncomputable def weight {b : ℕ} (f : (Fin b → Binary) → Binary) : ℕ := by
    25 classical
    26 exact (Finset.univ.filter (fun x => f x ≠ 0)).card
    27
    28axiom flip_twice {b : ℕ} (i : Fin b) (x : Fin b → Binary) : flip i (flip i x) = x
    29
    30axiom derivative_monomial {b : ℕ} (i : Fin b) (S : Finset (Fin b)) :
    31 derivative i (monomial S) = if i ∈ S then monomial (S.erase i) else 0
    32
    33axiom derivative_degree {b d : ℕ} (i : Fin b) (f : (Fin b → Binary) → Binary)
    34 (hf : f ∈ selectorSpan b (d+1)) : derivative i f ∈ selectorSpan b d
    35
    36axiom invariant_constant {b : ℕ} (f : (Fin b → Binary) → Binary)
    37 (hf : ∀ i x, f (flip i x) = f x) : ∀ x y, f x = f y
    38
    39axiom derivative_weight {b : ℕ} (i : Fin b) (f : (Fin b → Binary) → Binary) :
    40 weight (derivative i f) ≤ 2*weight f
    41
    42axiom constant_weight {b : ℕ} (c : Binary) (hc : c ≠ 0) :
    43 weight (fun _ : Fin b → Binary => c) = 2^b
    44
    45axiom nonzero_weight {b d : ℕ} (f : (Fin b → Binary) → Binary)
    46 (hf : f ∈ selectorSpan b d) (hne : f ≠ 0) : 2^b ≤ 2^d*weight f
    47
    48axiom uniform_nonzero_mass {b d : ℕ} (f : (Fin b → Binary) → Binary)
    49 (hf : f ∈ selectorSpan b d) (hne : f ≠ 0) :
    50 1/(2 : ℝ)^d ≤ Lax342547.RetainedImages.cellMass (fun _ : Fin b → Binary => 1/(2 : ℝ)^b)
    51 (fun x => f x ≠ 0)
    52
    53axiom uniform_error_exactification {b d : ℕ} (f : (Fin b → Binary) → Binary)
    54 (hf : f ∈ selectorSpan b d)
    55 (herr : Lax342547.RetainedImages.cellMass (fun _ : Fin b → Binary => 1/(2 : ℝ)^b)
    56 (fun x => f x ≠ 0) < 1/(2 : ℝ)^d) : f = 0
    57
    58axiom excluded_labels_exactification {b d : ℕ} (f : (Fin b → Binary) → Binary)
    59 (hf : f ∈ selectorSpan b d) (E : Finset (Fin b → Binary))
    60 (hzero : ∀ x, x ∉ E → f x = 0) (hE : 2^d*E.card < 2^b) : f = 0
    61
    62end Lax342547.BooleanWeight
    63
    Show ProofShow ProofShow ProofShow 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…