OAI/Combinatorics/Coboundary/Expansion.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

Local repairs, fat-ladder inequalities, and uniform raw cosystolic expansion.

  1. def OAI.CoboundaryExpanders.FatLadders.linkRestrict line 20
  2. def OAI.CoboundaryExpanders.FatLadders.linkLift line 21
  3. def OAI.CoboundaryExpanders.FatLadders.linkNorm line 24
  4. lemma OAI.CoboundaryExpanders.FatLadders.linkLift_support line 28
  5. lemma OAI.CoboundaryExpanders.FatLadders.delta_linkLift line 32
  6. lemma OAI.CoboundaryExpanders.FatLadders.delta_linkRestrict line 51
  7. lemma OAI.CoboundaryExpanders.FatLadders.starNorm_linkNorm line 76
  8. lemma OAI.CoboundaryExpanders.FatLadders.linkNorm_congr line 101
  9. theorem OAI.CoboundaryExpanders.FatLadders.linkCorrection_of_links line 110
  10. def OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.rawNorm line 154
  11. lemma OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.rawNorm_nonneg line 157
  12. lemma OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.rawNorm_weight line 162
  13. theorem OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.raw_correction line 185
  14. lemma OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.linkNorm_cofaces line 200
  15. lemma OAI.CoboundaryExpanders.TypedCosetFaces.IsFace.type_injective line 239
  16. def OAI.CoboundaryExpanders.TypedCosetFaces.faceStabilizer line 249
  17. lemma OAI.CoboundaryExpanders.TypedCosetFaces.faceStabilizer_fixes line 252
  18. lemma OAI.CoboundaryExpanders.TypedCosetFaces.facesLinkInvariant line 255
  19. lemma OAI.CoboundaryExpanders.TypedCosetFaces.facesLinkTransitive line 271
  20. lemma OAI.CoboundaryExpanders.TypedCosetFaces.delta_agrees line 311
  21. theorem OAI.CoboundaryExpanders.TypedCosetFaces.linkCorrection_of_cones line 315
  22. theorem OAI.CoboundaryExpanders.Construction.uniform_actual_linkCorrection line 355
  23. lemma OAI.CoboundaryExpanders.FatLadders.delta_zero line 379
  24. lemma OAI.CoboundaryExpanders.FatLadders.delta_add line 381
  25. lemma OAI.CoboundaryExpanders.FatLadders.delta_insert line 386
  26. theorem OAI.CoboundaryExpanders.FatLadders.delta_delta line 396
  27. lemma OAI.CoboundaryExpanders.FatLadders.delta_support line 414
  28. lemma OAI.CoboundaryExpanders.FatLadders.norm_zero line 422
  29. lemma OAI.CoboundaryExpanders.FatLadders.norm_add_le line 425
  30. def OAI.CoboundaryExpanders.FatLadders.WeightedEq line 430
  31. lemma OAI.CoboundaryExpanders.FatLadders.WeightedEq.atom_eq line 434
  32. lemma OAI.CoboundaryExpanders.FatLadders.WeightedEq.norm_eq line 441
  33. lemma OAI.CoboundaryExpanders.FatLadders.WeightedEq.starNorm_eq line 445
  34. lemma OAI.CoboundaryExpanders.FatLadders.WeightedEq.add_right line 452
  35. lemma OAI.CoboundaryExpanders.FatLadders.WeightedEq.delta_eq line 457
  36. lemma OAI.CoboundaryExpanders.FatLadders.WeightedEq.nearMinimal line 470
  37. lemma OAI.CoboundaryExpanders.FatLadders.fatFamily_top_eq line 476
  38. theorem OAI.CoboundaryExpanders.FatLadders.small_cochain_expansion line 486
  39. structure OAI.CoboundaryExpanders.LocalRepair.Size line 515
  40. instance OAI.CoboundaryExpanders.LocalRepair.(instance at line 521) line 521
  41. theorem OAI.CoboundaryExpanders.LocalRepair.repair line 523
  42. theorem OAI.CoboundaryExpanders.LocalRepair.cosystolic_correction line 551
  43. lemma OAI.CoboundaryExpanders.FatLadders.support_starNorm line 584
  44. lemma OAI.CoboundaryExpanders.FatLadders.local_global_difference line 592
  45. theorem OAI.CoboundaryExpanders.FatLadders.nearMinimal_repair_step line 603
  46. def OAI.CoboundaryExpanders.FatLadders.normSize line 646
  47. def OAI.CoboundaryExpanders.FatLadders.deltaHom line 653
  48. theorem OAI.CoboundaryExpanders.FatLadders.repair_coboundary line 658
  49. lemma OAI.CoboundaryExpanders.FatLadders.norm_le_choose line 680
  50. theorem OAI.CoboundaryExpanders.FatLadders.cosystolic_from_local line 688
  51. theorem OAI.CoboundaryExpanders.FatLadders.uniform_cosystolic_from_local line 731
  52. lemma OAI.CoboundaryExpanders.FatLadders.atom_scale line 773
  53. lemma OAI.CoboundaryExpanders.FatLadders.norm_scale line 778
  54. lemma OAI.CoboundaryExpanders.FatLadders.starSum_scale line 781
  55. lemma OAI.CoboundaryExpanders.FatLadders.starNorm_scale line 787
  56. lemma OAI.CoboundaryExpanders.FatLadders.collisionMass_scale line 794
  57. lemma OAI.CoboundaryExpanders.FatLadders.Balanced.scale line 800
  58. lemma OAI.CoboundaryExpanders.FatLadders.LinkCorrection.scale line 806
  59. lemma OAI.CoboundaryExpanders.FatLadders.LinkCorrection.mono line 813
  60. lemma OAI.CoboundaryExpanders.FatLadders.LocalMixing.scale line 818
  61. lemma OAI.CoboundaryExpanders.FatLadders.LocalMixing.mono line 828
  62. theorem OAI.CoboundaryExpanders.FatLadders.uniform_all_cosystolic_from_local line 838
  63. theorem OAI.CoboundaryExpanders.FatLadders.uniform_raw_cosystolic_from_local line 870
  64. theorem OAI.CoboundaryExpanders.Construction.uniform_actual_raw_cosystolic line 892