OAI/Combinatorics/HoneycombChords/ColumnProjection.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Column projection for critical honeycomb strips.

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

  1. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.matrixPath_sum line 14
  2. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.matrixPath_scale line 22
  3. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.matrixPath_restrict line 32
  4. def OAI.CriticalHoneycomb.Transfer.RasterGrid.weightedColumn line 46
  5. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.weighted_chosen_matrixPath line 48
  6. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.chosen_column_sum line 55
  7. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.shape_columns_sum line 75
  8. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.empty_chosenColumn line 97
  9. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.weighted_emptyColumn line 130
  10. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.constant_cut_product line 137
  11. def OAI.CriticalHoneycomb.Transfer.RasterGrid.transposeConfigurationEquiv line 160
  12. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.empty_column_shape_sum line 167
  13. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.vacuum_cut_entry line 195
  14. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.empty_row_shape_sum line 203
  15. def OAI.CriticalHoneycomb.Transfer.RasterGrid.hardAssignment line 226
  16. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.hardAssignment_boundary line 228
  17. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.hardAssignment_walls line 235
  18. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.hardAssignment_shape line 243
  19. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.transfer_cut_difference line 251
  20. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.actual_transfer_cut_bound line 267
  21. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.pool_cutrow_weight line 282
  22. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.HardChord.cutrow_weight line 302
  23. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.markTotal_tendsto line 307
  24. def OAI.CriticalHoneycomb.Transfer.RasterGrid.AnyRow.badHardWeight line 322
  25. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.AnyRow.badHardWeight_nonnegative line 326
  26. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.AnyRow.sum_badHardWeight_le line 331
  27. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.AnyRow.hardWeight_le_bad line 354
  28. def OAI.CriticalHoneycomb.Transfer.RasterGrid.AnyRow.rowErrorBound line 365
  29. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.AnyRow.actual_cutrow_bound line 368
  30. def OAI.CriticalHoneycomb.Transfer.RasterGrid.AnyRow.rowLimitError line 419
  31. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.AnyRow.rowErrorBound_limit line 421
  32. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.AnyRow.rowLimitError_limit line 425
  33. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.AnyRow.cauchy_of_cut_approximation line 428