OAI/Combinatorics/HoneycombChords/HyperbolicTransform.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Hyperbolic integral transforms, their domination estimates, and derivatives.

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

  1. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.real_unit_mem_integerComplement line 13
  2. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.cot_sum_real line 21
  3. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.shifted_reciprocal_sums line 31
  4. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.positive_shifted_reciprocal_hasSum line 40
  5. def OAI.CriticalHoneycomb.FiniteFunctional.Analytic.tanTerm line 58
  6. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.tanTerm_nonneg line 60
  7. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.tan_partial_fractions line 66
  8. def OAI.CriticalHoneycomb.FiniteFunctional.Analytic.laplaceTerm line 93
  9. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.laplaceTerm_nonneg line 96
  10. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.laplaceTerm_integrable line 101
  11. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.laplaceTerm_integral line 106
  12. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.laplaceTerm_factor line 115
  13. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.sinh_quotient_exponential line 121
  14. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.sinh_kernel_hasSum line 135
  15. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.sinh_kernel_integral_nonneg line 144
  16. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.sinh_kernel_integrable_nonneg line 163
  17. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.sinh_kernel_integrable line 170
  18. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.sinh_kernel_integral line 178
  19. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.cosh_sinh_split line 194
  20. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.cosh_sinh_kernel_integrable line 199
  21. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.cosh_sinh_kernel_integral_tan line 209
  22. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.tan_midpoint_identity line 220
  23. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.cosh_sinh_kernel_integral line 235
  24. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.exp_mul_sinh_le_sinh_add line 247
  25. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.pow_mul_exp_le_sinh line 255
  26. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.polynomial_kernel_integrable line 277
  27. def OAI.CriticalHoneycomb.FiniteFunctional.Analytic.hypJet line 300
  28. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.hypJet_zero line 302
  29. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.hypJet_one line 303
  30. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.hypJet_hasDerivAt line 304
  31. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.hypJet_abs_le line 310
  32. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.cosh_abs_le_exp_abs line 318
  33. def OAI.CriticalHoneycomb.FiniteFunctional.Analytic.transformJet line 320
  34. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.transformJet_zero line 322
  35. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.transformJet_hasDerivAt line 325
  36. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.transformJet_norm_le line 333
  37. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.transformJet_integrable line 347