OAI/Combinatorics/StripMass/ReflectionIntegrals.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. lemma OAI.CriticalStrip.integral_reflectionResidueKernel_eq_zero_index line 13
  2. lemma OAI.CriticalStrip.integral_reflectionResidueKernel_zero_index line 24
  3. lemma OAI.CriticalStrip.reflection_partialFractions_density line 39
  4. lemma OAI.CriticalStrip.expectation_reflection_cauchy line 55
  5. theorem OAI.CriticalStrip.reflection_expectation_cauchyMomentProblem line 83
  6. lemma OAI.CriticalStrip.harmonicCoordinate_natDegree line 110
  7. lemma OAI.CriticalStrip.harmonicCoordinate_leadingCoeff line 114
  8. lemma OAI.CriticalStrip.degree_lt_implies_natDegree_lt line 120
  9. lemma OAI.CriticalStrip.coeff_comp_top_of_le line 126
  10. lemma OAI.CriticalStrip.tildePoly_eval_zero line 137
  11. lemma OAI.CriticalStrip.comp_harmonic_odd line 146
  12. lemma OAI.CriticalStrip.projection_top_coefficients line 154
  13. lemma OAI.CriticalStrip.homogeneousQ_monic line 189
  14. lemma OAI.CriticalStrip.homogeneousQ_natDegree line 193
  15. lemma OAI.CriticalStrip.homogeneousQ_nextCoeff line 200
  16. lemma OAI.CriticalStrip.projectionD_expectation line 214
  17. lemma OAI.CriticalStrip.tendsto_scaled_fBranch_sq_zero line 273
  18. lemma OAI.CriticalStrip.tendsto_scaled_fBranch_zero line 286
  19. lemma OAI.CriticalStrip.projectionF_sub_initial_limit line 296
  20. lemma OAI.CriticalStrip.defect_resolvent_limit line 318
  21. lemma OAI.CriticalStrip.projectionF_sub_initial_integral line 341
  22. lemma OAI.CriticalStrip.homogeneous_projection_integral_coefficient line 398
  23. lemma OAI.CriticalStrip.eta_pos line 412
  24. lemma OAI.CriticalStrip.C_eta_identity line 421
  25. theorem OAI.CriticalStrip.homogeneous_arch_coefficient_integral line 437
  26. theorem OAI.CriticalStrip.homogeneous_arch_coefficient_growth line 460