OAI/Combinatorics/StripMass/DeformationWeights.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. lemma OAI.CriticalStrip.Diagram.lambda_pos line 16
  2. lemma OAI.CriticalStrip.Diagram.L_deformation_pos line 18
  3. lemma OAI.CriticalStrip.Diagram.physicalWeights_deformation_pos line 23
  4. lemma OAI.CriticalStrip.Diagram.physicalWeights_deformation_tile_nonneg line 39
  5. lemma OAI.CriticalStrip.Diagram.physicalWeights_two_lambda_nonneg line 52
  6. lemma OAI.CriticalStrip.Diagram.physicalWeights_two_lambda_pos line 57
  7. lemma OAI.CriticalStrip.Diagram.northInjection_nonneg line 63
  8. def OAI.CriticalStrip.Diagram.augmentedPhysicalWeights line 67
  9. def OAI.CriticalStrip.Diagram.deformationAngles line 70
  10. def OAI.CriticalStrip.Diagram.deformationWeights line 72
  11. lemma OAI.CriticalStrip.Diagram.deformationWeights_eq line 75
  12. lemma OAI.CriticalStrip.Diagram.deformationWeights_physical line 91
  13. lemma OAI.CriticalStrip.Diagram.deformationWeights_flat line 98
  14. lemma OAI.CriticalStrip.Diagram.augmentedPhysical_tile_nonneg line 101
  15. lemma OAI.CriticalStrip.Diagram.deformationWeights_nonnegative line 107
  16. lemma OAI.CriticalStrip.Diagram.deformationWeights_accessible line 116
  17. lemma OAI.CriticalStrip.Diagram.deformationAngles_scalar_ne_zero line 147
  18. lemma OAI.CriticalStrip.Diagram.deformationAngles_L_ne_zero line 163
  19. lemma OAI.CriticalStrip.Diagram.deformationWeights_stationary line 169
  20. lemma OAI.CriticalStrip.Diagram.continuousOn_column line 182
  21. lemma OAI.CriticalStrip.Diagram.continuousOn_deformationWeights_tile line 198
  22. lemma OAI.CriticalStrip.Diagram.continuousOn_deformationColumn line 212
  23. lemma OAI.CriticalStrip.Diagram.continuous_deformationAngles line 221
  24. lemma OAI.CriticalStrip.Diagram.continuousOn_deformationVector line 228
  25. lemma OAI.CriticalStrip.Diagram.summablePowers_flat_bottom line 239
  26. theorem OAI.CriticalStrip.Diagram.augmentedPhysical_summablePowers line 258
  27. lemma OAI.CriticalStrip.PositiveMatrix.Nonnegative.submatrix line 294
  28. lemma OAI.CriticalStrip.PositiveMatrix.submatrix_pow_le line 300
  29. lemma OAI.CriticalStrip.PositiveMatrix.SummablePowers.submatrix line 317
  30. lemma OAI.CriticalStrip.PositiveMatrix.SummablePowers.transpose line 326
  31. lemma OAI.CriticalStrip.PositiveMatrix.summablePowers_of_zero_rows line 331
  32. lemma OAI.CriticalStrip.Diagram.augmentedPhysical_nonnegative line 353
  33. def OAI.CriticalStrip.Diagram.vacuumAugmentEmbedding line 359
  34. def OAI.CriticalStrip.Diagram.sourceAugmentEmbedding line 362
  35. lemma OAI.CriticalStrip.Diagram.augmentedPhysical_vacuum_block line 365
  36. lemma OAI.CriticalStrip.Diagram.augmentedPhysical_source_block line 375
  37. theorem OAI.CriticalStrip.Diagram.physical_vacuum_summablePowers line 384
  38. theorem OAI.CriticalStrip.Diagram.physical_source_summablePowers line 391
  39. lemma OAI.CriticalStrip.Diagram.physical_column_nonnegative line 398
  40. lemma OAI.CriticalStrip.Diagram.physical_source_nonnegative line 403
  41. lemma OAI.CriticalStrip.Diagram.homogeneous_angleScalar_ne_zero line 408
  42. lemma OAI.CriticalStrip.Diagram.homogeneous_L_ne_zero line 413
  43. theorem OAI.CriticalStrip.Diagram.physical_vacuum_eq_tsum line 418
  44. theorem OAI.CriticalStrip.Diagram.physical_vacuum_nonneg line 427
  45. theorem OAI.CriticalStrip.Diagram.physical_northSource_eq_tsum line 438
  46. theorem OAI.CriticalStrip.Diagram.physical_source_weighted_summable line 449