OAI/Combinatorics/HoneycombChords/PlanarRows.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Planar rows 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.PlanarNormalization.act_congr_of_length line 13
  2. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.planarRow_congr_of_length line 37
  3. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.act_suffix line 46
  4. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.planarRow_suffix line 62
  5. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.planarRow_zero line 73
  6. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.seedAux line 88
  7. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.seedAux_zero line 91
  8. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.hardDoubleRow line 99
  9. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.hardDoubleRow_eq_columns line 102