OAI/Combinatorics/HoneycombChords/ColumnPositivity.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Column positivity 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.row_vacuum line 15
  2. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.actual_any_cut_bound line 17
  3. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.vacuum_column_cauchy line 25
  4. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.vacuum_row_cauchy line 34
  5. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.exists_vacuum_column_limit line 49
  6. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.exists_vacuum_row_limit line 53
  7. def OAI.CriticalHoneycomb.Transfer.RasterGrid.archColumn line 57
  8. def OAI.CriticalHoneycomb.Transfer.RasterGrid.archRow line 59
  9. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.archColumn_limit line 61
  10. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.archRow_limit line 64
  11. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.archColumn_vacuum line 67
  12. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.archRow_vacuum line 70
  13. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.physical_rank_one_limit line 74
  14. def OAI.CriticalHoneycomb.Transfer.RasterGrid.archProjection line 100
  15. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.physical_matrix_limit line 102
  16. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.projection_vacuum line 109
  17. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.projection_mul_transfer line 111
  18. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.transfer_mul_projection line 116
  19. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.projection_idempotent line 121
  20. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.arch_pairing line 128
  21. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.projection_mulVec line 131
  22. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.archColumn_eigen line 137
  23. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.archColumn_ne_zero line 143
  24. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.physical_vector_limit line 156
  25. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.physical_iterate_eigen line 162
  26. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.physical_fixed_line line 170
  27. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.projection_eigen_zero line 180
  28. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.physical_other_eigenvalue_small line 190