OAI/Analysis/PlanarPacking/Cardinal.lean

GitHub source file

133 declarations, 0 contain sorry, 0 declared as axioms

Gaussian cardinal functions for planar packing

The cardinal family and Fourier kernel follow the construction in A sharp Fourier certificate for planar circle packing (OpenAI, 2026).

  1. abbrev OAI.SharpPlanar.Plane line 24

    Also declared: ComparatorChallenges/PlanarPacking.lean:16 (same declaration text).

  2. def OAI.SharpPlanar.b line 26
  3. def OAI.SharpPlanar.h line 27
  4. def OAI.SharpPlanar.B line 28
  5. def OAI.SharpPlanar.residues line 30
  6. abbrev OAI.SharpPlanar.Node line 33
  7. abbrev OAI.SharpPlanar.X line 36
  8. def OAI.SharpPlanar.P line 38
  9. def OAI.SharpPlanar.Pcoeff line 41
  10. def OAI.SharpPlanar.Q line 51
  11. def OAI.SharpPlanar.D line 55
  12. def OAI.SharpPlanar.lambda line 60
  13. def OAI.SharpPlanar.z line 62
  14. def OAI.SharpPlanar.u line 66
  15. def OAI.SharpPlanar.v line 71
  16. structure OAI.SharpPlanar.CardinalData line 76
  17. def OAI.SharpPlanar.density line 82
  18. def OAI.SharpPlanar.kernelMoment line 88
  19. def OAI.SharpPlanar.K line 93
  20. def OAI.SharpPlanar.positiveData line 100
  21. def OAI.SharpPlanar.Scoords line 103
  22. def OAI.SharpPlanar.fixed₁ line 109
  23. def OAI.SharpPlanar.fixed₂ line 110
  24. theorem OAI.SharpPlanar.b_pos line 112
  25. theorem OAI.SharpPlanar.b_sq line 114
  26. theorem OAI.SharpPlanar.B_eq_inv_b_sq line 119
  27. theorem OAI.SharpPlanar.z_im line 121
  28. theorem OAI.SharpPlanar.strict_damping line 125
  29. theorem OAI.SharpPlanar.X_summable line 141
  30. theorem OAI.SharpPlanar.X_summable_coord line 144
  31. theorem OAI.SharpPlanar.X_norm line 148
  32. theorem OAI.SharpPlanar.X_summable_pairs line 154
  33. theorem OAI.SharpPlanar.h_pos line 159
  34. theorem OAI.SharpPlanar.B_pos line 160
  35. theorem OAI.SharpPlanar.imaginary_gaussian_denominator line 162
  36. theorem OAI.SharpPlanar.lambda_bound line 167
  37. theorem OAI.SharpPlanar.z_bound line 173
  38. def OAI.SharpPlanar.kappa line 184
  39. theorem OAI.SharpPlanar.kappa_pos line 186
  40. theorem OAI.SharpPlanar.kernelMoment_bound line 189
  41. def OAI.SharpPlanar.coeffMass line 213
  42. theorem OAI.SharpPlanar.Pcoeff_norm line 223
  43. lemma OAI.SharpPlanar.positive_coeff_mass line 242
  44. lemma OAI.SharpPlanar.positive_coeff_mass_le line 246
  45. lemma OAI.SharpPlanar.phase_norm line 254
  46. lemma OAI.SharpPlanar.atom_phase_norm line 258
  47. lemma OAI.SharpPlanar.frequency_distance_le line 262
  48. lemma OAI.SharpPlanar.u_bound line 271
  49. lemma OAI.SharpPlanar.v_bound line 292
  50. def OAI.SharpPlanar.densityBound line 307
  51. lemma OAI.SharpPlanar.densityBound_nonneg line 309
  52. lemma OAI.SharpPlanar.v_bound' line 311
  53. lemma OAI.SharpPlanar.summand_bound line 317
  54. lemma OAI.SharpPlanar.density_summable line 329
  55. lemma OAI.SharpPlanar.density_bound line 335
  56. def OAI.SharpPlanar.kernelEnvelope line 364
  57. lemma OAI.SharpPlanar.kernelEnvelope_nonneg line 367
  58. lemma OAI.SharpPlanar.kernelMoment_bound' line 374
  59. lemma OAI.SharpPlanar.atomic_bound line 380
  60. lemma OAI.SharpPlanar.piece_interval line 406
  61. lemma OAI.SharpPlanar.integral_piece_bound line 413
  62. lemma OAI.SharpPlanar.K_bound line 431
  63. lemma OAI.SharpPlanar.continuous_u line 456
  64. lemma OAI.SharpPlanar.continuous_v line 460
  65. lemma OAI.SharpPlanar.continuousOn_density line 464
  66. lemma OAI.SharpPlanar.denominator_ne line 478
  67. lemma OAI.SharpPlanar.continuous_lambda line 485
  68. lemma OAI.SharpPlanar.continuous_z line 489
  69. lemma OAI.SharpPlanar.continuous_kernelMoment line 493
  70. lemma OAI.SharpPlanar.piece_integrable line 498
  71. lemma OAI.SharpPlanar.density_positive_add line 504
  72. lemma OAI.SharpPlanar.density_positive_smul line 517
  73. lemma OAI.SharpPlanar.K_positive_add line 523
  74. lemma OAI.SharpPlanar.K_positive_smul line 545
  75. lemma OAI.SharpPlanar.residue_lt line 556
  76. lemma OAI.SharpPlanar.Q_pos line 560
  77. lemma OAI.SharpPlanar.Q_mod line 586
  78. lemma OAI.SharpPlanar.D_mod line 587
  79. def OAI.SharpPlanar.nodeWeight line 589
  80. def OAI.SharpPlanar.allNodeWeight line 590
  81. lemma OAI.SharpPlanar.nodeWeight_pos line 592
  82. lemma OAI.SharpPlanar.allNodeWeight_nonneg line 596
  83. lemma OAI.SharpPlanar.nodeWeight_le line 599
  84. lemma OAI.SharpPlanar.K_positive_bound line 604
  85. lemma OAI.SharpPlanar.Scoords_bound line 608
  86. lemma OAI.SharpPlanar.exp_nat_summable line 647
  87. lemma OAI.SharpPlanar.kernelEnvelope_summable line 652
  88. lemma OAI.SharpPlanar.pairEnvelope_summable line 656
  89. lemma OAI.SharpPlanar.Scoords_summable line 666
  90. lemma OAI.SharpPlanar.Scoords_mem line 670
  91. lemma OAI.SharpPlanar.Scoords_add line 674
  92. lemma OAI.SharpPlanar.Scoords_smul line 679
  93. def OAI.SharpPlanar.Slinear line 684
  94. def OAI.SharpPlanar.Sbound line 689
  95. lemma OAI.SharpPlanar.Sbound_nonneg line 692
  96. lemma OAI.SharpPlanar.Slinear_bound line 697
  97. def OAI.SharpPlanar.S line 709
  98. lemma OAI.SharpPlanar.S_apply line 711
  99. def OAI.SharpPlanar.complexLambda line 718
  100. def OAI.SharpPlanar.complexZ line 720
  101. lemma OAI.SharpPlanar.complexLambda_real line 723
  102. lemma OAI.SharpPlanar.complexZ_real line 724
  103. lemma OAI.SharpPlanar.reciprocal_disk_identity line 727
  104. lemma OAI.SharpPlanar.reciprocal_disk_bound line 740
  105. def OAI.SharpPlanar.diskCenter line 771
  106. lemma OAI.SharpPlanar.disk_coordinate_bounds line 773
  107. lemma OAI.SharpPlanar.disk_denominator_lower line 788
  108. lemma OAI.SharpPlanar.disk_denominator_ne line 797
  109. lemma OAI.SharpPlanar.b_lower_simple line 804
  110. lemma OAI.SharpPlanar.disk_lambda_bound line 809
  111. lemma OAI.SharpPlanar.disk_z_bound line 818
  112. lemma OAI.SharpPlanar.disk_delta_bounds line 832
  113. lemma OAI.SharpPlanar.disk_z_imaginary line 843
  114. lemma OAI.SharpPlanar.disk_z_imaginary_simple line 877
  115. def OAI.SharpPlanar.complexU line 889
  116. def OAI.SharpPlanar.complexV line 893
  117. lemma OAI.SharpPlanar.complexU_real line 898
  118. lemma OAI.SharpPlanar.complexV_real line 899
  119. lemma OAI.SharpPlanar.disk_frequency_distance line 901
  120. lemma OAI.SharpPlanar.disk_phase_bound line 917
  121. lemma OAI.SharpPlanar.complexU_disk_bound line 931
  122. lemma OAI.SharpPlanar.complexV_disk_bound line 961
  123. def OAI.SharpPlanar.finiteDensity line 982
  124. lemma OAI.SharpPlanar.finiteDensity_disk_bound line 985
  125. def OAI.SharpPlanar.complexDirectFactor line 1013
  126. def OAI.SharpPlanar.complexTransformedFactor line 1015
  127. lemma OAI.SharpPlanar.divided_power_norm line 1019
  128. lemma OAI.SharpPlanar.phase_exp_norm_bound line 1024
  129. lemma OAI.SharpPlanar.complexDirectFactor_disk_bound line 1033
  130. lemma OAI.SharpPlanar.complexTransformedFactor_disk_bound line 1056
  131. lemma OAI.SharpPlanar.numerical_moment_bound line 1080
  132. lemma OAI.SharpPlanar.directIntegrand_disk_bound line 1091
  133. lemma OAI.SharpPlanar.transformedIntegrand_disk_bound line 1109