Lax Lean Archive

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

Point atoms and finite flavor distributions

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

    Definition 5.4 on the concrete cut space. Each atom has a single nonzero moment representative. Generic, shared-only, and pure flavors retain exactly their specified coordinates, and always retain the # and Z blocks. Their parameter law samples all retained bits independently and uniformly.

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

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

    1 atom_component proven

    2 flavor_coordinates proven

    3 parameterLaw_product proven

    Lean source view on GitHub

    1import Lax342547.ConcreteCut
    2import Mathlib.Probability.Distributions.Uniform
    3import Mathlib.Tactic.DeriveFintype
    4
    5/-!
    6---
    7title: Point atoms and finite flavor distributions
    8type: lemma
    9---
    10Definition 5.4 on the concrete cut space. Each atom has a single nonzero
    11moment representative. Generic, shared-only, and pure flavors retain
    12exactly their specified coordinates, and always retain the # and Z blocks.
    13Their parameter law samples all retained bits independently and uniformly.
    14-/
    15
    16namespace Lax342547.Atoms
    17
    18set_option backward.isDefEq.respectTransparency false
    19
    20open Lax342547.MomentSpace Lax342547.TagGeometry Lax342547.ConcreteGeometry
    21open Lax342547.CutProfiles Lax342547.ConcreteCut
    22
    23noncomputable def atomRepresentation {k n b degree : ℕ} (l : Tag k)
    24 (s : Fin b → Binary) (z : Base k n → Binary)
    25 (hz : ∀ i, i ∉ allowedBase k n l → z i = 0) : Representation k n b degree := by
    26 classical
    27 refine ⟨Pi.single l (pointMoment selectorEval s z), ?_⟩
    28 intro t _
    29 by_cases ht : l = t
    30 · subst t
    31 simp only [Pi.single_eq_same]
    32 exact Submodule.subset_span ⟨s, z, hz, rfl⟩
    33 · simp [ht]
    34
    35noncomputable def atom {k n b degree : ℕ} (l : Tag k) (s : Fin b → Binary) (z : Base k n → Binary)
    36 (hz : ∀ i, i ∉ allowedBase k n l → z i = 0) : Profile k n b degree :=
    37 (representationCut k n b degree).rangeRestrict (atomRepresentation l s z hz)
    38
    39inductive Flavor (k : ℕ) where
    40 | generic
    41 | sharedOnly
    42 | pure (blocks : Finset (Tag k × Tag k))
    43 deriving Fintype
    44
    45def retained {k n : ℕ} (l : Tag k) (f : Flavor k) : Set (Base k n)
    46 | Sum.inl ((d, t), _) => l ∈ interval k d ∧ match f with
    47 | .generic => True
    48 | .sharedOnly => False
    49 | .pure blocks => (d, t) ∈ blocks
    50 | Sum.inr (q, _) => match f with
    51 | .pure _ => q ≠ 0
    52 | _ => True
    53
    54abbrev Parameters {k : ℕ} (n : ℕ) (l : Tag k) (f : Flavor k) :=
    55 {i : Base k n // i ∈ retained l f} → Binary
    56
    57noncomputable instance {k n : ℕ} (l : Tag k) (f : Flavor k) :
    58 Fintype {i : Base k n // i ∈ retained l f} := Fintype.ofFinite _
    59
    60noncomputable instance {k n : ℕ} (l : Tag k) (f : Flavor k) : Fintype (Parameters n l f) := by
    61 classical
    62 exact inferInstanceAs (Fintype ({i : Base k n // i ∈ retained l f} → Binary))
    63
    64noncomputable def parameterValue {k n : ℕ} {l : Tag k} {f : Flavor k} (p : Parameters n l f)
    65 (i : Base k n) : Binary := by
    66 classical
    67 exact if hi : i ∈ retained l f then p ⟨i, hi⟩ else 0
    68
    69noncomputable def parameterLaw {k : ℕ} (n : ℕ) (l : Tag k) (f : Flavor k) :
    70 PMF (Parameters n l f) := PMF.uniformOfFintype _
    71
    72def testerSummary {k n b degree r : ℕ} (hr : 2 * r ≤ n)
    73 (s : Fin b → Binary) (z : Base k n → Binary) : Option (Tag k × Tag k) → Binary
    74 | none => blockTester (degree := degree) hr shared (pointMoment selectorEval s z)
    75 | some (d, t) => blockTester (degree := degree) hr (ordinary d t) (pointMoment selectorEval s z)
    76
    77axiom atom_component {k n b degree : ℕ} (l : Tag k) (s : Fin b → Binary) (z : Base k n → Binary)
    78 (hz : ∀ i, i ∉ allowedBase k n l → z i = 0) (e : Component (Tag k)) :
    79 (atom (degree := degree) l s z hz).val e = if l ∈ e.val then pointMoment selectorEval s z else 0
    80
    81axiom flavor_coordinates {k n : ℕ} (l : Tag k) (f : Flavor k) :
    82 retained (n := n) l f ⊆ allowedBase k n l ∧
    83 (∀ i : Fin n, sharp i ∈ retained l f) ∧ (∀ i : Fin n, free i ∈ retained l f)
    84
    85axiom parameterLaw_product {k n : ℕ} (l : Tag k) (f : Flavor k) (p : Parameters n l f) :
    86 parameterLaw n l f p = ∏ i : {i : Base k n // i ∈ retained l f}, PMF.uniformOfFintype Binary (p i)
    87
    88end Lax342547.Atoms
    89
    Show 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…