OAI/Combinatorics/StripMass/StieltjesLimits.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. theorem OAI.CriticalStrip.tendsto_realStieltjes_zero line 13
  2. theorem OAI.CriticalStrip.polynomial_constant_of_limit line 25
  3. theorem OAI.CriticalStrip.moments_zero_of_stieltjes_decay line 44
  4. def OAI.CriticalStrip.fBranch line 95
  5. def OAI.CriticalStrip.projectionF line 96
  6. def OAI.CriticalStrip.projectionD line 98
  7. theorem OAI.CriticalStrip.integrableOn_omega_projection line 101
  8. theorem OAI.CriticalStrip.offCut_one_neg line 115
  9. theorem OAI.CriticalStrip.offCut_neg_one_pos line 120
  10. theorem OAI.CriticalStrip.integrableOn_projection_weight line 125
  11. theorem OAI.CriticalStrip.fBranch_transform line 137
  12. theorem OAI.CriticalStrip.fBranch_square_transform line 149
  13. theorem OAI.CriticalStrip.projectionF_polynomial line 163
  14. theorem OAI.CriticalStrip.norm_neg_atTop line 190
  15. theorem OAI.CriticalStrip.projectionF_cauchy line 195
  16. theorem OAI.CriticalStrip.projection_moments_of_decay line 216
  17. theorem OAI.CriticalStrip.projectionD_cauchy line 233
  18. def OAI.CriticalStrip.tildePoly line 295
  19. theorem OAI.CriticalStrip.affine_natDegree line 298
  20. theorem OAI.CriticalStrip.affine_leadingCoeff line 303
  21. theorem OAI.CriticalStrip.tildePoly_natDegree_le line 308
  22. theorem OAI.CriticalStrip.tildePoly_eval line 313
  23. theorem OAI.CriticalStrip.tildePoly_eq_zero_iff line 331
  24. theorem OAI.CriticalStrip.tildePoly_zero_of_degree_lt line 343
  25. def OAI.CriticalStrip.highBranch line 356
  26. def OAI.CriticalStrip.lowBranch line 357
  27. theorem OAI.CriticalStrip.sqrt_half line 359
  28. theorem OAI.CriticalStrip.sqrt_two_lt_two line 366
  29. theorem OAI.CriticalStrip.highBranch_zero line 371
  30. theorem OAI.CriticalStrip.lowBranch_zero line 381
  31. theorem OAI.CriticalStrip.highBranch_continuous line 393
  32. theorem OAI.CriticalStrip.lowBranch_continuous line 394
  33. theorem OAI.CriticalStrip.branches_sq line 396
  34. theorem OAI.CriticalStrip.branches_harmonic line 406
  35. theorem OAI.CriticalStrip.branches_sum line 413