OAI/Analysis/FreeGroupFactor/RadialCoefficients.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FreeGroupFactorMain.coefficientSqNorm line 14
  2. theorem OAI.FreeGroupFactorMain.coefficientSqNorm_nonneg line 16
  3. theorem OAI.FreeGroupFactorMain.coefficientSqNorm_zero line 19
  4. theorem OAI.FreeGroupFactorMain.coefficientSqNorm_single line 22
  5. theorem OAI.FreeGroupFactorMain.coefficientSqNorm_smul line 26
  6. theorem OAI.FreeGroupFactorMain.coefficientSqNorm_add_of_disjoint line 33
  7. theorem OAI.FreeGroupFactorMain.coefficientSqNorm_sum_of_disjoint line 53
  8. theorem OAI.FreeGroupFactorMain.coefficientSqNorm_sum_le line 72
  9. theorem OAI.FreeGroupFactorMain.coefficientSqNorm_add_le line 97
  10. def OAI.FreeGroupFactorMain.Radial.paths line 106
  11. def OAI.FreeGroupFactorMain.Radial.sphere line 110
  12. theorem OAI.FreeGroupFactorMain.Radial.paths_mem_length line 114
  13. theorem OAI.FreeGroupFactorMain.Radial.sphere_mem_length line 123
  14. theorem OAI.FreeGroupFactorMain.Radial.cons_images_disjoint line 133
  15. theorem OAI.FreeGroupFactorMain.Radial.card_paths line 141
  16. theorem OAI.FreeGroupFactorMain.Radial.card_sphere_succ line 152
  17. def OAI.FreeGroupFactorMain.Radial.signed line 160
  18. theorem OAI.FreeGroupFactorMain.Radial.signed_length line 165
  19. theorem OAI.FreeGroupFactorMain.Radial.signed_map_fst line 171
  20. theorem OAI.FreeGroupFactorMain.Radial.signed_injective line 178
  21. theorem OAI.FreeGroupFactorMain.Radial.signed_reduced_paths line 182
  22. theorem OAI.FreeGroupFactorMain.Radial.signed_reduced_sphere line 196
  23. def OAI.FreeGroupFactorMain.Radial.vertex line 208
  24. theorem OAI.FreeGroupFactorMain.Radial.toWord_vertex line 210
  25. theorem OAI.FreeGroupFactorMain.Radial.vertex_injOn line 214
  26. theorem OAI.FreeGroupFactorMain.Radial.sum_sphere_succ line 221
  27. theorem OAI.FreeGroupFactorMain.Radial.sum_paths_succ line 229
  28. theorem OAI.FreeGroupFactorMain.Radial.vertex_nil line 238
  29. theorem OAI.FreeGroupFactorMain.Radial.vertex_cons_true line 241
  30. theorem OAI.FreeGroupFactorMain.Radial.vertex_cons_false line 246
  31. def OAI.FreeGroupFactorMain.Radial.shell line 250
  32. def OAI.FreeGroupFactorMain.Radial.shift line 253
  33. theorem OAI.FreeGroupFactorMain.Radial.shift_single line 257
  34. def OAI.FreeGroupFactorMain.Radial.sumShift line 261
  35. theorem OAI.FreeGroupFactorMain.Radial.sumShift_apply line 265
  36. theorem OAI.FreeGroupFactorMain.Radial.shell_zero line 269
  37. theorem OAI.FreeGroupFactorMain.Radial.shell_succ line 272
  38. theorem OAI.FreeGroupFactorMain.Radial.outward_shell line 277
  39. theorem OAI.FreeGroupFactorMain.Radial.sumShift_shell line 289
  40. theorem OAI.FreeGroupFactorMain.Radial.sumShift_shell_one line 305
  41. theorem OAI.FreeGroupFactorMain.Radial.inward_shell line 311
  42. theorem OAI.FreeGroupFactorMain.Radial.sumShift_shell_succ line 320
  43. def OAI.FreeGroupFactorMain.Radial.vertices line 326
  44. theorem OAI.FreeGroupFactorMain.Radial.shell_eq_sum_vertices line 329
  45. theorem OAI.FreeGroupFactorMain.Radial.shell_apply line 334
  46. theorem OAI.FreeGroupFactorMain.Radial.shell_support line 339
  47. theorem OAI.FreeGroupFactorMain.Radial.card_vertices line 345
  48. theorem OAI.FreeGroupFactorMain.Radial.vertices_disjoint line 349
  49. def OAI.FreeGroupFactorMain.Radial.rightShell line 362
  50. def OAI.FreeGroupFactorMain.Radial.leftShell line 365
  51. theorem OAI.FreeGroupFactorMain.Radial.sqNorm_shell_succ line 368
  52. theorem OAI.FreeGroupFactorMain.Radial.sumShift_rightShell_zero line 380
  53. theorem OAI.FreeGroupFactorMain.Radial.sumShift_rightShell_succ line 388
  54. theorem OAI.FreeGroupFactorMain.Radial.sqNorm_rightShell line 406
  55. theorem OAI.FreeGroupFactorMain.Radial.sqNorm_leftShell line 417
  56. def OAI.FreeGroupFactorMain.Radial.partialInverse line 429
  57. theorem OAI.FreeGroupFactorMain.Radial.partialInverse_zero line 432
  58. theorem OAI.FreeGroupFactorMain.Radial.partialInverse_succ line 435
  59. theorem OAI.FreeGroupFactorMain.Radial.sumShift_partialInverse line 439
  60. theorem OAI.FreeGroupFactorMain.Radial.rightShell_disjoint line 450
  61. theorem OAI.FreeGroupFactorMain.Radial.leftShell_disjoint line 456
  62. theorem OAI.FreeGroupFactorMain.Radial.sqNorm_partialInverse line 462
  63. def OAI.FreeGroupFactorMain.Radial.averagedInverse line 473
  64. theorem OAI.FreeGroupFactorMain.Radial.sumShift_averagedInverse line 476
  65. theorem OAI.FreeGroupFactorMain.Radial.sqNorm_averagedInverse_le line 487
  66. theorem OAI.FreeGroupFactorMain.Radial.sqNorm_averagedInverse_residual line 510
  67. theorem OAI.FreeGroupFactorMain.Radial.sqNorm_averagedInverse_residual_le line 525
  68. def OAI.FreeGroupFactorMain.Radial.prefixSumOperator line 535
  69. theorem OAI.FreeGroupFactorMain.Radial.sqNorm_prefixSum_residual_le line 538
  70. theorem OAI.FreeGroupFactorMain.Radial.exists_small_prefix_inverse line 547