Lax Lean Archive

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

Joint distribution of the unary mixer row matrix

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

    All indexed L and R matrices are sampled from one finite product. The full forward/reverse observation list has additive compatibility cost. A surjective coordinate selection retains just the incident formal rows, including their separate L and R halves.

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

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

    1 joint_row_law proven

    2 mixerRows_rank proven

    3 row_corank_bound proven

    4 unary_failure_probability proven

    Lean source view on GitHub

    1import Lax342547.UnaryMixer
    2import Lax342547.MixerRowLaw
    3import Lax342547.CorankCounting
    4
    5/-!
    6---
    7title: Joint distribution of the unary mixer row matrix
    8type: lemma
    9---
    10All indexed L and R matrices are sampled from one finite product.
    11The full forward/reverse observation list has additive compatibility
    12cost. A surjective coordinate selection retains just the incident
    13formal rows, including their separate L and R halves.
    14-/
    15
    16namespace Lax342547.UnaryRowLaw
    17
    18open Lax342547.MomentSpace Lax342547.UnaryMixer
    19
    20variable {E I N : Type} [Fintype E] [Fintype I] [Fintype N]
    21
    22abbrev Index (E : Type) (J : ℕ) := Bool × Fin J × E × E
    23
    24abbrev RowIndex (r : E → ℕ) (inc : Finset E) (J : ℕ) :=
    25 (t : Block inc J) × (Fin (blockRank r t) ⊕ Fin (blockRank r t))
    26
    27noncomputable instance (r : E → ℕ) (inc : Finset E) (J : ℕ) :
    28 DecidableEq (RowIndex r inc J) := Classical.decEq _
    29
    30noncomputable instance (r : E → ℕ) (inc : Finset E) (J : ℕ) :
    31 Fintype (RowIndex r inc J) := Fintype.ofFinite _
    32
    33def flatten {r : E → ℕ} {inc : Finset E} {J : ℕ} :
    34 Rows r inc J ≃ₗ[Binary] (RowIndex r inc J → Binary) where
    35 toFun x a := Sum.elim (x a.1).1 (x a.1).2 a.2
    36 invFun y t := (fun a => y ⟨t, .inl a⟩, fun a => y ⟨t, .inr a⟩)
    37 left_inv x := rfl
    38 right_inv y := by funext a; rcases a with ⟨t, a | a⟩ <;> rfl
    39 map_add' x y := by funext a; rcases a with ⟨t, a | a⟩ <;> rfl
    40 map_smul' a x := by funext b; rcases b with ⟨t, b | b⟩ <;> rfl
    41
    42abbrev FullList (r : E → ℕ) (J : ℕ) (N : Type) :=
    43 ∀ p : Index E J, Matrix (Fin (r p.2.2.1)) N Binary × Matrix N (Fin (r p.2.2.2)) Binary
    44
    45def fullObservations {r : E → ℕ} {J : ℕ}
    46 (Z : ∀ e, Matrix I (Fin (r e)) Binary) (D : Matrix I N Binary) :
    47 (Index E J → Matrix I I Binary) →ₗ[Binary] FullList r J N :=
    48 FiniteLinearLaw.familyMap (fun p => MixerRowLaw.observations (Z p.2.2.1) (Z p.2.2.2) D)
    49
    50def pack {r : E → ℕ} (inc : Finset E) {J : ℕ} :
    51 FullList r J N →ₗ[Binary] Matrix (RowIndex r inc J) N Binary where
    52 toFun y a i := match a with
    53 | ⟨.inl (j, e, f), .inl h⟩ => (y (false, j, e, f.val)).1 h i
    54 | ⟨.inl (j, e, f), .inr h⟩ => (y (true, j, e, f.val)).1 h i
    55 | ⟨.inr (j, e, f), .inl h⟩ => (y (false, j, e.val, f)).2 i h
    56 | ⟨.inr (j, e, f), .inr h⟩ => (y (true, j, e.val, f)).2 i h
    57 map_add' x y := by
    58 funext a i
    59 rcases a with ⟨⟨j, e, f⟩ | ⟨j, e, f⟩, a | a⟩ <;> rfl
    60 map_smul' c x := by
    61 funext a i
    62 rcases a with ⟨⟨j, e, f⟩ | ⟨j, e, f⟩, a | a⟩ <;> rfl
    63
    64def mixerRows {r : E → ℕ} (inc : Finset E) {J : ℕ}
    65 (Z : ∀ e, Matrix I (Fin (r e)) Binary) (D : Matrix I N Binary) :
    66 (Index E J → Matrix I I Binary) →ₗ[Binary] Matrix (RowIndex r inc J) N Binary :=
    67 (pack inc).comp (fullObservations Z D)
    68
    69noncomputable def rowLinear {r : E → ℕ} (inc : Finset E) {J : ℕ}
    70 (Z : ∀ e, Matrix I (Fin (r e)) Binary) (D : Matrix I N Binary)
    71 (M : Index E J → Matrix I I Binary) : (N → Binary) →ₗ[Binary] Rows r inc J :=
    72 (rowMap inc Z (fun j e f => M (false, j, e, f))
    73 (fun j e f => M (true, j, e, f))).comp D.mulVecLin
    74
    75axiom mixerRows_rank {r : E → ℕ} (inc : Finset E) {J : ℕ}
    76 (Z : ∀ e, Matrix I (Fin (r e)) Binary) (D : Matrix I N Binary)
    77 (M : Index E J → Matrix I I Binary) :
    78 (mixerRows inc Z D M).rank = Module.finrank Binary (LinearMap.range (rowLinear inc Z D M))
    79
    80open scoped ENNReal
    81
    82axiom joint_row_law [DecidableEq E] [DecidableEq I] [DecidableEq N]
    83 {r : E → ℕ} (inc : Finset E) {J K : ℕ}
    84 (Z : ∀ e, Matrix I (Fin (r e)) Binary) (D : Matrix I N Binary)
    85 (hZ : ∀ e, Function.Injective (Z e).mulVec) (hD : Function.Injective D.mulVec)
    86 (hr : ∑ e, r e ≤ K) (y : Matrix (RowIndex r inc J) N Binary) :
    87 (PMF.uniformOfFintype (Index E J → Matrix I I Binary)).map (mixerRows inc Z D) y ≤
    88 2 ^ (2 * J * K ^ 2) * PMF.uniformOfFintype (Matrix (RowIndex r inc J) N Binary) y
    89
    90axiom row_corank_bound [DecidableEq E] [DecidableEq I] [DecidableEq N]
    91 {r : E → ℕ} (inc : Finset E) {J K : ℕ}
    92 (Z : ∀ e, Matrix I (Fin (r e)) Binary) (D : Matrix I N Binary)
    93 (hZ : ∀ e, Function.Injective (Z e).mulVec) (hD : Function.Injective D.mulVec)
    94 (hr : ∑ e, r e ≤ K) (s : ℕ) :
    95 (PMF.uniformOfFintype (Index E J → Matrix I I Binary)).toOuterMeasure
    96 {M | (mixerRows inc Z D M).rank + s ≤ Fintype.card (RowIndex r inc J)} ≤
    97 (2 : ℝ≥0∞) ^ (2 * J * K ^ 2 + s * (4 * J * inc.card * K)) / 2 ^ (s * Fintype.card N)
    98
    99def leftMixers {J : ℕ} (M : Index E J → Matrix I I Binary) : Fin J → E → E → Matrix I I Binary :=
    100 fun j e f => M (false, j, e, f)
    101
    102def rightMixers {J : ℕ} (M : Index E J → Matrix I I Binary) : Fin J → E → E → Matrix I I Binary :=
    103 fun j e f => M (true, j, e, f)
    104
    105open Lax342547.TagGeometry Lax342547.ConcreteGeometry Lax342547.ConcreteCut Lax342547.CutProfiles
    106
    107def UnaryBad {k n b degree r₀ J : ℕ} {hr : 2 * r₀ ≤ n}
    108 (D : Testers (k := k) (b := b) (degree := degree) hr) (x : Profile k n b degree)
    109 (l : Tag k) (s : Fin b → Binary) (s₀ : ℕ)
    110 (M : Index (Component (Tag k)) J → Moment k n b degree) : Prop :=
    111 ∃ z : Base k n → Binary, ∃ hz : ∀ i, i ∉ allowedBase k n l → z i = 0,
    112 (FormalQuadratic.polarMatrix (fun v =>
    113 gradient D (leftMixers M) (rightMixers M) x (atomAlongZ l s z hz v))).rank < 2 * (J - s₀)
    114
    115axiom unary_failure_probability {k n b degree r₀ J K : ℕ} {hr : 2 * r₀ ≤ n}
    116 (hk : 0 < k) (D : Testers (k := k) (b := b) (degree := degree) hr)
    117 (x : Profile k n b degree) (hx : x ≠ 0) (hK : ∑ e, (x.val e).rank ≤ K)
    118 (l : Tag k) (s : Fin b → Binary) (s₀ : ℕ) :
    119 (PMF.uniformOfFintype (Index (Component (Tag k)) J → Moment k n b degree)).toOuterMeasure
    120 {M | UnaryBad D x l s s₀ M} ≤
    121 (2 : ℝ≥0∞) ^ (2 * J * K ^ 2 + (s₀ + 1) * (4 * J * (2 * k) * K)) / 2 ^ ((s₀ + 1) * n)
    122
    123end Lax342547.UnaryRowLaw
    124
    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…