OAI/Analysis/FreeGroupFactor/RankTwoCoefficients.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FreeGroupFactorMain.RankTwo.tupleSphere line 18
  2. theorem OAI.FreeGroupFactorMain.RankTwo.tupleSphere_image line 21
  3. theorem OAI.FreeGroupFactorMain.RankTwo.shell_eq_tuple line 35
  4. theorem OAI.FreeGroupFactorMain.RankTwo.pair_push_pattern_le line 43
  5. theorem OAI.FreeGroupFactorMain.RankTwo.pair_push_pattern_le_free_add line 63
  6. theorem OAI.FreeGroupFactorMain.RankTwo.right_pairColors_card line 81
  7. theorem OAI.FreeGroupFactorMain.RankTwo.positiveCount_even_add_two line 94
  8. theorem OAI.FreeGroupFactorMain.RankTwo.left_pairColors_card line 98
  9. theorem OAI.FreeGroupFactorMain.RankTwo.pair_shell_right_le line 109
  10. theorem OAI.FreeGroupFactorMain.RankTwo.pair_shell_left_le_free_add line 122
  11. theorem OAI.FreeGroupFactorMain.coefficientPair_nonneg line 142
  12. theorem OAI.FreeGroupFactorMain.coefficientPair_eq_zero_of_disjoint line 146
  13. theorem OAI.FreeGroupFactorMain.pushCoefficients_nonneg line 156
  14. def OAI.FreeGroupFactorMain.RankTwo.shellWeight line 172
  15. theorem OAI.FreeGroupFactorMain.RankTwo.shellWeight_nonneg line 174
  16. theorem OAI.FreeGroupFactorMain.RankTwo.shellWeight_product_bound line 180
  17. def OAI.FreeGroupFactorMain.RankTwo.rightConstant line 195
  18. def OAI.FreeGroupFactorMain.RankTwo.leftConstant line 196
  19. theorem OAI.FreeGroupFactorMain.RankTwo.pair_rightShell_le line 198
  20. theorem OAI.FreeGroupFactorMain.RankTwo.pair_leftShell_le_free_add line 214
  21. theorem OAI.FreeGroupFactorMain.RankTwo.pair_leftShell_free_le line 240
  22. theorem OAI.FreeGroupFactorMain.RankTwo.leftShell_nonneg line 251
  23. theorem OAI.FreeGroupFactorMain.RankTwo.pair_leftShell_push_nonneg line 258
  24. def OAI.FreeGroupFactorMain.RankTwo.partialConstant line 265
  25. def OAI.FreeGroupFactorMain.RankTwo.inverseConstant line 266
  26. def OAI.FreeGroupFactorMain.RankTwo.residualConstant line 268
  27. theorem OAI.FreeGroupFactorMain.RankTwo.rightConstant_nonneg line 271
  28. theorem OAI.FreeGroupFactorMain.RankTwo.leftConstant_nonneg line 272
  29. theorem OAI.FreeGroupFactorMain.RankTwo.partialConstant_nonneg line 273
  30. theorem OAI.FreeGroupFactorMain.RankTwo.inverseConstant_nonneg line 276
  31. theorem OAI.FreeGroupFactorMain.RankTwo.residualConstant_nonneg line 279
  32. theorem OAI.FreeGroupFactorMain.RankTwo.neg_one_pow_sq line 283
  33. theorem OAI.FreeGroupFactorMain.RankTwo.sqNorm_push_partial_le line 287
  34. theorem OAI.FreeGroupFactorMain.RankTwo.sqNorm_push_inverse_le line 307
  35. theorem OAI.FreeGroupFactorMain.RankTwo.signed_left_pair_le line 324
  36. theorem OAI.FreeGroupFactorMain.RankTwo.sqNorm_signed_left_sum_le line 339
  37. theorem OAI.FreeGroupFactorMain.RankTwo.sqNorm_push_residual_le line 370
  38. theorem OAI.FreeGroupFactorMain.RankTwo.exists_small_pushed_inverse line 386
  39. def OAI.FreeGroupFactorMain.RankTwo.twoGenerator line 412
  40. def OAI.FreeGroupFactorMain.RankTwo.realizeSummand line 414
  41. def OAI.FreeGroupFactorMain.RankTwo.realize line 419
  42. theorem OAI.FreeGroupFactorMain.RankTwo.realize_syllable line 421
  43. def OAI.FreeGroupFactorMain.RankTwo.syllabify line 424
  44. theorem OAI.FreeGroupFactorMain.RankTwo.syllabify_generator line 427
  45. theorem OAI.FreeGroupFactorMain.RankTwo.syllable_zpow line 430
  46. theorem OAI.FreeGroupFactorMain.RankTwo.syllabify_realize line 437
  47. theorem OAI.FreeGroupFactorMain.RankTwo.realize_injective line 445
  48. theorem OAI.FreeGroupFactorMain.pushCoefficients_comp line 452
  49. theorem OAI.FreeGroupFactorMain.coefficientSqNorm_shift line 460
  50. theorem OAI.FreeGroupFactorMain.freeCocycle_zpow_of_zero line 465
  51. def OAI.FreeGroupFactorMain.RankTwo.concretePrefix line 473
  52. def OAI.FreeGroupFactorMain.RankTwo.concreteWord line 474
  53. def OAI.FreeGroupFactorMain.RankTwo.concretePrefixHom line 476
  54. theorem OAI.FreeGroupFactorMain.RankTwo.concretePrefixHom_of line 479
  55. theorem OAI.FreeGroupFactorMain.RankTwo.concretePrefix_zero line 483
  56. theorem OAI.FreeGroupFactorMain.RankTwo.concretePrefix_succ line 484
  57. theorem OAI.FreeGroupFactorMain.RankTwo.cocycle_twoGenerator_true line 489
  58. theorem OAI.FreeGroupFactorMain.RankTwo.cocycle_twoGenerator_false line 493
  59. theorem OAI.FreeGroupFactorMain.RankTwo.cocycle_concretePrefix line 497
  60. theorem OAI.FreeGroupFactorMain.RankTwo.cocycle_concreteWord line 507
  61. theorem OAI.FreeGroupFactorMain.RankTwo.push_sumShift line 522
  62. theorem OAI.FreeGroupFactorMain.RankTwo.rank_two_cocycle_identity line 529
  63. theorem OAI.FreeGroupFactorMain.RankTwo.sqNorm_concrete_push line 536
  64. theorem OAI.FreeGroupFactorMain.smallCocycleTwo line 543