OAI/Combinatorics/StripMass/AugmentedColumn.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. def OAI.CriticalStrip.Diagram.northInjectionWeights line 17
  2. def OAI.CriticalStrip.Diagram.sourceFullSplit line 19
  3. lemma OAI.CriticalStrip.Diagram.sourceFullSplit_inl line 42
  4. lemma OAI.CriticalStrip.Diagram.sourceFullSplit_inr line 44
  5. def OAI.CriticalStrip.Diagram.augmentVector line 47
  6. lemma OAI.CriticalStrip.Diagram.augmentVector_split line 50
  7. lemma OAI.CriticalStrip.Diagram.augmentVector_padTop line 55
  8. lemma OAI.CriticalStrip.Diagram.augmentVector_source line 58
  9. lemma OAI.CriticalStrip.Diagram.augmentVector_empty line 61
  10. lemma OAI.CriticalStrip.Diagram.column_last_factor line 65
  11. lemma OAI.CriticalStrip.Diagram.northInjection_column_blocks line 75
  12. lemma OAI.CriticalStrip.Diagram.augmentVector_stationary line 92
  13. def OAI.CriticalStrip.Diagram.angleAugmented line 119
  14. lemma OAI.CriticalStrip.Diagram.angleAugmented_restricted_stationary line 122
  15. lemma OAI.CriticalStrip.Diagram.continuousOn_angleAugmented line 135
  16. def OAI.CriticalStrip.Diagram.ColumnChain.weight line 161
  17. lemma OAI.CriticalStrip.Diagram.ColumnChain.weighted_runs_cons line 165
  18. def OAI.CriticalStrip.Diagram.ColumnChain.mass line 188
  19. lemma OAI.CriticalStrip.Diagram.ColumnChain.mass_zero line 191
  20. lemma OAI.CriticalStrip.Diagram.ColumnChain.mass_succ line 195
  21. lemma OAI.CriticalStrip.Diagram.ColumnChain.mass_eq_pow line 216
  22. lemma OAI.CriticalStrip.Diagram.ColumnChain.weight_head_ne_zero line 233
  23. lemma OAI.CriticalStrip.Diagram.ColumnChain.weight_tail_ne_zero line 239
  24. theorem OAI.CriticalStrip.Diagram.ColumnChain.north_shape line 245
  25. lemma OAI.CriticalStrip.Diagram.ColumnChain.north_birth_unique_shape line 280
  26. theorem OAI.CriticalStrip.Diagram.ColumnChain.north_birth_exists_unique line 300
  27. def OAI.CriticalStrip.Diagram.ColumnChain.read line 327
  28. lemma OAI.CriticalStrip.Diagram.ColumnChain.read_nil line 330
  29. lemma OAI.CriticalStrip.Diagram.ColumnChain.read_cons_zero line 332
  30. lemma OAI.CriticalStrip.Diagram.ColumnChain.read_cons_succ line 334
  31. lemma OAI.CriticalStrip.Diagram.ColumnChain.read_ge line 337
  32. lemma OAI.CriticalStrip.Diagram.ColumnChain.read_entries line 341
  33. lemma OAI.CriticalStrip.Diagram.ColumnChain.support_empty_read line 350
  34. structure OAI.CriticalStrip.Diagram.ColumnChain.LocallyCompatible line 358
  35. lemma OAI.CriticalStrip.Diagram.ColumnChain.compatible_empty_iff line 365
  36. lemma OAI.CriticalStrip.Diagram.ColumnChain.read_tile_ne_zero line 400
  37. lemma OAI.CriticalStrip.PositiveMatrix.submatrix_pow_equiv line 424
  38. lemma OAI.CriticalStrip.PositiveMatrix.SummablePowers.reindex line 430
  39. lemma OAI.CriticalStrip.PositiveMatrix.summablePowers_reindex_iff line 435
  40. lemma OAI.CriticalStrip.PositiveMatrix.SummablePowers.fromBlocks_zero_right line 446
  41. lemma OAI.CriticalStrip.PositiveMatrix.summablePowers_of_zero_cols line 477