Lax Lean Archive

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

Exact reference Gram-orbit marginals under injective affine restrictions

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

    An injective coefficient restriction of a uniform full paired Gram orbit has exactly the uniform prescribed slice law. The simultaneous ambient action preserves the full Gram and transports every restriction fiber.

    Concept map
    6 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax342547.FrameTuples
    2
    3/-!
    4---
    5title: Exact reference Gram-orbit marginals under injective affine restrictions
    6type: lemma
    7---
    8An injective coefficient restriction of a uniform full paired Gram orbit
    9has exactly the uniform prescribed slice law. The simultaneous ambient
    10action preserves the full Gram and transports every restriction fiber.
    11-/
    12
    13namespace Lax342547.OrbitSliceLaw
    14noncomputable section
    15open Lax342547.MomentSpace Lax342547.FrameSymmetry Lax342547.FrameTuples
    16open scoped BigOperators ENNReal
    17set_option backward.isDefEq.respectTransparency false
    18
    19
    20def restrictOrbit {B H I J N : Type} [Fintype B] [Fintype H]
    21 [Fintype I] [Fintype J] [Fintype N] (G : Matrix B H Binary)
    22 (C : Matrix B I Binary) (D : Matrix H J Binary)
    23 (hC : Function.Injective C.mulVec) (hD : Function.Injective D.mulVec)
    24 (z : Orbit N G) : Orbit N (C.transpose*G*D) :=
    25 ⟨(z.val.1*C,z.val.2*D),by
    26 refine ⟨?_,?_,?_⟩
    27 · intro x y hh
    28 apply hC
    29 apply z.property.1
    30 simpa only [Matrix.mulVec_mulVec] using hh
    31 · intro x y hh
    32 apply hD
    33 apply z.property.2.1
    34 simpa only [Matrix.mulVec_mulVec] using hh
    35 · simp only [Matrix.transpose_mul,Matrix.mul_assoc]
    36 rw [← Matrix.mul_assoc z.val.1.transpose,z.property.2.2]⟩
    37
    38def changeOrbit {B H N : Type} [Fintype B] [Fintype H] [Fintype N] [DecidableEq N]
    39 (c : Change N) (G : Matrix B H Binary) (z : Orbit N G) : Orbit N G :=
    40 ⟨(c.C*z.val.1,c.D.transpose*z.val.2),by
    41 refine ⟨?_,?_,?_⟩
    42 · intro x y hh
    43 apply z.property.1
    44 apply c.injective
    45 simpa only [Matrix.mulVec_mulVec] using hh
    46 · intro x y hh
    47 apply z.property.2.1
    48 apply c.dual_injective
    49 simpa only [Matrix.mulVec_mulVec] using hh
    50 · have he : c.C.transpose*c.D.transpose = 1 := by simpa using congrArg Matrix.transpose c.DC
    51 simp only [Matrix.transpose_mul,Matrix.mul_assoc,← Matrix.mul_assoc c.C.transpose,
    52 he,Matrix.one_mul,z.property.2.2]⟩
    53
    54def orbitEquiv {B H N : Type} [Fintype B] [Fintype H] [Fintype N] [DecidableEq N]
    55 (c : Change N) (G : Matrix B H Binary) : Orbit N G ≃ Orbit N G where
    56 toFun := changeOrbit c G
    57 invFun := changeOrbit c.inv G
    58 left_inv z := by
    59 apply Subtype.ext
    60 have he : c.C.transpose*c.D.transpose = 1 := by simpa using congrArg Matrix.transpose c.DC
    61 apply Prod.ext <;> simp [changeOrbit,Change.inv,← Matrix.mul_assoc,c.DC,he]
    62 right_inv z := by
    63 apply Subtype.ext
    64 have he : c.D.transpose*c.C.transpose = 1 := by simpa using congrArg Matrix.transpose c.CD
    65 apply Prod.ext <;> simp [changeOrbit,Change.inv,← Matrix.mul_assoc,c.CD,he]
    66
    67axiom slice_uniform {B H I J N : Type} [Fintype B] [Fintype H]
    68 [Fintype I] [Fintype J] [Fintype N] [DecidableEq N]
    69 (G : Matrix B H Binary) [Nonempty (Orbit N G)]
    70 (C : Matrix B I Binary) (D : Matrix H J Binary)
    71 (hC : Function.Injective C.mulVec) (hD : Function.Injective D.mulVec)
    72 [Nonempty (Orbit N (C.transpose*G*D))] :
    73 (PMF.uniformOfFintype (Orbit N G)).map (restrictOrbit G C D hC hD) =
    74 PMF.uniformOfFintype (Orbit N (C.transpose*G*D))
    75
    76end
    77end Lax342547.OrbitSliceLaw
    78
    Show Proof
    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…