OAI/Combinatorics/HoneycombChords/FunctionalTransforms.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

Integral transforms and endpoint constraints for the finite strip functional.

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

  1. def OAI.CriticalHoneycomb.FiniteFunctional.RepresentsDensity line 18
  2. lemma OAI.CriticalHoneycomb.FiniteFunctional.lift_zDensity line 20
  3. lemma OAI.CriticalHoneycomb.FiniteFunctional.angle_identity line 52
  4. lemma OAI.CriticalHoneycomb.FiniteFunctional.angle_abs line 53
  5. lemma OAI.CriticalHoneycomb.FiniteFunctional.angle_lt_pi_half line 54
  6. lemma OAI.CriticalHoneycomb.FiniteFunctional.density_transform_surjective line 56
  7. lemma OAI.CriticalHoneycomb.FiniteFunctional.pairing_eq_zIntegral line 67
  8. lemma OAI.CriticalHoneycomb.FiniteFunctional.value_C_eq_fusion line 77
  9. lemma OAI.CriticalHoneycomb.FiniteFunctional.C_parameter_zero line 88
  10. lemma OAI.CriticalHoneycomb.FiniteFunctional.D_zero line 89
  11. lemma OAI.CriticalHoneycomb.FiniteFunctional.D_neg_four line 90
  12. lemma OAI.CriticalHoneycomb.FiniteFunctional.aStar_ne_zero line 91
  13. lemma OAI.CriticalHoneycomb.FiniteFunctional.value_div_D_eq_interpolant line 99
  14. lemma OAI.CriticalHoneycomb.FiniteFunctional.value_inv_D_eq_interpolant line 118
  15. lemma OAI.CriticalHoneycomb.FiniteFunctional.iteratedDeriv_complex_ofReal line 137
  16. lemma OAI.CriticalHoneycomb.FiniteFunctional.C_even_jet_zero line 147
  17. lemma OAI.CriticalHoneycomb.FiniteFunctional.C_jet_hasDerivAt line 167
  18. def OAI.CriticalHoneycomb.FiniteFunctional.pairingKernel line 185
  19. def OAI.CriticalHoneycomb.FiniteFunctional.PairingIntegrable line 187
  20. lemma OAI.CriticalHoneycomb.FiniteFunctional.pairingKernel_jet_ae line 190
  21. lemma OAI.CriticalHoneycomb.FiniteFunctional.pairingJet_integrable line 200
  22. def OAI.CriticalHoneycomb.FiniteFunctional.functionalJet line 208
  23. lemma OAI.CriticalHoneycomb.FiniteFunctional.functionalJet_zero line 213
  24. lemma OAI.CriticalHoneycomb.FiniteFunctional.functionalJet_hasDerivAt line 218
  25. lemma OAI.CriticalHoneycomb.FiniteFunctional.iteratedDeriv_integralFusion line 227
  26. lemma OAI.CriticalHoneycomb.FiniteFunctional.value_jet_eq line 240
  27. lemma OAI.CriticalHoneycomb.FiniteFunctional.pairingKernel_add line 246
  28. lemma OAI.CriticalHoneycomb.FiniteFunctional.pairingKernel_smul line 251
  29. lemma OAI.CriticalHoneycomb.FiniteFunctional.pairingKernel_zero line 256
  30. lemma OAI.CriticalHoneycomb.FiniteFunctional.PairingIntegrable.add line 259
  31. lemma OAI.CriticalHoneycomb.FiniteFunctional.PairingIntegrable.smul line 264
  32. lemma OAI.CriticalHoneycomb.FiniteFunctional.PairingIntegrable.zero line 269
  33. lemma OAI.CriticalHoneycomb.FiniteFunctional.value_add line 274
  34. lemma OAI.CriticalHoneycomb.FiniteFunctional.value_smul line 283
  35. lemma OAI.CriticalHoneycomb.FiniteFunctional.value_zero line 290
  36. lemma OAI.CriticalHoneycomb.FiniteFunctional.M_integrable_and_annihilated line 293
  37. lemma OAI.CriticalHoneycomb.FiniteFunctional.integralInterpolant_even line 336
  38. lemma OAI.CriticalHoneycomb.FiniteFunctional.pairingKernel_div_D_ae line 344
  39. lemma OAI.CriticalHoneycomb.FiniteFunctional.pairing_div_D_integrable line 354
  40. lemma OAI.CriticalHoneycomb.FiniteFunctional.value_sub line 362
  41. lemma OAI.CriticalHoneycomb.FiniteFunctional.finite_endpoint_constraints line 369
  42. lemma OAI.CriticalHoneycomb.FiniteFunctional.interpolant_eq_integralInterpolant line 415
  43. lemma OAI.CriticalHoneycomb.FiniteFunctional.interpolant_fusion_eq_integral_eventually line 423