OAI/Analysis/PlanarPacking/CanonicalRows.lean

GitHub source file

109 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpPlanar.IntegerIntervals.CBox.SqNormCheck line 11
  2. instance OAI.SharpPlanar.IntegerIntervals.(instance at line 13) line 13
  3. lemma OAI.SharpPlanar.IntegerIntervals.CBox.norm_le_rat line 16
  4. def OAI.SharpPlanar.lambdaCap line 49
  5. def OAI.SharpPlanar.zCap line 50
  6. def OAI.SharpPlanar.dampingCap line 51
  7. def OAI.SharpPlanar.slopeCap line 52
  8. lemma OAI.SharpPlanar.kernel_den_sq line 54
  9. lemma OAI.SharpPlanar.z_re line 57
  10. lemma OAI.SharpPlanar.lambda_sq line 59
  11. lemma OAI.SharpPlanar.z_sq line 63
  12. lemma OAI.SharpPlanar.lambda_sq_antitone line 70
  13. lemma OAI.SharpPlanar.z_sq_antitone line 75
  14. lemma OAI.SharpPlanar.endpoint_kernel_bounds line 82
  15. lemma OAI.SharpPlanar.piece_secant_bound line 93
  16. lemma OAI.SharpPlanar.piece_damping_bound line 100
  17. lemma OAI.SharpPlanar.piece_kernel_bounds line 122
  18. def OAI.SharpPlanar.IntegerBasis.uAmplitude line 139
  19. def OAI.SharpPlanar.IntegerBasis.vAmplitude line 141
  20. def OAI.SharpPlanar.IntegerBasis.uAmplitudeBox line 144
  21. def OAI.SharpPlanar.IntegerBasis.vAmplitudeBox line 147
  22. lemma OAI.SharpPlanar.IntegerBasis.uAmplitudeBox_contains line 149
  23. lemma OAI.SharpPlanar.IntegerBasis.vAmplitudeBox_contains line 161
  24. def OAI.SharpPlanar.IntegerBasis.densityNum line 171

    Source comment

    Zero-based piece indexing: this is exactly the source M_1,...,M_6.
    def densityNum : Fin 6 → ℤ := ![56,48,35,25,19,1571]
  25. def OAI.SharpPlanar.IntegerBasis.densityDen line 172
  26. def OAI.SharpPlanar.IntegerBasis.densityCap line 173
  27. lemma OAI.SharpPlanar.IntegerBasis.densityDen_pos line 174
  28. def OAI.SharpPlanar.IntegerBasis.DensityCheck line 176
  29. instance OAI.SharpPlanar.IntegerBasis.(instance at line 180) line 180
  30. lemma OAI.SharpPlanar.IntegerBasis.density_finite_check line 182
  31. lemma OAI.SharpPlanar.IntegerBasis.density_check line 186
  32. lemma OAI.SharpPlanar.IntegerBasis.amplitude_endpoints line 190
  33. lemma OAI.SharpPlanar.IntegerBasis.uAmplitude_bound line 203
  34. lemma OAI.SharpPlanar.IntegerBasis.unit_phase_norm line 225
  35. lemma OAI.SharpPlanar.IntegerBasis.u_norm_amplitude line 228
  36. lemma OAI.SharpPlanar.IntegerBasis.v_norm_amplitude line 234
  37. lemma OAI.SharpPlanar.IntegerBasis.basis_density_bounds line 242
  38. lemma OAI.SharpPlanar.densityCap_nonneg line 253
  39. lemma OAI.SharpPlanar.piece_summand_bound line 255
  40. lemma OAI.SharpPlanar.piece_density_bound line 266
  41. lemma OAI.SharpPlanar.lambdaCap_nonneg line 294
  42. lemma OAI.SharpPlanar.zCap_nonneg line 295
  43. lemma OAI.SharpPlanar.dampingCap_pos line 296
  44. lemma OAI.SharpPlanar.slopeCap_nonneg line 297
  45. def OAI.SharpPlanar.pieceMass line 299
  46. def OAI.SharpPlanar.pieceL line 301
  47. def OAI.SharpPlanar.atomMass line 303
  48. def OAI.SharpPlanar.atomL line 304
  49. def OAI.SharpPlanar.segmentEnvelope line 306
  50. lemma OAI.SharpPlanar.segmentEnvelope_nonneg line 311
  51. lemma OAI.SharpPlanar.kernelMoment_segment_bound line 316
  52. lemma OAI.SharpPlanar.exp_segment_bound line 342
  53. lemma OAI.SharpPlanar.pieceMass_nonneg line 365
  54. lemma OAI.SharpPlanar.segment_exp_integral_bound line 371
  55. lemma OAI.SharpPlanar.segmentEnvelope_integral_bound line 384
  56. lemma OAI.SharpPlanar.sharp_integral_piece_bound line 395
  57. lemma OAI.SharpPlanar.kernelMoment_endpoint_bound line 420
  58. def OAI.SharpPlanar.atomicCoefficient line 442
  59. lemma OAI.SharpPlanar.atomicCoefficient_norm line 443
  60. lemma OAI.SharpPlanar.sharp_atomic_bound line 446
  61. theorem OAI.SharpPlanar.sharp_moment_bound line 467
  62. lemma OAI.SharpPlanar.pieceMass_antitone line 491
  63. lemma OAI.SharpPlanar.pieceL_nonneg line 512
  64. lemma OAI.SharpPlanar.atomL_nonneg line 514
  65. lemma OAI.SharpPlanar.pieceL_shift_bound line 520
  66. lemma OAI.SharpPlanar.atomL_shift line 531
  67. lemma OAI.SharpPlanar.pieceL_period_bound line 537
  68. lemma OAI.SharpPlanar.periodic_geometric_sum line 551
  69. def OAI.SharpPlanar.rowFactor line 578
  70. def OAI.SharpPlanar.rowPiece line 580
  71. def OAI.SharpPlanar.rowTable line 582
  72. lemma OAI.SharpPlanar.rowFactor_nonneg line 586
  73. lemma OAI.SharpPlanar.rowFactor_periodic line 589
  74. lemma OAI.SharpPlanar.rowPiece_nonneg line 593
  75. lemma OAI.SharpPlanar.rowPiece_period_bound line 598
  76. lemma OAI.SharpPlanar.rowPiece_tail_sum line 612
  77. lemma OAI.SharpPlanar.paired_jet_bound line 631
  78. lemma OAI.SharpPlanar.sharp_S_row line 639
  79. def OAI.SharpPlanar.rowTailNorm line 662
  80. lemma OAI.SharpPlanar.rowTailNorm_summable line 665
  81. lemma OAI.SharpPlanar.natural_row_tail_summable line 669
  82. lemma OAI.SharpPlanar.natural_row_tail_bound line 673
  83. theorem OAI.SharpPlanar.sharp_S_tail line 679
  84. def OAI.SharpPlanar.rowQLower line 712
  85. def OAI.SharpPlanar.rowDUpper line 715
  86. lemma OAI.SharpPlanar.pi_fine line 719
  87. lemma OAI.SharpPlanar.b_fine line 721
  88. lemma OAI.SharpPlanar.rowQLower_bound line 724
  89. lemma OAI.SharpPlanar.rowDUpper_bound line 737
  90. def OAI.SharpPlanar.pieceBase line 754
  91. lemma OAI.SharpPlanar.pieceBase_pos line 755
  92. lemma OAI.SharpPlanar.pieceBase_lt_one line 756
  93. lemma OAI.SharpPlanar.pieceBase_contains line 757
  94. lemma OAI.SharpPlanar.decay_pieceBase line 769
  95. def OAI.SharpPlanar.massRational line 777
  96. lemma OAI.SharpPlanar.massRational_nonneg line 779
  97. lemma OAI.SharpPlanar.pieceMass_le line 783
  98. def OAI.SharpPlanar.factorRational line 793
  99. def OAI.SharpPlanar.pieceRational line 795
  100. def OAI.SharpPlanar.tableRational line 798
  101. lemma OAI.SharpPlanar.factorRational_nonneg line 800
  102. lemma OAI.SharpPlanar.rowFactor_le line 806
  103. lemma OAI.SharpPlanar.rowPiece_le line 818
  104. lemma OAI.SharpPlanar.rowTable_le line 831
  105. lemma OAI.SharpPlanar.tableRational_zero line 845
  106. lemma OAI.SharpPlanar.tableRational_four line 849
  107. lemma OAI.SharpPlanar.tableRational_sixteen line 853
  108. lemma OAI.SharpPlanar.tableRational_hundred line 857
  109. theorem OAI.SharpPlanar.rowTable_bounds line 862