Lax Lean Archive

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

The affine minus-column law at a fixed plus frame

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

    With P,X fixed, the Q columns have prescribed evaluations against [P,X] and the Y columns have zero evaluations against P. These two independent affine column families are conditioned only on joint minus injectivity. The failure probability before that conditioning is at most 2^(2(d+h)-N).

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

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

    1 completion_event_bound proven

    2 conditional_uniform proven

    3 rank_failure proven

    4 raw_conditioning proven

    Lean source view on GitHub

    1import Lax342547.FrameSymmetry
    2import Lax342547.GramColumns
    3
    4/-!
    5---
    6title: The affine minus-column law at a fixed plus frame
    7type: lemma
    8---
    9With P,X fixed, the Q columns have prescribed evaluations against [P,X]
    10and the Y columns have zero evaluations against P. These two independent
    11affine column families are conditioned only on joint minus injectivity.
    12The failure probability before that conditioning is at most 2^(2(d+h)-N).
    13-/
    14
    15namespace Lax342547.ConditionalMinus
    16
    17open Lax342547.MomentSpace Lax342547.RawFrames Lax342547.GramColumns
    18open scoped ENNReal
    19
    20variable {B H N : Type} [Fintype B] [Fintype H] [Fintype N]
    21
    22abbrev ColumnProduct (E : Matrix B B Binary) (P : Matrix N B Binary) (X : Matrix N H Binary) :=
    23 GramFiber (Matrix.fromCols P X) (Matrix.fromRows E 0) × GramFiber P (0 : Matrix B H Binary)
    24
    25def Good {E : Matrix B B Binary} {P : Matrix N B Binary} {X : Matrix N H Binary}
    26 (z : ColumnProduct E P X) : Prop :=
    27 Function.Injective (fun w : (B → Binary) × (H → Binary) =>
    28 z.1.val.mulVec w.1 + z.2.val.mulVec w.2)
    29
    30abbrev Completion (E : Matrix B B Binary) (P : Matrix N B Binary) (X : Matrix N H Binary) :=
    31 {z : ColumnProduct E P X // Good z}
    32
    33abbrev Fiber (E : Matrix B B Binary) (P : Matrix N B Binary) (X : Matrix N H Binary) :=
    34 {F : Frame B H N E // F.P = P ∧ F.X = X}
    35
    36noncomputable instance (E : Matrix B B Binary) (P : Matrix N B Binary) (X : Matrix N H Binary) :
    37 Fintype (Completion E P X) := by classical exact Subtype.fintype _
    38
    39noncomputable instance (E : Matrix B B Binary) (P : Matrix N B Binary) (X : Matrix N H Binary) :
    40 Fintype (Fiber E P X) := by classical exact Subtype.fintype _
    41
    42omit [Fintype N] in
    43theorem combined_injective_iff (P : Matrix N B Binary) (X : Matrix N H Binary) :
    44 Function.Injective (Matrix.fromCols P X).mulVec ↔
    45 Function.Injective (fun z : (B → Binary) × (H → Binary) => P.mulVec z.1 + X.mulVec z.2) := by
    46 constructor
    47 · intro h z w he
    48 have h' := h (a₁ := Sum.elim z.1 z.2) (a₂ := Sum.elim w.1 w.2)
    49 (by simpa only [Matrix.fromCols_mulVec_sumElim] using he)
    50 exact Prod.ext (funext (fun b => congrFun h' (Sum.inl b)))
    51 (funext (fun j => congrFun h' (Sum.inr j)))
    52 · intro h z w he
    53 have h' := h (a₁ := (z ∘ Sum.inl, z ∘ Sum.inr)) (a₂ := (w ∘ Sum.inl, w ∘ Sum.inr))
    54 (by simpa only [Matrix.fromCols_mulVec] using he)
    55 funext j
    56 cases j with
    57 | inl b => exact congrFun (congrArg Prod.fst h') b
    58 | inr j => exact congrFun (congrArg Prod.snd h') j
    59
    60def columns {E : Matrix B B Binary} {P : Matrix N B Binary} {X : Matrix N H Binary}
    61 (F : Fiber E P X) : Completion E P X :=
    62 ⟨(⟨F.val.Q, by
    63 simp only [← F.property.1, ← F.property.2, Matrix.transpose_fromCols,
    64 Matrix.fromRows_mul, F.val.gram, F.val.plus_annihilator]⟩,
    65 ⟨F.val.Y, by simpa only [← F.property.1] using F.val.minus_annihilator⟩), F.val.minus_injective⟩
    66
    67def assemble {E : Matrix B B Binary} {P : Matrix N B Binary} {X : Matrix N H Binary}
    68 (hPX : Function.Injective (Matrix.fromCols P X).mulVec) (z : Completion E P X) : Fiber E P X :=
    69 ⟨{ P := P, X := X, Q := z.val.1.val, Y := z.val.2.val,
    70 plus_injective := (combined_injective_iff P X).mp hPX,
    71 minus_injective := z.property,
    72 gram := (Matrix.fromRows_inj (by
    73 simpa only [Matrix.transpose_fromCols, Matrix.fromRows_mul] using z.val.1.property)).1,
    74 plus_annihilator := (Matrix.fromRows_inj (by
    75 simpa only [Matrix.transpose_fromCols, Matrix.fromRows_mul] using z.val.1.property)).2,
    76 minus_annihilator := z.val.2.property }, rfl, rfl⟩
    77
    78def completionEquiv {E : Matrix B B Binary} {P : Matrix N B Binary} {X : Matrix N H Binary}
    79 (hPX : Function.Injective (Matrix.fromCols P X).mulVec) : Fiber E P X ≃ Completion E P X where
    80 toFun := columns
    81 invFun := assemble hPX
    82 left_inv F := by
    83 apply Subtype.ext
    84 apply frameData_injective
    85 exact Prod.ext F.property.1.symm (Prod.ext rfl (Prod.ext F.property.2.symm rfl))
    86 right_inv z := by cases z; rfl
    87
    88axiom conditional_uniform {E : Matrix B B Binary} {P : Matrix N B Binary} {X : Matrix N H Binary}
    89 (hPX : Function.Injective (Matrix.fromCols P X).mulVec)
    90 [Nonempty (Fiber E P X)] [Nonempty (Completion E P X)] :
    91 (PMF.uniformOfFintype (Fiber E P X)).map columns = PMF.uniformOfFintype (Completion E P X)
    92
    93axiom rank_failure [DecidableEq B] [DecidableEq H] [DecidableEq N]
    94 (E : Matrix B B Binary) (P : Matrix N B Binary) (X : Matrix N H Binary)
    95 (hPX : Function.Injective (Matrix.fromCols P X).mulVec) [Nonempty (ColumnProduct E P X)] :
    96 (PMF.uniformOfFintype (ColumnProduct E P X)).toOuterMeasure {z | ¬ Good z} ≤
    97 (2 : ℝ≥0∞) ^ (2 * (Fintype.card B + Fintype.card H)) / 2 ^ Fintype.card N
    98
    99axiom raw_conditioning {E : Matrix B B Binary} {P : Matrix N B Binary} {X : Matrix N H Binary}
    100 (hPX : Function.Injective (Matrix.fromCols P X).mulVec)
    101 [Nonempty (Frame B H N E)] [Nonempty (Fiber E P X)] [Nonempty (Completion E P X)]
    102 (h : ∃ F ∈ {F : Frame B H N E | F.P = P ∧ F.X = X},
    103 F ∈ (PMF.uniformOfFintype (Frame B H N E)).support) :
    104 ((PMF.uniformOfFintype (Frame B H N E)).filter {F | F.P = P ∧ F.X = X} h).map
    105 (fun F => (F.Q, F.Y)) =
    106 (PMF.uniformOfFintype (Completion E P X)).map (fun z => (z.val.1.val, z.val.2.val))
    107
    108axiom completion_event_bound [DecidableEq B] [DecidableEq H] [DecidableEq N]
    109 (E : Matrix B B Binary) (P : Matrix N B Binary) (X : Matrix N H Binary)
    110 (hPX : Function.Injective (Matrix.fromCols P X).mulVec)
    111 [Nonempty (ColumnProduct E P X)] [Nonempty (Completion E P X)]
    112 (hN : 2 * (Fintype.card B + Fintype.card H) + 1 ≤ Fintype.card N)
    113 (S : Set (ColumnProduct E P X)) :
    114 (PMF.uniformOfFintype (Completion E P X)).toOuterMeasure {z | z.val ∈ S} ≤
    115 2 * (PMF.uniformOfFintype (ColumnProduct E P X)).toOuterMeasure S
    116
    117end Lax342547.ConditionalMinus
    118
    Show 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…