Lax Lean Archive

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

Actual exposure cover projection

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

    Quotienting the exposed columns and restricting to the annihilator of exposed rows gives the actual covered-tensor projection, its mode envelopes, rank monotonicity, and sum identity.

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

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

    1 cover_restriction_kernel proven

    2 projected_column_envelope proven

    3 projected_row_envelope proven

    4 projection_rank_le proven

    5 projection_sum proven

    6 projection_zero_of_columns proven

    Lean source view on GitHub

    1import Lax342547.ProjectedSpans
    2import Lax342547.RankLoss
    3
    4/-!
    5---
    6title: Actual exposure cover projection
    7type: lemma
    8---
    9Quotienting the exposed columns and restricting to the annihilator of exposed rows gives the actual covered-tensor projection, its mode envelopes, rank monotonicity, and sum identity.
    10-/
    11
    12namespace Lax342547.CoverProjection
    13
    14open Lax342547.GreedySpans
    15open scoped BigOperators
    16
    17noncomputable def projection {K V W : Type} [Field K] [AddCommGroup V] [Module K V]
    18 [AddCommGroup W] [Module K W] (M : V →ₗ[K] W)
    19 (S : Submodule K W) (T : Submodule K (Module.Dual K V)) :
    20 T.dualCoannihilator →ₗ[K] (W ⧸ S) := S.mkQ.comp (M.comp T.dualCoannihilator.subtype)
    21
    22axiom cover_restriction_kernel {K V : Type} [Field K] [AddCommGroup V] [Module K V]
    23 [FiniteDimensional K V] (T : Submodule K (Module.Dual K V)) :
    24 LinearMap.ker T.dualCoannihilator.subtype.dualMap = T
    25
    26axiom projected_column_envelope {K V W : Type} [Field K] [AddCommGroup V] [Module K V]
    27 [AddCommGroup W] [Module K W] (M : V →ₗ[K] W)
    28 (S : Submodule K W) (T : Submodule K (Module.Dual K V)) :
    29 LinearMap.range (projection M S T) ≤ (LinearMap.range M).map S.mkQ
    30
    31axiom projected_row_envelope {K V W : Type} [Field K] [AddCommGroup V] [Module K V]
    32 [AddCommGroup W] [Module K W] (M : V →ₗ[K] W)
    33 (S : Submodule K W) (T : Submodule K (Module.Dual K V)) :
    34 LinearMap.range (projection M S T).dualMap ≤
    35 (LinearMap.range M.dualMap).map T.dualCoannihilator.subtype.dualMap
    36
    37axiom projection_rank_le {K V W : Type} [Field K] [AddCommGroup V] [Module K V]
    38 [AddCommGroup W] [Module K W] [FiniteDimensional K V] [FiniteDimensional K W]
    39 (M : V →ₗ[K] W) (S : Submodule K W) (T : Submodule K (Module.Dual K V)) :
    40 Module.finrank K (LinearMap.range (projection M S T)) ≤ Module.finrank K (LinearMap.range M)
    41
    42axiom projection_zero_of_columns {K V W : Type} [Field K] [AddCommGroup V] [Module K V]
    43 [AddCommGroup W] [Module K W] (M : V →ₗ[K] W)
    44 (S : Submodule K W) (T : Submodule K (Module.Dual K V)) (h : LinearMap.range M ≤ S) :
    45 projection M S T = 0
    46
    47axiom projection_sum {K V W ι : Type} [Field K] [Fintype ι]
    48 [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W]
    49 (M : ι → V →ₗ[K] W) (S : Submodule K W) (T : Submodule K (Module.Dual K V)) :
    50 projection (∑ i, M i) S T = ∑ i, projection (M i) S T
    51
    52end Lax342547.CoverProjection
    53
    Show 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…