OAI/Combinatorics/HoneycombChords/StripProjection.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Strip projection 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.inverseAtOne line 27
  2. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.inverseAtOne_mul line 29
  3. def OAI.CriticalHoneycomb.Transfer.RasterGrid.eigenPair line 32
  4. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.eigenPair_base line 33
  5. def OAI.CriticalHoneycomb.Transfer.RasterGrid.normalizedDual line 36
  6. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.normalized_pair line 38
  7. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.normalized_dual_eigen line 41
  8. def OAI.CriticalHoneycomb.Transfer.RasterGrid.markedProjection line 50
  9. def OAI.CriticalHoneycomb.Transfer.RasterGrid.markedEigenvalue line 52
  10. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.markedProjection_base line 53
  11. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.markedProjection_idempotent line 57
  12. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.markedProjection_mul line 68
  13. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.mul_markedProjection line 76
  14. def OAI.CriticalHoneycomb.Transfer.RasterGrid.markedRemainder line 84
  15. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.marked_remainder_orthogonal line 86
  16. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.double_pow_projection line 91
  17. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.double_remainder_power line 96
  18. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.double_remainder_limit line 105
  19. def OAI.CriticalHoneycomb.Transfer.RasterGrid.jetBaseHom line 110
  20. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.markedRemainder_base line 116
  21. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.marked_remainder_limit line 126
  22. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.orthogonal_pow_add line 136
  23. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.markedProjection_pow line 145
  24. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.marked_power_split line 149
  25. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.markedEigenvalue_pow line 159
  26. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.jetBaseHom_apply line 182
  27. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.jet_kernel_lift line 183
  28. def OAI.CriticalHoneycomb.Transfer.RasterGrid.markedGap line 214
  29. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.markedGap_base line 216
  30. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.markedGap_kernel line 229
  31. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.marked_fixed_projected line 235
  32. def OAI.CriticalHoneycomb.Transfer.RasterGrid.commonScalar line 250
  33. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.markedProjection_mulVec line 253
  34. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.commuting_common_line line 262