OAI/Combinatorics/HoneycombChords/TransferProjection.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

Transfer 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.columnDelta line 16
  2. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.columnDelta_vector line 18
  3. def OAI.CriticalHoneycomb.Transfer.RasterGrid.physicalDoubleMatrix line 33
  4. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.physicalDoubleMatrix_eq line 36
  5. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.physical_double_rank_one line 48
  6. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.projection_mul_double line 65
  7. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.double_mul_projection line 68
  8. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.double_vector_limit line 71
  9. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.double_fixed_projected line 79
  10. def OAI.CriticalHoneycomb.Transfer.RasterGrid.gapMatrix line 89
  11. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.projection_mul_gap line 91
  12. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.gap_kernel line 93
  13. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.physical_gap_det_ne_zero line 102
  14. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.planarRow_smul line 117
  15. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.planarRow_add line 122
  16. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.fixedSeed line 127
  17. def OAI.CriticalHoneycomb.Transfer.PlanarNormalization.fixedColumn line 130
  18. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.fixedColumn_eq_kernel line 132
  19. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.fixedColumn_none line 147
  20. lemma OAI.CriticalHoneycomb.Transfer.PlanarNormalization.fixed_double_columns line 157
  21. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.fixed_column_mulVec line 182
  22. def OAI.CriticalHoneycomb.Transfer.RasterGrid.markedColumn line 207
  23. def OAI.CriticalHoneycomb.Transfer.RasterGrid.boundaryProduct line 210
  24. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.boundaryProduct_zero line 212
  25. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.boundaryProduct_cons line 213
  26. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.vacuum_cons line 217
  27. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.singleColumn_zero line 220
  28. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.singleColumn_succ line 223
  29. def OAI.CriticalHoneycomb.Transfer.RasterGrid.portSumLeft line 228
  30. def OAI.CriticalHoneycomb.Transfer.RasterGrid.portSumRight line 230
  31. def OAI.CriticalHoneycomb.Transfer.RasterGrid.portSumBoth line 232
  32. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.boundaryProduct_vacuum line 234
  33. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.portSumLeft_succ line 236
  34. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.portSumRight_succ line 240
  35. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.portSumBoth_succ line 244
  36. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.marked_power_coords line 251
  37. theorem OAI.CriticalHoneycomb.Transfer.RasterGrid.marked_power_mixed line 290
  38. def OAI.CriticalHoneycomb.Transfer.RasterGrid.fixedDoubleMatrix line 304
  39. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.fixedDoubleMatrix_eq line 309
  40. def OAI.CriticalHoneycomb.Transfer.RasterGrid.physicalMarkedK line 324
  41. def OAI.CriticalHoneycomb.Transfer.RasterGrid.markedDoubleMatrix line 330
  42. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.markedDoubleMatrix_eq line 334
  43. def OAI.CriticalHoneycomb.Transfer.RasterGrid.spinCharge line 365
  44. def OAI.CriticalHoneycomb.Transfer.RasterGrid.columnCharge line 366
  45. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.sourceR_charge line 367
  46. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.columnKernel_charge line 372
  47. def OAI.CriticalHoneycomb.Transfer.RasterGrid.HasShift line 395
  48. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.kernel_hasShift line 397
  49. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.shift_mul line 402
  50. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.shift_add line 410
  51. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.transfer_power_shift line 418
  52. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.charge_vacuum line 431
  53. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.archColumn_charge line 433
  54. lemma OAI.CriticalHoneycomb.Transfer.RasterGrid.archRow_charge line 443