OAI/NumberTheory/Ostmann/Construction/ConstituentDiagonalSupport.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Exact bad/good splitting of the original-prior pivot diagonal

  1. theorem OAI.Ostmann.scheduledBadMatchingSet_subset line 12
  2. def OAI.Ostmann.scheduledGoodMatchingSet line 20
  3. def OAI.Ostmann.constituentMatchingFamily line 35
  4. theorem OAI.Ostmann.constituentCharacterCorrelation_cell_split line 44
  5. theorem OAI.Ostmann.constituentPivotDiagonal_cell_split line 78
  6. theorem OAI.Ostmann.constituentPivotDiagonal_average_split line 100