Lax Lean Archive

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

Uniform tuple images on prescribed Gram orbits

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

    Independent primal coefficient tuples have the uniform law on their individually injective realizations with prescribed Gram. Tuples using channels have the analogous law after conditioning on the self-channel Gram, including singular Gram matrices and arbitrary tuple dimensions.

    Concept map
    5 concepts
    100%
    Proven claimDefinitionThis 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 full_product proven

    2 full_uniform proven

    3 primal_family proven

    4 primal_product proven

    5 primal_uniform proven

    6 raw_full_conditioning proven

    Lean source view on GitHub

    1import Lax342547.FrameSymmetry
    2
    3/-!
    4---
    5title: Uniform tuple images on prescribed Gram orbits
    6type: lemma
    7---
    8Independent primal coefficient tuples have the uniform law on their
    9individually injective realizations with prescribed Gram. Tuples using
    10channels have the analogous law after conditioning on the self-channel
    11Gram, including singular Gram matrices and arbitrary tuple dimensions.
    12-/
    13
    14namespace Lax342547.FrameTuples
    15
    16open Lax342547.MomentSpace Lax342547.RawFrames Lax342547.FrameSymmetry
    17
    18abbrev Orbit {I J : Type} (N : Type) [Fintype I] [Fintype J] [Fintype N]
    19 (G : Matrix I J Binary) :=
    20 {z : Matrix N I Binary × Matrix N J Binary //
    21 Function.Injective z.1.mulVec ∧ Function.Injective z.2.mulVec ∧ z.1.transpose * z.2 = G}
    22
    23noncomputable instance {I J N : Type} [Fintype I] [Fintype J] [Fintype N]
    24 (G : Matrix I J Binary) : Fintype (Orbit N G) := by classical exact Subtype.fintype _
    25
    26variable {B H I J N : Type} [Fintype B] [Fintype H] [Fintype I] [Fintype J] [Fintype N]
    27
    28def primalTuple {E : Matrix B B Binary} (C : Matrix B I Binary) (D : Matrix B J Binary)
    29 (hC : Function.Injective C.mulVec) (hD : Function.Injective D.mulVec)
    30 (F : Frame B H N E) : Orbit N (C.transpose * E * D) :=
    31 ⟨(F.P * C, F.Q * D), by
    32 refine ⟨?_, ?_, ?_⟩
    33 · intro x y h
    34 apply hC
    35 have he := F.plus_injective (a₁ := (C.mulVec x, 0)) (a₂ := (C.mulVec y, 0))
    36 (by simpa only [Matrix.mulVec_zero, add_zero, Matrix.mulVec_mulVec] using h)
    37 exact congrArg Prod.fst he
    38 · intro x y h
    39 apply hD
    40 have he := F.minus_injective (a₁ := (D.mulVec x, 0)) (a₂ := (D.mulVec y, 0))
    41 (by simpa only [Matrix.mulVec_zero, add_zero, Matrix.mulVec_mulVec] using h)
    42 exact congrArg Prod.fst he
    43 · calc
    44 _ = C.transpose * (F.P.transpose * F.Q) * D := by
    45 simp only [Matrix.transpose_mul, Matrix.mul_assoc]
    46 _ = _ := by rw [F.gram]⟩
    47
    48def fullGram (E : Matrix B B Binary) (G : Matrix H H Binary) : Matrix (B ⊕ H) (B ⊕ H) Binary :=
    49 Matrix.fromBlocks E 0 0 G
    50
    51abbrev ChannelFiber (E : Matrix B B Binary) (G : Matrix H H Binary) :=
    52 {F : Frame B H N E // F.X.transpose * F.Y = G}
    53
    54noncomputable instance (E : Matrix B B Binary) (G : Matrix H H Binary) :
    55 Fintype (ChannelFiber (N := N) E G) := by classical exact Subtype.fintype _
    56
    57theorem combined_gram {E : Matrix B B Binary} (F : Frame B H N E) :
    58 (plus F).val.transpose * (minus F).val = fullGram E (F.X.transpose * F.Y) := by
    59 simp only [plus, minus, Matrix.transpose_fromCols, Matrix.fromRows_mul_fromCols,
    60 F.gram, F.plus_annihilator, F.minus_annihilator, fullGram]
    61
    62def fullTuple {E : Matrix B B Binary} {G : Matrix H H Binary}
    63 (C : Matrix (B ⊕ H) I Binary) (D : Matrix (B ⊕ H) J Binary)
    64 (hC : Function.Injective C.mulVec) (hD : Function.Injective D.mulVec)
    65 (F : ChannelFiber (N := N) E G) : Orbit N (C.transpose * fullGram E G * D) :=
    66 ⟨((plus F.val).val * C, (minus F.val).val * D), by
    67 refine ⟨?_, ?_, ?_⟩
    68 · intro x y h
    69 apply hC
    70 apply (plus F.val).property
    71 simpa only [Matrix.mulVec_mulVec] using h
    72 · intro x y h
    73 apply hD
    74 apply (minus F.val).property
    75 simpa only [Matrix.mulVec_mulVec] using h
    76 · calc
    77 _ = C.transpose * ((plus F.val).val.transpose * (minus F.val).val) * D := by
    78 simp only [Matrix.transpose_mul, Matrix.mul_assoc]
    79 _ = _ := by rw [combined_gram, F.property]⟩
    80
    81axiom primal_uniform [DecidableEq N] {E : Matrix B B Binary} [Nonempty (Frame B H N E)]
    82 (C : Matrix B I Binary) (D : Matrix B J Binary)
    83 (hC : Function.Injective C.mulVec) (hD : Function.Injective D.mulVec)
    84 [Nonempty (Orbit N (C.transpose * E * D))] :
    85 (PMF.uniformOfFintype (Frame B H N E)).map (primalTuple C D hC hD) =
    86 PMF.uniformOfFintype (Orbit N (C.transpose * E * D))
    87
    88axiom full_uniform [DecidableEq N] {E : Matrix B B Binary} {G : Matrix H H Binary}
    89 [Nonempty (ChannelFiber (N := N) E G)]
    90 (C : Matrix (B ⊕ H) I Binary) (D : Matrix (B ⊕ H) J Binary)
    91 (hC : Function.Injective C.mulVec) (hD : Function.Injective D.mulVec)
    92 [Nonempty (Orbit N (C.transpose * fullGram E G * D))] :
    93 (PMF.uniformOfFintype (ChannelFiber (N := N) E G)).map (fullTuple C D hC hD) =
    94 PMF.uniformOfFintype (Orbit N (C.transpose * fullGram E G * D))
    95
    96axiom raw_full_conditioning [DecidableEq N] {E : Matrix B B Binary} {G : Matrix H H Binary}
    97 [Nonempty (Frame B H N E)] [Nonempty (ChannelFiber (N := N) E G)]
    98 (C : Matrix (B ⊕ H) I Binary) (D : Matrix (B ⊕ H) J Binary)
    99 (hC : Function.Injective C.mulVec) (hD : Function.Injective D.mulVec)
    100 [Nonempty (Orbit N (C.transpose * fullGram E G * D))]
    101 (h : ∃ F ∈ {F : Frame B H N E | F.X.transpose * F.Y = G},
    102 F ∈ (PMF.uniformOfFintype (Frame B H N E)).support) :
    103 ((PMF.uniformOfFintype (Frame B H N E)).filter {F | F.X.transpose * F.Y = G} h).map
    104 (fun F => ((plus F).val * C, (minus F).val * D)) =
    105 (PMF.uniformOfFintype (Orbit N (C.transpose * fullGram E G * D))).map Subtype.val
    106
    107axiom primal_product {Draw : Type} [Fintype Draw] [DecidableEq Draw] [DecidableEq N]
    108 {E : Matrix B B Binary} [Nonempty (Frame B H N E)]
    109 (C : Draw → Matrix B I Binary) (D : Draw → Matrix B J Binary)
    110 (hC : ∀ s, Function.Injective (C s).mulVec) (hD : ∀ s, Function.Injective (D s).mulVec)
    111 [∀ s, Nonempty (Orbit N ((C s).transpose * E * D s))]
    112 (z : Draw → Matrix N I Binary × Matrix N J Binary) :
    113 (PMF.uniformOfFintype (Draw → Frame B H N E)).map
    114 (fun o s => ((o s).P * C s, (o s).Q * D s)) z =
    115 ∏ s, (PMF.uniformOfFintype (Orbit N ((C s).transpose * E * D s))).map Subtype.val (z s)
    116
    117axiom primal_family {Draw : Type} [Fintype Draw] [DecidableEq Draw] [DecidableEq N]
    118 {K L : Draw → Type} [∀ s, Fintype (K s)] [∀ s, Fintype (L s)]
    119 {E : Matrix B B Binary} [Nonempty (Frame B H N E)]
    120 (C : ∀ s, Matrix B (K s) Binary) (D : ∀ s, Matrix B (L s) Binary)
    121 (hC : ∀ s, Function.Injective (C s).mulVec) (hD : ∀ s, Function.Injective (D s).mulVec)
    122 [∀ s, Nonempty (Orbit N ((C s).transpose * E * D s))]
    123 (z : ∀ s, Matrix N (K s) Binary × Matrix N (L s) Binary) :
    124 (PMF.uniformOfFintype (Draw → Frame B H N E)).map
    125 (fun o s => ((o s).P * C s, (o s).Q * D s)) z =
    126 ∏ s, (PMF.uniformOfFintype (Orbit N ((C s).transpose * E * D s))).map Subtype.val (z s)
    127
    128axiom full_product {Draw : Type} [Fintype Draw] [DecidableEq Draw] [DecidableEq N]
    129 {K L : Draw → Type} [∀ s, Fintype (K s)] [∀ s, Fintype (L s)]
    130 {E : Matrix B B Binary} (G : Draw → Matrix H H Binary)
    131 [∀ s, Nonempty (ChannelFiber (N := N) E (G s))]
    132 (C : ∀ s, Matrix (B ⊕ H) (K s) Binary) (D : ∀ s, Matrix (B ⊕ H) (L s) Binary)
    133 (hC : ∀ s, Function.Injective (C s).mulVec) (hD : ∀ s, Function.Injective (D s).mulVec)
    134 [∀ s, Nonempty (Orbit N ((C s).transpose * fullGram E (G s) * D s))]
    135 (z : ∀ s, Matrix N (K s) Binary × Matrix N (L s) Binary) :
    136 (PMF.uniformOfFintype (∀ s, ChannelFiber (N := N) E (G s))).map
    137 (fun o s => ((plus (o s).val).val * C s, (minus (o s).val).val * D s)) z =
    138 ∏ s, (PMF.uniformOfFintype (Orbit N ((C s).transpose * fullGram E (G s) * D s))).map
    139 Subtype.val (z s)
    140
    141end Lax342547.FrameTuples
    142
    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…