OAI/Combinatorics/StripMass/CauchyMatrices.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. def OAI.CriticalStrip.boundedCauchyMatrix line 14
  2. theorem OAI.CriticalStrip.basisDet_eq line 17
  3. theorem OAI.CriticalStrip.boundedCauchyMatrix_det line 27
  4. theorem OAI.CriticalStrip.basis_cauchy_basis_eq line 34
  5. theorem OAI.CriticalStrip.basis_cauchy_basis_nonneg line 41
  6. theorem OAI.CriticalStrip.basis_cauchy_basis_pos line 50
  7. theorem OAI.CriticalStrip.product_restrict_cube line 59
  8. theorem OAI.CriticalStrip.integral_pos_on_cube line 64
  9. theorem OAI.CriticalStrip.integral_cauchy_basis line 88
  10. theorem OAI.CriticalStrip.integrable_cauchy_basis line 101
  11. theorem OAI.CriticalStrip.basis_transformed_nonneg line 108
  12. theorem OAI.CriticalStrip.basis_transformed_pos line 122
  13. theorem OAI.CriticalStrip.det_momentMatrix_pos line 136
  14. def OAI.CriticalStrip.cauchyDefect line 151
  15. def OAI.CriticalStrip.CauchyMomentProblem line 154
  16. theorem OAI.CriticalStrip.cauchyDefect_moment line 157
  17. theorem OAI.CriticalStrip.cauchyMomentProblem_iff line 181
  18. theorem OAI.CriticalStrip.existsUnique_cauchyMomentProblem line 189
  19. theorem OAI.CriticalStrip.cauchyMomentProblem_zero line 202
  20. def OAI.CriticalStrip.quarticDen line 217
  21. def OAI.CriticalStrip.quarticBase line 218
  22. def OAI.CriticalStrip.quarticWeighted line 219
  23. def OAI.CriticalStrip.straightener line 220
  24. theorem OAI.CriticalStrip.quarticDen_pos line 222
  25. theorem OAI.CriticalStrip.straightener_deriv line 226
  26. theorem OAI.CriticalStrip.straightener_inj line 231
  27. theorem OAI.CriticalStrip.straightener_image line 239
  28. theorem OAI.CriticalStrip.scaled_cauchy line 253
  29. theorem OAI.CriticalStrip.quartic_base_integral line 267
  30. theorem OAI.CriticalStrip.integral_reciprocal line 293
  31. theorem OAI.CriticalStrip.quartic_weighted_integral line 321
  32. def OAI.CriticalStrip.uniformDen line 357
  33. def OAI.CriticalStrip.uniformizer line 358
  34. theorem OAI.CriticalStrip.uniformDen_pos line 360
  35. theorem OAI.CriticalStrip.uniformizer_mem line 364
  36. theorem OAI.CriticalStrip.uniformizer_deriv line 372
  37. theorem OAI.CriticalStrip.uniformizer_inj line 381
  38. theorem OAI.CriticalStrip.omega_uniformizer line 389
  39. theorem OAI.CriticalStrip.uniformizer_image line 399