Lax Lean Archive

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

Joint channel law and its independent-column density

Lax342547.ChannelDensity · concepts/Lax342547/ChannelDensity.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 raw joint channel law is constant on each individually injective Gram orbit. Gram normalization bounds its density relative to completely independent channel columns by 2^(h²+2), independently of the primal dimension. The bound multiplies over the fixed set of components.

    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 4 statements. Each proof establishes one of them relative to its assumptions.

    1 all_components_density proven

    2 event_density proven

    3 point_density proven

    4 same_gram_mass proven

    Lean source view on GitHub

    1import Lax342547.FrameSymmetry
    2import Lax342547.GramNormalization
    3
    4/-!
    5---
    6title: Joint channel law and its independent-column density
    7type: lemma
    8---
    9The raw joint channel law is constant on each individually injective
    10Gram orbit. Gram normalization bounds its density relative to completely
    11independent channel columns by 2^(h²+2), independently of the primal
    12dimension. The bound multiplies over the fixed set of components.
    13-/
    14
    15namespace Lax342547.ChannelDensity
    16
    17open Lax342547.MomentSpace Lax342547.RawFrames
    18open scoped ENNReal
    19
    20variable {B H N : Type} [Fintype B] [Fintype H] [Fintype N]
    21
    22def channels {E : Matrix B B Binary} (F : Frame B H N E) :
    23 Matrix N H Binary × Matrix N H Binary := (F.X, F.Y)
    24
    25noncomputable def jointLaw (E : Matrix B B Binary) [Nonempty (Frame B H N E)] :
    26 PMF (Matrix N H Binary × Matrix N H Binary) :=
    27 (PMF.uniformOfFintype (Frame B H N E)).map channels
    28
    29axiom same_gram_mass [DecidableEq N] (E : Matrix B B Binary)
    30 [Nonempty (Frame B H N E)] (A A' B B' : Matrix N H Binary)
    31 (hA : Function.Injective A.mulVec) (hA' : Function.Injective A'.mulVec)
    32 (hB : Function.Injective B.mulVec) (hB' : Function.Injective B'.mulVec)
    33 (hG : A.transpose * B = A'.transpose * B') :
    34 jointLaw E (A, B) = jointLaw E (A', B')
    35
    36axiom point_density [DecidableEq H] [DecidableEq N]
    37 (E : Matrix B B Binary) [Nonempty (Frame B H N E)]
    38 (hN : Fintype.card H + Fintype.card H + 1 ≤ Fintype.card N)
    39 (z : Matrix N H Binary × Matrix N H Binary) :
    40 jointLaw E z ≤ (2 : ℝ≥0∞) ^ (Fintype.card H * Fintype.card H + 2) *
    41 PMF.uniformOfFintype (Matrix N H Binary × Matrix N H Binary) z
    42
    43axiom event_density [DecidableEq H] [DecidableEq N]
    44 (E : Matrix B B Binary) [Nonempty (Frame B H N E)]
    45 (hN : Fintype.card H + Fintype.card H + 1 ≤ Fintype.card N)
    46 (S : Set (Matrix N H Binary × Matrix N H Binary)) :
    47 (jointLaw E).toOuterMeasure S ≤
    48 (2 : ℝ≥0∞) ^ (Fintype.card H * Fintype.card H + 2) *
    49 (PMF.uniformOfFintype (Matrix N H Binary × Matrix N H Binary)).toOuterMeasure S
    50
    51axiom all_components_density {Comp : Type} [Fintype Comp] [DecidableEq Comp]
    52 [DecidableEq H] [DecidableEq N]
    53 (E : Matrix B B Binary) [Nonempty (Frame B H N E)]
    54 (hN : Fintype.card H + Fintype.card H + 1 ≤ Fintype.card N)
    55 (z : Comp → Matrix N H Binary × Matrix N H Binary) :
    56 (RawLaw.uniformLaw E).map (fun o e => channels (o e)) z ≤
    57 (2 : ℝ≥0∞) ^ (Fintype.card Comp * (Fintype.card H * Fintype.card H + 2)) *
    58 PMF.uniformOfFintype (Comp → Matrix N H Binary × Matrix N H Binary) z
    59
    60end Lax342547.ChannelDensity
    61
    Show 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…