OAI/Combinatorics/HoneycombChords/ArchContinuation.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

Arch continuation 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.FiniteContinuation.halfRect line 14
  2. def OAI.CriticalHoneycomb.FiniteContinuation.BottomArch line 15
  3. def OAI.CriticalHoneycomb.FiniteContinuation.archRun line 19
  4. lemma OAI.CriticalHoneycomb.FiniteContinuation.archRun_head line 20
  5. lemma OAI.CriticalHoneycomb.FiniteContinuation.archRun_last line 22
  6. lemma OAI.CriticalHoneycomb.FiniteContinuation.archRun_mem line 24
  7. lemma OAI.CriticalHoneycomb.FiniteContinuation.eastRun_min line 31
  8. def OAI.CriticalHoneycomb.FiniteContinuation.archExtend line 39
  9. lemma OAI.CriticalHoneycomb.FiniteContinuation.archExtend_head line 41
  10. lemma OAI.CriticalHoneycomb.FiniteContinuation.archExtend_last line 44
  11. lemma OAI.CriticalHoneycomb.FiniteContinuation.archExtend_length line 47
  12. lemma OAI.CriticalHoneycomb.FiniteContinuation.archExtend_chain line 54
  13. lemma OAI.CriticalHoneycomb.FiniteContinuation.archExtend_nodup line 71
  14. def OAI.CriticalHoneycomb.FiniteContinuation.aboveZero line 105
  15. lemma OAI.CriticalHoneycomb.FiniteContinuation.archExtend_filter line 106
  16. lemma OAI.CriticalHoneycomb.FiniteContinuation.archExtend_injective line 127
  17. lemma OAI.CriticalHoneycomb.FiniteContinuation.finite_arch_bound line 135
  18. lemma OAI.CriticalHoneycomb.FiniteContinuation.archExtend_mem line 148
  19. def OAI.CriticalHoneycomb.FiniteContinuation.archChord line 172
  20. lemma OAI.CriticalHoneycomb.FiniteContinuation.archChord_injective line 186
  21. lemma OAI.CriticalHoneycomb.FiniteContinuation.arch_extended_weight line 194
  22. theorem OAI.CriticalHoneycomb.FiniteContinuation.arch_partial_sum_le line 201
  23. theorem OAI.CriticalHoneycomb.FiniteContinuation.bottom_arch_summable_of_lt line 235
  24. def OAI.CriticalHoneycomb.FiniteContinuation.reverseArch line 244
  25. def OAI.CriticalHoneycomb.FiniteContinuation.reverseArchEquiv line 250
  26. theorem OAI.CriticalHoneycomb.FiniteContinuation.bottom_arch_summable line 256
  27. structure OAI.CriticalHoneycomb.FiniteContinuation.ArchEnds line 269
  28. def OAI.CriticalHoneycomb.FiniteContinuation.ArchFamily line 274
  29. def OAI.CriticalHoneycomb.FiniteContinuation.archNodes line 278
  30. def OAI.CriticalHoneycomb.FiniteContinuation.archFamilyWeight line 282
  31. lemma OAI.CriticalHoneycomb.FiniteContinuation.archFamilyWeight_nonnegative line 285
  32. lemma OAI.CriticalHoneycomb.FiniteContinuation.arch_family_summable line 288
  33. def OAI.CriticalHoneycomb.FiniteContinuation.ArchSystem line 304
  34. def OAI.CriticalHoneycomb.FiniteContinuation.archSystemWeight line 307
  35. lemma OAI.CriticalHoneycomb.FiniteContinuation.arch_system_summable line 310
  36. lemma OAI.CriticalHoneycomb.FiniteContinuation.archNodes_mem line 313
  37. def OAI.CriticalHoneycomb.FiniteContinuation.archHeight line 323
  38. lemma OAI.CriticalHoneycomb.FiniteContinuation.archNodes_height line 326
  39. def OAI.CriticalHoneycomb.FiniteContinuation.topTurn line 332
  40. lemma OAI.CriticalHoneycomb.FiniteContinuation.topTurn_injective line 333
  41. lemma OAI.CriticalHoneycomb.FiniteContinuation.topTurn_adj line 342
  42. def OAI.CriticalHoneycomb.FiniteContinuation.archSystemNodes line 347
  43. def OAI.CriticalHoneycomb.FiniteContinuation.ArchSystemsFit line 351
  44. lemma OAI.CriticalHoneycomb.FiniteContinuation.archSystemsFit_of_height line 356
  45. lemma OAI.CriticalHoneycomb.FiniteContinuation.eventually_archSystemsFit line 380
  46. def OAI.CriticalHoneycomb.FiniteContinuation.halfStripSystemMass line 386
  47. def OAI.CriticalHoneycomb.FiniteContinuation.finitePureArchMass line 389
  48. theorem OAI.CriticalHoneycomb.FiniteContinuation.pure_arch_limit line 394