OAI/Combinatorics/HoneycombChords/ColumnExpansion.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

Column expansion for critical honeycomb strips.

The formulas follow the finite strip transfer calculation in the companion paper on uniform marked polygon estimates.

  1. def OAI.CriticalHoneycomb.Transfer.ListBound.marked line 14
  2. lemma OAI.CriticalHoneycomb.Transfer.ListBound.marked_nonnegative line 17
  3. lemma OAI.CriticalHoneycomb.Transfer.ListBound.weight_le_marked_encode line 26
  4. def OAI.CriticalHoneycomb.Transfer.ListBound.markTotal line 49
  5. lemma OAI.CriticalHoneycomb.Transfer.ListBound.sum_marked line 52
  6. lemma OAI.CriticalHoneycomb.Transfer.ListBound.finite_marked_system_bound line 62
  7. lemma OAI.CriticalHoneycomb.Transfer.ListBound.markTotal_limit line 84
  8. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.SelectedSystem.node_of_incident line 99
  9. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.Matches.nonempty_selected line 112
  10. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.SelectedSystem.nonempty_row line 137
  11. def OAI.CriticalHoneycomb.Transfer.RasterGrid.restrictedPartition line 153
  12. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.actual_restricted_component_bound line 158
  13. def OAI.CriticalHoneycomb.Transfer.RasterGrid.badHardWeight line 207
  14. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.badHardWeight_nonnegative line 211
  15. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.sum_badHardWeight_le line 216
  16. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.hardWeight_le_bad line 239
  17. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.markTotal_nonnegative line 250
  18. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.markTotal_mono line 255
  19. def OAI.CriticalHoneycomb.Transfer.RasterGrid.middleErrorBound line 264
  20. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.middleErrorBound_limit line 266
  21. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.actual_middle_row_bound line 269
  22. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.sourceR_PT line 318
  23. def OAI.CriticalHoneycomb.Transfer.RasterGrid.transposeWire line 322
  24. def OAI.CriticalHoneycomb.Transfer.RasterGrid.transposeSpins line 327
  25. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.physical_transpose line 329
  26. def OAI.CriticalHoneycomb.Transfer.RasterGrid.allGridPartition line 339
  27. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.prescribed_eq_allGrid line 346
  28. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.allGrid_transpose line 364
  29. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.prescribed_transpose line 383
  30. def OAI.CriticalHoneycomb.Transfer.RasterGrid.rowTransfer line 386
  31. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.prescribed_hard_transfer line 387
  32. def OAI.CriticalHoneycomb.Transfer.RasterGrid.transposeShape line 400
  33. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.transposeShape_involutive line 406
  34. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.transposeShape_visits line 407
  35. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.transposeShape_empty line 408
  36. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.occupied_symm line 409
  37. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.vacant_symm line 413
  38. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.shapeTensor_PT line 415
  39. def OAI.CriticalHoneycomb.Transfer.RasterGrid.transposeConfiguration line 428
  40. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.orientation_transpose line 430
  41. def OAI.CriticalHoneycomb.Transfer.RasterGrid.allChosenGrid line 441
  42. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.chosen_eq_allGrid line 448
  43. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.chosen_transpose line 466
  44. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.sum_visits_transpose line 487
  45. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.weighted_chosen_transpose line 491