OAI/Combinatorics/HoneycombChords/TransformSurjectivity.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

Polynomial and proper rational transforms and surjectivity onto finite interpolation data.

The development follows OpenAI, Uniform marked-polygon estimates and sharp finite bridge moments (2026), Sections 6 and 7.

  1. def OAI.CriticalHoneycomb.FiniteFunctional.Analytic.integralJet line 16
  2. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.integralJet_hasDerivAt line 19
  3. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.integralJet_zero_eq line 42
  4. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.integralJet_eq_iteratedDeriv line 46
  5. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.hypJet_odd line 72
  6. def OAI.CriticalHoneycomb.FiniteFunctional.Analytic.polynomialTransformJet line 75
  7. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.polynomialTransformJet_hasDerivAt line 78
  8. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.polynomialTransformJet_add line 86
  9. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.polynomialTransformJet_smul line 91
  10. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.polynomialTransformJet_X_mul line 100
  11. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.polynomialTransformJet_C line 111
  12. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.polynomialTransformJet_two line 115
  13. def OAI.CriticalHoneycomb.FiniteFunctional.Analytic.polynomialKernel line 124
  14. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.polynomialKernel_eq_sum line 127
  15. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.polynomialKernel_integrable line 137
  16. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.polynomialTransform_eq_integral line 143
  17. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.triangular_span line 158
  18. def OAI.CriticalHoneycomb.FiniteFunctional.Analytic.poleCoeff line 197
  19. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.poleCoeff_smooth line 204
  20. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.poleCoeff_eq_zero line 214
  21. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.poleCoeff_diagonal_ne_zero line 227
  22. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.reciprocal_power_hasDerivAt line 239
  23. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.poleJet_expansion line 249
  24. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.poleJet_span line 303
  25. def OAI.CriticalHoneycomb.FiniteFunctional.Analytic.reciprocalCosinePower line 328
  26. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.cosineDouble_hasDerivAt line 331
  27. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.sineDouble_hasDerivAt line 336
  28. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.reciprocalCosinePower_hasDerivAt line 341
  29. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.reciprocalCosinePower_two line 352
  30. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.reciprocalCosine_den_ne_zero line 373
  31. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.integralJet_one line 390
  32. def OAI.CriticalHoneycomb.FiniteFunctional.Analytic.inverseCosinePolynomial line 403
  33. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.inverseCosinePolynomial_degree line 408
  34. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.inverseCosinePolynomial_transform line 419
  35. def OAI.CriticalHoneycomb.FiniteFunctional.Analytic.zMonomial line 453
  36. def OAI.CriticalHoneycomb.FiniteFunctional.Analytic.zCoshJet line 454
  37. def OAI.CriticalHoneycomb.FiniteFunctional.Analytic.zG line 456
  38. def OAI.CriticalHoneycomb.FiniteFunctional.Analytic.zDensity line 457
  39. def OAI.CriticalHoneycomb.FiniteFunctional.Analytic.zKernel line 462
  40. def OAI.CriticalHoneycomb.FiniteFunctional.Analytic.zTransform line 464
  41. def OAI.CriticalHoneycomb.FiniteFunctional.Analytic.TransformDomain line 467
  42. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.zKernel_add line 469
  43. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.zKernel_smul line 474
  44. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.zKernel_zero line 479
  45. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.zKernel_monomial line 481
  46. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.zKernel_coshJet line 487
  47. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.zKernel_g line 492
  48. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.zKernel_monomial_integrable line 499
  49. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.zKernel_coshJet_integrable line 504
  50. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.zKernel_g_integrable line 509
  51. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.zDensity_integrable line 515
  52. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.zTransform_add line 528
  53. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.zTransform_smul line 536
  54. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.zTransform_zero line 542
  55. def OAI.CriticalHoneycomb.FiniteFunctional.Analytic.zTransformLinear line 544
  56. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.zTransform_monomial line 551
  57. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.zTransform_coshJet line 554
  58. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.zTransform_g line 557
  59. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.zPolynomial_mem line 565
  60. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.zTransform_polynomial line 578
  61. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.mixed_inverse_step line 600
  62. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.reciprocalProduct_mem line 608
  63. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.monomial_inverse_step line 629
  64. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.properMonomial_mem line 636
  65. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.properPolynomial_mem line 668
  66. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.cosine_sum_pos line 701
  67. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.zMonomial_mem line 710
  68. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.zCoshJet_mem line 712
  69. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.zG_mem line 714
  70. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.firstPole_mem_range line 717
  71. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.poleJet_mem_range line 731
  72. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.secondPole_mem_range line 747
  73. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.zTransform_surjective line 772