OAI/Combinatorics/StripMass/RightStieltjes.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. lemma OAI.CriticalStrip.transformed_omega_extended line 15
  2. lemma OAI.CriticalStrip.omega_resolvent_extended line 33
  3. lemma OAI.CriticalStrip.stieltjes_omega_right line 59
  4. lemma OAI.CriticalStrip.transformed_squareWeight_extended line 88
  5. lemma OAI.CriticalStrip.squareWeight_resolvent_extended line 101
  6. lemma OAI.CriticalStrip.stieltjes_omega_square_right line 133
  7. lemma OAI.CriticalStrip.offCut_of_outside line 167
  8. lemma OAI.CriticalStrip.fBranch_transform_outside line 172
  9. lemma OAI.CriticalStrip.fBranch_square_transform_outside line 186
  10. lemma OAI.CriticalStrip.projectionF_polynomial_outside line 204
  11. lemma OAI.CriticalStrip.projectionF_cauchy_outside line 231
  12. lemma OAI.CriticalStrip.lagrange_reverse_cauchy_sum line 264
  13. def OAI.CriticalStrip.reflectionCauchyKernel line 298
  14. lemma OAI.CriticalStrip.measurable_reflectionCauchyKernel line 301
  15. lemma OAI.CriticalStrip.integrable_reflectionCauchyKernel line 305
  16. lemma OAI.CriticalStrip.reflectionCauchyKernel_sum_swaps line 317
  17. def OAI.CriticalStrip.cauchyDensity line 355
  18. lemma OAI.CriticalStrip.integrable_cauchyDensity line 358
  19. lemma OAI.CriticalStrip.integral_cauchyDensity_pos line 374
  20. lemma OAI.CriticalStrip.integral_reflectionCauchyKernel line 383
  21. lemma OAI.CriticalStrip.integral_density_unitCube_positive line 408
  22. lemma OAI.CriticalStrip.reflection_expectation_cauchy line 413
  23. lemma OAI.CriticalStrip.projection_initial_monic line 448
  24. lemma OAI.CriticalStrip.projectionF_positive_cauchy line 460
  25. lemma OAI.CriticalStrip.projectionF_neg line 497
  26. lemma OAI.CriticalStrip.scaled_cauchyDensity line 513
  27. lemma OAI.CriticalStrip.scaled_cauchyDensity_bound line 522
  28. lemma OAI.CriticalStrip.cauchyDensity_limit line 540