OAI/Combinatorics/HoneycombChords/ChordMass.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Chord mass 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.Pad line 15
  2. instance OAI.CriticalHoneycomb.Transfer.ListBound.padFintype line 18
  3. def OAI.CriticalHoneycomb.Transfer.ListBound.encode line 22
  4. def OAI.CriticalHoneycomb.Transfer.ListBound.decode line 26
  5. lemma OAI.CriticalHoneycomb.Transfer.ListBound.decode_encode line 30
  6. def OAI.CriticalHoneycomb.Transfer.ListBound.weight line 40
  7. lemma OAI.CriticalHoneycomb.Transfer.ListBound.weight_nonnegative line 43
  8. lemma OAI.CriticalHoneycomb.Transfer.ListBound.weight_encode line 51
  9. lemma OAI.CriticalHoneycomb.Transfer.ListBound.sum_weight line 61
  10. lemma OAI.CriticalHoneycomb.Transfer.ListBound.finite_system_bound line 74
  11. def OAI.CriticalHoneycomb.Transfer.RasterGrid.relativePartition line 103
  12. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.relativePartition_eq_prescribed line 105
  13. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.active_shape_decomposition line 111
  14. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.actual_partition_component_bound line 126
  15. def OAI.CriticalHoneycomb.Transfer.RasterGrid.hardWeight line 178
  16. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.hardWeight_nonnegative line 181
  17. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.sum_hardWeight line 186
  18. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.systemNodes_weight line 191
  19. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.system_hardWeight line 198
  20. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.hard_wall_partition_bound line 207
  21. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.eventually_hard_wall_partition_bound line 238
  22. def OAI.CriticalHoneycomb.Transfer.RasterGrid.poolArchHeight line 259
  23. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.poolArchHeight_ge line 261
  24. def OAI.CriticalHoneycomb.Transfer.RasterGrid.archTailWeight line 266
  25. def OAI.CriticalHoneycomb.Transfer.RasterGrid.archTailMass line 268
  26. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.archTailWeight_nonnegative line 269
  27. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.archTailWeight_le line 274
  28. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.archTail_summable line 279
  29. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.archTailMass_limit line 281
  30. def OAI.CriticalHoneycomb.Transfer.RasterGrid.badPoolWeight line 296
  31. def OAI.CriticalHoneycomb.Transfer.RasterGrid.badPoolMass line 301
  32. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.badPoolWeight_nonnegative line 302
  33. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.badPoolWeight_le line 308
  34. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.badPool_summable line 314
  35. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.badPoolMass_eq line 316
  36. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.nat_half_tendsto line 329
  37. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.badPoolMass_limit line 334
  38. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.pool_midrow_weight line 338
  39. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.HardChord.midrow_weight line 359