Lax Lean Archive

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

Ambient symmetries and frame marginals

Lax342547.FrameSymmetry · concepts/Lax342547/FrameSymmetry.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 simultaneous primal and inverse-transpose action preserves all three raw Gram constraints. Its bijections of completion sets determine the uniform plus-frame and channel marginals exactly.

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

    1 full_frame_orbit proven

    2 minus_uniform proven

    3 minusChannel_uniform proven

    4 plus_uniform proven

    5 plusChannel_uniform proven

    Lean source view on GitHub

    1import Lax342547.RawLaw
    2import Mathlib.Data.Matrix.ColumnRowPartitioned
    3
    4/-!
    5---
    6title: Ambient symmetries and frame marginals
    7type: lemma
    8---
    9The simultaneous primal and inverse-transpose action preserves all three
    10raw Gram constraints. Its bijections of completion sets determine the
    11uniform plus-frame and channel marginals exactly.
    12-/
    13
    14namespace Lax342547.FrameSymmetry
    15
    16open Lax342547.MomentSpace Lax342547.RawFrames
    17
    18variable {B H N : Type} [Fintype B] [Fintype H] [Fintype N] [DecidableEq N]
    19
    20structure Change (N : Type) [Fintype N] [DecidableEq N] where
    21 C : Matrix N N Binary
    22 D : Matrix N N Binary
    23 CD : C * D = 1
    24 DC : D * C = 1
    25
    26def Change.inv (c : Change N) : Change N := ⟨c.D, c.C, c.DC, c.CD⟩
    27
    28def Change.dual (c : Change N) : Change N where
    29 C := c.D.transpose
    30 D := c.C.transpose
    31 CD := by simpa using congrArg Matrix.transpose c.CD
    32 DC := by simpa using congrArg Matrix.transpose c.DC
    33
    34theorem Change.injective (c : Change N) : Function.Injective c.C.mulVec := by
    35 intro x y h
    36 have h' := congrArg c.D.mulVec h
    37 simpa only [Matrix.mulVec_mulVec, c.DC, Matrix.one_mulVec] using h'
    38
    39theorem Change.dual_injective (c : Change N) : Function.Injective c.D.transpose.mulVec := by
    40 have hDC : c.C.transpose * c.D.transpose = 1 := by
    41 simpa using congrArg Matrix.transpose c.DC
    42 intro x y h
    43 have h' := congrArg c.C.transpose.mulVec h
    44 simpa only [Matrix.mulVec_mulVec, hDC, Matrix.one_mulVec] using h'
    45
    46def transform (c : Change N) {E : Matrix B B Binary} (F : Frame B H N E) :
    47 Frame B H N E where
    48 P := c.C * F.P
    49 Q := c.D.transpose * F.Q
    50 X := c.C * F.X
    51 Y := c.D.transpose * F.Y
    52 plus_injective := by
    53 intro x y h
    54 apply F.plus_injective
    55 apply c.injective
    56 simpa only [Matrix.mulVec_add, Matrix.mulVec_mulVec] using h
    57 minus_injective := by
    58 intro x y h
    59 apply F.minus_injective
    60 apply c.dual_injective
    61 simpa only [Matrix.mulVec_add, Matrix.mulVec_mulVec] using h
    62 gram := by
    63 have hCD : c.C.transpose * c.D.transpose = 1 := by
    64 simpa using congrArg Matrix.transpose c.DC
    65 simpa only [Matrix.transpose_mul, Matrix.mul_assoc, ← Matrix.mul_assoc c.C.transpose,
    66 hCD, Matrix.one_mul] using F.gram
    67 plus_annihilator := by
    68 have hCD : c.C.transpose * c.D.transpose = 1 := by
    69 simpa using congrArg Matrix.transpose c.DC
    70 simpa only [Matrix.transpose_mul, Matrix.mul_assoc, ← Matrix.mul_assoc c.C.transpose,
    71 hCD, Matrix.one_mul] using F.plus_annihilator
    72 minus_annihilator := by
    73 have hCD : c.C.transpose * c.D.transpose = 1 := by
    74 simpa using congrArg Matrix.transpose c.DC
    75 simpa only [Matrix.transpose_mul, Matrix.mul_assoc, ← Matrix.mul_assoc c.C.transpose,
    76 hCD, Matrix.one_mul] using F.minus_annihilator
    77
    78def frameEquiv (c : Change N) {E : Matrix B B Binary} : Frame B H N E ≃ Frame B H N E where
    79 toFun := transform c
    80 invFun := transform c.inv
    81 left_inv F := by
    82 apply frameData_injective
    83 have hCD : c.C.transpose * c.D.transpose = 1 := by
    84 simpa using congrArg Matrix.transpose c.DC
    85 simp [frameData, transform, Change.inv, ← Matrix.mul_assoc, c.DC, hCD]
    86 right_inv F := by
    87 apply frameData_injective
    88 have hDC : c.D.transpose * c.C.transpose = 1 := by
    89 simpa using congrArg Matrix.transpose c.CD
    90 simp [frameData, transform, Change.inv, ← Matrix.mul_assoc, c.CD, hDC]
    91
    92abbrev Injection (I N : Type) [Fintype I] :=
    93 {A : Matrix N I Binary // Function.Injective A.mulVec}
    94
    95noncomputable instance {I N : Type} [Fintype I] [Fintype N] :
    96 Fintype (Injection I N) := by classical exact Subtype.fintype _
    97
    98def plus {E : Matrix B B Binary} (F : Frame B H N E) : Injection (B ⊕ H) N :=
    99 ⟨Matrix.fromCols F.P F.X, by
    100 intro x y h
    101 have h' := F.plus_injective (a₁ := (x ∘ Sum.inl, x ∘ Sum.inr))
    102 (a₂ := (y ∘ Sum.inl, y ∘ Sum.inr)) (by simpa [Matrix.fromCols_mulVec] using h)
    103 funext i
    104 cases i with
    105 | inl b => exact congrFun (congrArg Prod.fst h') b
    106 | inr h => exact congrFun (congrArg Prod.snd h') h⟩
    107
    108def minus {E : Matrix B B Binary} (F : Frame B H N E) : Injection (B ⊕ H) N :=
    109 ⟨Matrix.fromCols F.Q F.Y, by
    110 intro x y h
    111 have h' := F.minus_injective (a₁ := (x ∘ Sum.inl, x ∘ Sum.inr))
    112 (a₂ := (y ∘ Sum.inl, y ∘ Sum.inr)) (by simpa [Matrix.fromCols_mulVec] using h)
    113 funext i
    114 cases i with
    115 | inl b => exact congrFun (congrArg Prod.fst h') b
    116 | inr h => exact congrFun (congrArg Prod.snd h') h⟩
    117
    118def plusChannel {E : Matrix B B Binary} (F : Frame B H N E) : Injection H N :=
    119 ⟨F.X, by
    120 intro x y h
    121 have he := F.plus_injective (a₁ := (0, x)) (a₂ := (0, y)) (by simpa using h)
    122 exact congrArg Prod.snd he⟩
    123
    124def minusChannel {E : Matrix B B Binary} (F : Frame B H N E) : Injection H N :=
    125 ⟨F.Y, by
    126 intro x y h
    127 have he := F.minus_injective (a₁ := (0, x)) (a₂ := (0, y)) (by simpa using h)
    128 exact congrArg Prod.snd he⟩
    129
    130axiom plus_uniform {E : Matrix B B Binary} [Nonempty (Frame B H N E)]
    131 [Nonempty (Injection (B ⊕ H) N)] :
    132 (PMF.uniformOfFintype (Frame B H N E)).map plus =
    133 PMF.uniformOfFintype (Injection (B ⊕ H) N)
    134
    135axiom minus_uniform {E : Matrix B B Binary} [Nonempty (Frame B H N E)]
    136 [Nonempty (Injection (B ⊕ H) N)] :
    137 (PMF.uniformOfFintype (Frame B H N E)).map minus =
    138 PMF.uniformOfFintype (Injection (B ⊕ H) N)
    139
    140axiom plusChannel_uniform {E : Matrix B B Binary} [Nonempty (Frame B H N E)]
    141 [Nonempty (Injection H N)] :
    142 (PMF.uniformOfFintype (Frame B H N E)).map plusChannel =
    143 PMF.uniformOfFintype (Injection H N)
    144
    145axiom minusChannel_uniform {E : Matrix B B Binary} [Nonempty (Frame B H N E)]
    146 [Nonempty (Injection H N)] :
    147 (PMF.uniformOfFintype (Frame B H N E)).map minusChannel =
    148 PMF.uniformOfFintype (Injection H N)
    149
    150axiom full_frame_orbit {E : Matrix B B Binary} (F G : Frame B H N E)
    151 (hchannel : F.X.transpose * F.Y = G.X.transpose * G.Y) :
    152 ∃ c : Change N, transform c F = G
    153
    154end Lax342547.FrameSymmetry
    155
    Show ProofShow ProofShow 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…