OAI/Combinatorics/HoneycombChords/BoundaryExpansion.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

Boundary expansion 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.RasterGrid.markedLeft line 14
  2. def OAI.CriticalHoneycomb.Transfer.RasterGrid.markedRight line 16
  3. def OAI.CriticalHoneycomb.Transfer.RasterGrid.markedMixed line 18
  4. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.marked_base line 20
  5. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.markedLeft_eq line 24
  6. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.markedRight_eq line 29
  7. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.markedLeft_shift line 34
  8. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.markedRight_shift line 40
  9. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.projection_shift_zero line 46
  10. def OAI.CriticalHoneycomb.Transfer.RasterGrid.archDual line 65
  11. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.archDual_add line 67
  12. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.archDual_sub line 70
  13. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.archDual_smul line 73
  14. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.archDual_A line 79
  15. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.archDual_left_A line 80
  16. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.archDual_right_A line 83
  17. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.archDual_gap line 86
  18. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.archDual_double line 91
  19. def OAI.CriticalHoneycomb.Transfer.RasterGrid.reducedSolve line 96
  20. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.gap_reducedSolve line 98
  21. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.archDual_reducedSolve line 101
  22. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.reducedSolve_equation line 104
  23. def OAI.CriticalHoneycomb.Transfer.RasterGrid.eigenLeft line 114
  24. def OAI.CriticalHoneycomb.Transfer.RasterGrid.eigenRight line 116
  25. def OAI.CriticalHoneycomb.Transfer.RasterGrid.eigenSource line 118
  26. def OAI.CriticalHoneycomb.Transfer.RasterGrid.eigenCoefficient line 121
  27. def OAI.CriticalHoneycomb.Transfer.RasterGrid.eigenMixed line 122
  28. def OAI.CriticalHoneycomb.Transfer.RasterGrid.markedEigenvector line 124
  29. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.eigenLeft_equation line 126
  30. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.eigenRight_equation line 130
  31. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.eigenMixed_equation line 134
  32. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.double_archColumn line 144
  33. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.source_marked_eigenvector line 148
  34. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.gap_archColumn line 175
  35. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.inv_gap_archColumn line 178
  36. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.archRow_double line 181
  37. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.vecMul_projection line 185
  38. def OAI.CriticalHoneycomb.Transfer.RasterGrid.dualSolve line 192
  39. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.dualSolve_gap line 194
  40. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.dualSolve_pair line 197
  41. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.dualSolve_A line 200
  42. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.dualSolve_equation line 203
  43. def OAI.CriticalHoneycomb.Transfer.RasterGrid.dualLeft line 211
  44. def OAI.CriticalHoneycomb.Transfer.RasterGrid.dualRight line 213
  45. def OAI.CriticalHoneycomb.Transfer.RasterGrid.dualSource line 215
  46. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.dualSource_pair line 218
  47. def OAI.CriticalHoneycomb.Transfer.RasterGrid.dualMixed line 224
  48. def OAI.CriticalHoneycomb.Transfer.RasterGrid.dualEigenvector line 226
  49. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.dualLeft_equation line 228
  50. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.dualRight_equation line 234
  51. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.dualMixed_equation line 240
  52. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.source_dual_eigenvector line 253
  53. lemma OAI.CriticalHoneycomb.BoundaryJet.powers_of_power_small line 280
  54. lemma OAI.CriticalHoneycomb.BoundaryJet.continuous_base line 295
  55. lemma OAI.CriticalHoneycomb.BoundaryJet.continuous_left line 297
  56. lemma OAI.CriticalHoneycomb.BoundaryJet.continuous_right line 299
  57. lemma OAI.CriticalHoneycomb.BoundaryJet.continuous_both line 301
  58. lemma OAI.CriticalHoneycomb.BoundaryJet.continuous_C line 303
  59. def OAI.CriticalHoneycomb.BoundaryJet.scaleHom line 305
  60. lemma OAI.CriticalHoneycomb.BoundaryJet.base_scale line 311
  61. lemma OAI.CriticalHoneycomb.BoundaryJet.left_scale line 312
  62. lemma OAI.CriticalHoneycomb.BoundaryJet.right_scale line 313
  63. lemma OAI.CriticalHoneycomb.BoundaryJet.both_scale line 314
  64. lemma OAI.CriticalHoneycomb.BoundaryJet.scale_zero line 315
  65. lemma OAI.CriticalHoneycomb.BoundaryJet.scale_inverse line 316
  66. lemma OAI.CriticalHoneycomb.BoundaryJet.continuous_scale line 318
  67. lemma OAI.CriticalHoneycomb.BoundaryJet.continuous_scale_parameter line 324
  68. def OAI.CriticalHoneycomb.BoundaryJet.scaleMatrix line 330
  69. lemma OAI.CriticalHoneycomb.BoundaryJet.scaleMatrix_pow line 332
  70. lemma OAI.CriticalHoneycomb.BoundaryJet.scaleMatrix_inverse line 335
  71. lemma OAI.CriticalHoneycomb.BoundaryJet.continuous_scaleMatrix line 339
  72. lemma OAI.CriticalHoneycomb.BoundaryJet.continuous_scaleMatrix_parameter line 345
  73. theorem OAI.CriticalHoneycomb.BoundaryJet.stable_jet_powers line 353