Lax Lean Archive

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

Rank control for the frozen baseline on primal inputs

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

    Retract the primal inputs before constructing the baseline. Its channel evaluation factors through the bounded primal retraction and the dual of the opposite pin space. This separates the two costs and avoids paying for arbitrary channel-channel entries of the table.

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

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

    1 bounded_baseline proven

    2 channel_rank proven

    Lean source view on GitHub

    1import Lax342547.PrimalRetractions
    2import Mathlib.LinearAlgebra.Dual.Lemmas
    3import Mathlib.LinearAlgebra.Dimension.Constructions
    4import Mathlib.LinearAlgebra.Dimension.LinearMap
    5
    6/-!
    7---
    8title: Rank control for the frozen baseline on primal inputs
    9type: lemma
    10---
    11Retract the primal inputs before constructing the baseline. Its channel
    12evaluation factors through the bounded primal retraction and the dual of
    13the opposite pin space. This separates the two costs and avoids paying
    14for arbitrary channel-channel entries of the table.
    15-/
    16
    17namespace Lax342547.BaselineRank
    18
    19open Lax342547.MomentSpace Lax342547.FrozenBaselines
    20
    21variable {V W C : Type} [AddCommGroup V] [Module Binary V]
    22 [AddCommGroup W] [Module Binary W] [AddCommGroup C] [Module Binary C]
    23
    24def retracted {J D Keys : Submodule Binary V} (S : Splitting J D Keys)
    25 (hD : D ≤ J) (p : V →ₗ[Binary] V) (hfix : ∀ v ∈ J ⊔ Keys, p v = v) :
    26 Splitting J D Keys where
    27 frozen := S.frozen.comp p
    28 table := S.table.comp p
    29 frozen_fixed v hv := by
    30 rw [LinearMap.comp_apply, hfix v ((sup_le_sup hD le_rfl) hv)]
    31 exact S.frozen_fixed v hv
    32 table_zero v hv := by
    33 rw [LinearMap.comp_apply, hfix v ((sup_le_sup hD le_rfl) hv)]
    34 exact S.table_zero v hv
    35 frozen_table v := by
    36 rw [LinearMap.comp_apply, hfix v.val ((show J ≤ J ⊔ Keys from le_sup_left) v.property)]
    37 exact S.frozen_table v
    38 table_sum v := by
    39 simp only [LinearMap.comp_apply, hfix v.val ((show J ≤ J ⊔ Keys from le_sup_left) v.property)]
    40 exact S.table_sum v
    41
    42axiom channel_rank [FiniteDimensional Binary V] [FiniteDimensional Binary W]
    43 (J D Keys U : Submodule Binary V) (J' D' Keys' : Submodule Binary W)
    44 (hD : D ≤ J) (S : Splitting J D Keys) (S' : Splitting J' D' Keys')
    45 (p : V →ₗ[Binary] V) (hfix : ∀ v ∈ J ⊔ Keys, p v = v)
    46 (A : V →ₗ[Binary] W →ₗ[Binary] Binary) (T : J →ₗ[Binary] J' →ₗ[Binary] Binary)
    47 (q : C →ₗ[Binary] J') :
    48 Module.finrank Binary (LinearMap.range
    49 ((baseline (retracted S hD p hfix) S' A T).compl₁₂ U.subtype (J'.subtype.comp q))) ≤
    50 Module.finrank Binary (LinearMap.range (p.comp U.subtype)) + Module.finrank Binary D'
    51
    52axiom bounded_baseline [FiniteDimensional Binary V] [FiniteDimensional Binary W]
    53 (J D Keys U : Submodule Binary V) (J' D' Keys' U' : Submodule Binary W)
    54 (hD : D ≤ J) (hD' : D' ≤ J') (hKeys : Disjoint J Keys) (hKeys' : Disjoint J' Keys')
    55 (hspan : J ⊔ U = ⊤) (hKeyPrimal : Keys ≤ U)
    56 (hspan' : J' ⊔ U' = ⊤) (hKeyPrimal' : Keys' ≤ U')
    57 (A : V →ₗ[Binary] W →ₗ[Binary] Binary) (T : J →ₗ[Binary] J' →ₗ[Binary] Binary)
    58 (h : Compatible J D J' D' A T) :
    59 ∃ B : V →ₗ[Binary] W →ₗ[Binary] Binary,
    60 ExtendsFrozen D Keys D' Keys' A B ∧ (∀ v : J, ∀ w : J', B v.val w.val = T v w) ∧
    61 (∀ q : C →ₗ[Binary] J',
    62 Module.finrank Binary (LinearMap.range (B.compl₁₂ U.subtype (J'.subtype.comp q))) ≤
    63 Module.finrank Binary ↥(J ⊓ U) + Module.finrank Binary Keys + Module.finrank Binary D') ∧
    64 ∀ q : C →ₗ[Binary] J,
    65 Module.finrank Binary (LinearMap.range (B.flip.compl₁₂ U'.subtype (J.subtype.comp q))) ≤
    66 Module.finrank Binary ↥(J' ⊓ U') + Module.finrank Binary Keys' + Module.finrank Binary D
    67
    68end Lax342547.BaselineRank
    69
    Show 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…