OAI/Combinatorics/HoneycombChords/SechTransform.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Exact hyperbolic secant integral transforms and pairings.

  1. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.sech_split line 10
  2. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.sech_kernel_integrable_pi4 line 18
  3. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.sech_kernel_integral_pi4 line 24
  4. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.sech_scale_bound line 37
  5. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.sech_scaled_kernel line 43
  6. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.sech_kernel_integrable line 48
  7. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.sech_kernel_integral line 54
  8. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.cosh_pair_split line 65
  9. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.sech_pair_integrable line 70
  10. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.sech_pair_integral line 79