Lax Lean Archive

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

Independent nominal affine slices from the free block

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

    Two affine maps have the same constant-coordinate value on their translation columns. Subtracting those columns leaves an independent uniform free matrix with 2d+1 columns. This pays nominal dependence without falsely identifying the two translation directions.

    Concept map
    11 concepts; 8 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

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

    1 affine_pair_failure proven

    2 joinedFree_uniform proven

    3 pairMap_injective_of_joined proven

    4 point_gram_ignores_free proven

    5 point_gram_setFree proven

    6 point_pair_failure proven

    7 point_pair_independent proven

    8 pointColumns_eraseFree proven

    Lean source view on GitHub

    1import Lax342547.GramNormalization
    2import Lax342547.ConcreteGeometry
    3
    4/-!
    5---
    6title: Independent nominal affine slices from the free block
    7type: lemma
    8---
    9Two affine maps have the same constant-coordinate value on their translation
    10columns. Subtracting those columns leaves an independent uniform free matrix
    11with 2d+1 columns. This pays nominal dependence without falsely identifying
    12the two translation directions.
    13-/
    14
    15namespace Lax342547.AffineSliceIndependence
    16
    17open Lax342547.MomentSpace Lax342547.TagGeometry Lax342547.ConcreteGeometry
    18open scoped ENNReal
    19
    20def affineColumns {D N : Type} (Z : Matrix N (Option D) Binary) :
    21 Matrix (Option N) (Option D) Binary
    22 | none,none => 1
    23 | none,some _ => 0
    24 | some n,j => Z n j
    25
    26def joinedFree {D N : Type} (Z : Matrix N (Option D) Binary × Matrix N (Option D) Binary) :
    27 Matrix N (Option (D ⊕ D)) Binary
    28 | n,none => Z.1 n none+Z.2 n none
    29 | n,some (Sum.inl d) => Z.1 n (some d)
    30 | n,some (Sum.inr d) => Z.2 n (some d)
    31
    32def joinedFreeMap {D N : Type} :
    33 (Matrix N (Option D) Binary × Matrix N (Option D) Binary) →ₗ[Binary]
    34 Matrix N (Option (D ⊕ D)) Binary where
    35 toFun := joinedFree
    36 map_add' Z W := by
    37 ext n j
    38 cases j with
    39 | some j => cases j <;> rfl
    40 | none => change (Z.1 n none+W.1 n none)+(Z.2 n none+W.2 n none) =
    41 (Z.1 n none+Z.2 n none)+(W.1 n none+W.2 n none)
    42 ring
    43 map_smul' c Z := by
    44 ext n j
    45 cases j with
    46 | some j => cases j <;> rfl
    47 | none => change c*(Z.1 n none)+c*(Z.2 n none) = c*(Z.1 n none+Z.2 n none)
    48 ring
    49
    50def pairMap {D N : Type} [Fintype D] (Z : Matrix N (Option D) Binary × Matrix N (Option D) Binary) :
    51 ((Option D → Binary) × (Option D → Binary)) →ₗ[Binary] (Option N → Binary) where
    52 toFun v := (affineColumns Z.1).mulVec v.1+(affineColumns Z.2).mulVec v.2
    53 map_add' _ _ := by simp only [Prod.fst_add,Prod.snd_add,Matrix.mulVec_add]; abel
    54 map_smul' c v := by
    55 change (affineColumns Z.1).mulVec (c • v.1)+(affineColumns Z.2).mulVec (c • v.2) = _
    56 simp [Matrix.mulVec_smul,smul_add]
    57
    58axiom pairMap_injective_of_joined {D N : Type} [Fintype D] [Fintype N]
    59 (Z : Matrix N (Option D) Binary × Matrix N (Option D) Binary)
    60 (hZ : Function.Injective (joinedFree Z).mulVec) : Function.Injective (pairMap Z)
    61
    62axiom joinedFree_uniform {D N : Type} [Fintype D] [Fintype N] [DecidableEq D] [DecidableEq N] :
    63 (PMF.uniformOfFintype (Matrix N (Option D) Binary × Matrix N (Option D) Binary)).map joinedFree =
    64 PMF.uniformOfFintype (Matrix N (Option (D ⊕ D)) Binary)
    65
    66axiom affine_pair_failure {D N : Type} [Fintype D] [Fintype N] [DecidableEq D] [DecidableEq N] :
    67 (PMF.uniformOfFintype (Matrix N (Option D) Binary × Matrix N (Option D) Binary)).toOuterMeasure
    68 {Z | ¬ Function.Injective (pairMap Z)} ≤
    69 (2 : ℝ≥0∞)^(2*Fintype.card D+1)/(2 : ℝ≥0∞)^Fintype.card N
    70
    71/-- Coefficients of the actual affine point map at a fixed selector. -/
    72def pointColumns {k n b degree : ℕ} {D : Type} (s : Fin b → Binary)
    73 (V : Matrix (Base k n) (Option D) Binary) : Matrix (Coordinate k n b degree) (Option D) Binary :=
    74 fun c j => selectorEval s c.1 * match c.2 with
    75 | none => match j with | none => 1 | some _ => 0
    76 | some a => V a j
    77
    78def freePart {k n : ℕ} {D : Type} (V : Matrix (Base k n) (Option D) Binary) :
    79 Matrix (Fin n) (Option D) Binary := fun i j => V (free i) j
    80
    81def eraseFree {k n : ℕ} {D : Type} (V : Matrix (Base k n) (Option D) Binary) :
    82 Matrix (Base k n) (Option D) Binary
    83 | Sum.inr (q,i),j => if q = 2 then 0 else V (Sum.inr (q,i)) j
    84 | Sum.inl a,j => V (Sum.inl a) j
    85
    86def setFree {k n : ℕ} {D : Type} (V : Matrix (Base k n) (Option D) Binary)
    87 (Z : Matrix (Fin n) (Option D) Binary) : Matrix (Base k n) (Option D) Binary
    88 | Sum.inr (q,i),j => if q = 2 then Z i j else V (Sum.inr (q,i)) j
    89 | Sum.inl a,j => V (Sum.inl a) j
    90
    91axiom point_pair_independent {k n b degree : ℕ} {D : Type} [Fintype D]
    92 (s : Fin b → Binary) (V W : Matrix (Base k n) (Option D) Binary)
    93 (hZ : Function.Injective (joinedFree (freePart V,freePart W)).mulVec) :
    94 Function.Injective (fun uv : (Option D → Binary) × (Option D → Binary) =>
    95 (pointColumns (degree := degree) s V).mulVec uv.1+
    96 (pointColumns (degree := degree) s W).mulVec uv.2)
    97
    98axiom pointColumns_eraseFree {k n b degree : ℕ} {D : Type} [Fintype D]
    99 (s : Fin b → Binary) (V : Matrix (Base k n) (Option D) Binary) :
    100 (changeZ (0 : Matrix (Fin n) (Fin n) Binary)).toMatrix' * pointColumns (degree := degree) s V =
    101 pointColumns s (eraseFree V)
    102
    103axiom point_gram_ignores_free {k n b degree r : ℕ} {D : Type} [Fintype D]
    104 (hr : 2*r ≤ n) (hd : 1 ≤ degree) (M : Fin b → Matrix (Fin n) (Fin n) Binary)
    105 (s : Fin b → Binary) (V W : Matrix (Base k n) (Option D) Binary) :
    106 (pointColumns s V).transpose*selfGram hr hd M*pointColumns s W =
    107 (pointColumns s (eraseFree V)).transpose*selfGram hr hd M*pointColumns s (eraseFree W)
    108
    109axiom point_gram_setFree {k n b degree r : ℕ} {D : Type} [Fintype D]
    110 (hr : 2*r ≤ n) (hd : 1 ≤ degree) (M : Fin b → Matrix (Fin n) (Fin n) Binary)
    111 (s : Fin b → Binary) (V W : Matrix (Base k n) (Option D) Binary)
    112 (Z T : Matrix (Fin n) (Option D) Binary) :
    113 (pointColumns s (setFree V Z)).transpose*selfGram hr hd M*pointColumns s (setFree W T) =
    114 (pointColumns s V).transpose*selfGram hr hd M*pointColumns s W
    115
    116axiom point_pair_failure {k n b degree : ℕ} {D : Type} [Fintype D] [DecidableEq D]
    117 (s : Fin b → Binary) (V W : Matrix (Base k n) (Option D) Binary) :
    118 (PMF.uniformOfFintype (Matrix (Fin n) (Option D) Binary × Matrix (Fin n) (Option D) Binary)).toOuterMeasure
    119 {Z | ¬ Function.Injective (fun uv : (Option D → Binary) × (Option D → Binary) =>
    120 (pointColumns (degree := degree) s (setFree V Z.1)).mulVec uv.1+
    121 (pointColumns (degree := degree) s (setFree W Z.2)).mulVec uv.2)} ≤
    122 (2 : ℝ≥0∞)^(2*Fintype.card D+1)/(2 : ℝ≥0∞)^n
    123
    124end Lax342547.AffineSliceIndependence
    125
    Show ProofShow ProofShow 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…