OAI/Combinatorics/HadwigerCounterexample/FlatLevelShifts.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Flat Level Shifts

  1. theorem OAI.HadwigerCounterexample.shift_factors line 16

    Source documentation

    Shift a P row to an X t row. If the Gram comparisons obey Boolean monomial identities, there are coordinate factors of H for which both the left and the right row arrays diagonalize all these shifts.

    theorem shift_factors [DecidableEq J] (P : Mat I J) (H : Mat J J)
    (hP : Function.Injective P.mulVec) (hH : Function.Injective H.mulVec)
    (X : Q → Mat I J)
    (h1 : ∀ a, X a * H * Pᵀ = P * H * (X a)ᵀ)
    (h2 : ∀ a b, X a * H * (X b)ᵀ = X b * H * (X a)ᵀ)
    (h3 : ∀ a, X a * H * (X a)ᵀ = X a * H * Pᵀ) :
    ∃ (K C : Mat J J) (f : Q → J → F), H = K * Cᵀ ∧
      ∀ a, X a * C = P * C * diagonal (f a) ∧ X a * K = P * K * diagonal (f a) := by
…

    Mentions: OAI.HadwigerCounterexample.Mat, OAI.HadwigerCounterexample.F