OAI/Combinatorics/StripMass/MonicPositive.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. lemma OAI.CriticalStrip.projectionF_high_scaled_limit line 15
  2. lemma OAI.CriticalStrip.projectionF_cauchy_scaled_limit line 39
  3. theorem OAI.CriticalStrip.MonicProblem.eval_C_pos line 55
  4. lemma OAI.CriticalStrip.Diagram.scalarValue_continuous line 90
  5. lemma OAI.CriticalStrip.Diagram.homogeneous_discriminant_ne_zero line 95
  6. def OAI.CriticalStrip.Diagram.separatedHomogeneous line 109
  7. lemma OAI.CriticalStrip.Diagram.separatedHomogeneous_injective line 112
  8. lemma OAI.CriticalStrip.Diagram.separatedHomogeneous_tendsto line 120
  9. lemma OAI.CriticalStrip.Diagram.separatedHomogeneous_discriminants line 127
  10. lemma OAI.CriticalStrip.Diagram.polynomial_eval_limit_of_coeff line 139
  11. theorem OAI.CriticalStrip.Diagram.archPolynomialAt_homogeneous_of_ne line 150
  12. lemma OAI.CriticalStrip.Diagram.nextScalar_homogeneous_of_ne line 192
  13. theorem OAI.CriticalStrip.Diagram.scalarValue_homogeneous_positive line 203
  14. lemma OAI.CriticalStrip.projectionD_nonneg_right line 238
  15. lemma OAI.CriticalStrip.integral_cauchyDensity_lower line 258
  16. lemma OAI.CriticalStrip.projectionF_continuousAt line 271
  17. lemma OAI.CriticalStrip.projectionF_one_neg line 278
  18. lemma OAI.CriticalStrip.branches_inverse line 306
  19. lemma OAI.CriticalStrip.branches_order line 329
  20. lemma OAI.CriticalStrip.projection_low_difference line 333
  21. theorem OAI.CriticalStrip.MonicProblem.eval_pos_between line 352
  22. lemma OAI.CriticalStrip.Diagram.c_eq_critical line 416
  23. lemma OAI.CriticalStrip.Diagram.scalarValue_homogeneous_ne_zero line 421
  24. theorem OAI.CriticalStrip.Diagram.archPolynomialAt_homogeneous line 429
  25. lemma OAI.CriticalStrip.Diagram.nextScalar_homogeneous line 434
  26. lemma OAI.CriticalStrip.MonicProblem.eval_c line 448
  27. theorem OAI.CriticalStrip.MonicProblem.eval_pos_Icc line 470
  28. theorem OAI.CriticalStrip.Diagram.scalarValue_deformation_positive line 490
  29. lemma OAI.CriticalStrip.Diagram.scalarValue_deformation_ne_zero line 509
  30. lemma OAI.CriticalStrip.Diagram.cosine_deformation line 515