OAI/Combinatorics/StripMass/RealEvaluation.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. def OAI.CriticalStrip.Diagram.anglePhase line 14
  2. lemma OAI.CriticalStrip.Diagram.anglePhase_ne_zero line 16
  3. lemma OAI.CriticalStrip.Diagram.anglePhase_zero line 17
  4. lemma OAI.CriticalStrip.Diagram.anglePhase_add line 18
  5. lemma OAI.CriticalStrip.Diagram.anglePhase_neg line 20
  6. lemma OAI.CriticalStrip.Diagram.anglePhase_sub line 22
  7. lemma OAI.CriticalStrip.Diagram.anglePhase_nat_mul line 24
  8. lemma OAI.CriticalStrip.Diagram.anglePhase_int_mul line 26
  9. lemma OAI.CriticalStrip.Diagram.anglePhase_lambda line 28
  10. lemma OAI.CriticalStrip.Diagram.anglePhase_sine line 29
  11. lemma OAI.CriticalStrip.Diagram.anglePhase_cosine line 33
  12. def OAI.CriticalStrip.Diagram.angleCharacter line 37
  13. def OAI.CriticalStrip.Diagram.angleEvaluation line 44
  14. lemma OAI.CriticalStrip.Diagram.angleEvaluation_monomial line 47
  15. lemma OAI.CriticalStrip.Diagram.angleEvaluation_constant line 50
  16. lemma OAI.CriticalStrip.Diagram.angleEvaluation_variable line 54
  17. lemma OAI.CriticalStrip.Diagram.rationalAt_const_complex line 58
  18. lemma OAI.CriticalStrip.Diagram.rationalAt_angle_variable line 65
  19. lemma OAI.CriticalStrip.Diagram.rationalAt_angle_sin line 73
  20. lemma OAI.CriticalStrip.Diagram.rationalAt_angle_cos line 81
  21. lemma OAI.CriticalStrip.Diagram.rationalAt_angle_L line 87
  22. lemma OAI.CriticalStrip.Diagram.rationalAt_angle_weights line 96
  23. lemma OAI.CriticalStrip.Diagram.rationalAt_angle_spectralA line 122
  24. lemma OAI.CriticalStrip.Diagram.rationalAt_angle_spectralWeights line 131
  25. lemma OAI.CriticalStrip.Diagram.angleEvaluation_rowCosine line 140
  26. lemma OAI.CriticalStrip.Diagram.angleEvaluation_scalar line 146
  27. lemma OAI.CriticalStrip.Diagram.continuous_angleEvaluation line 159
  28. def OAI.CriticalStrip.PositiveMatrix.Nonnegative line 194
  29. def OAI.CriticalStrip.PositiveMatrix.SummablePowers line 196
  30. def OAI.CriticalStrip.PositiveMatrix.Accessible line 198
  31. lemma OAI.CriticalStrip.PositiveMatrix.Nonnegative.pow line 201
  32. lemma OAI.CriticalStrip.PositiveMatrix.Nonnegative.mulVec line 211
  33. lemma OAI.CriticalStrip.PositiveMatrix.Nonnegative.mulVec_mono line 216
  34. lemma OAI.CriticalStrip.PositiveMatrix.entry_mul_le_mulVec line 221
  35. lemma OAI.CriticalStrip.PositiveMatrix.stationary_partial_sum line 225
  36. lemma OAI.CriticalStrip.PositiveMatrix.summable_injection line 236
  37. theorem OAI.CriticalStrip.PositiveMatrix.summablePowers_of_stationary line 247
  38. lemma OAI.CriticalStrip.PositiveMatrix.SummablePowers.tendsto_zero line 259
  39. lemma OAI.CriticalStrip.PositiveMatrix.SummablePowers.mulVec_tendsto_zero line 262
  40. lemma OAI.CriticalStrip.PositiveMatrix.SummablePowers.mulVec_summable line 267
  41. lemma OAI.CriticalStrip.PositiveMatrix.SummablePowers.stationary_eq_tsum line 273
  42. lemma OAI.CriticalStrip.PositiveMatrix.SummablePowers.stationary_nonneg line 286
  43. lemma OAI.CriticalStrip.PositiveMatrix.SummablePowers.unique_stationary line 293
  44. lemma OAI.CriticalStrip.PositiveMatrix.pow_mulVec_le line 299
  45. lemma OAI.CriticalStrip.PositiveMatrix.summablePowers_of_le line 317
  46. def OAI.CriticalStrip.PositiveMatrix.HasSupervector line 328
  47. lemma OAI.CriticalStrip.PositiveMatrix.HasSupervector.summablePowers line 331
  48. lemma OAI.CriticalStrip.PositiveMatrix.SummablePowers.hasSupervector line 348
  49. lemma OAI.CriticalStrip.PositiveMatrix.hasSupervector_iff line 373
  50. lemma OAI.CriticalStrip.PositiveMatrix.isOpen_hasSupervector line 377
  51. theorem OAI.CriticalStrip.PositiveMatrix.summablePowers_of_connected_stationary line 393
  52. theorem OAI.CriticalStrip.PositiveMatrix.summablePowers_on_Icc line 427
  53. theorem OAI.CriticalStrip.PositiveMatrix.SummablePowers.weighted line 447