OAI/Combinatorics/Coboundary/Averaging.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

Finite F2 averaging and bounded-cone estimates for weighted local cochains.

  1. def OAI.CoboundaryExpanders.Averaging.supportNorm line 22
  2. lemma OAI.CoboundaryExpanders.Averaging.supportNorm_nonneg line 26
  3. lemma OAI.CoboundaryExpanders.Averaging.support_indicator_sum_le line 35
  4. lemma OAI.CoboundaryExpanders.Averaging.exists_le_of_sum_le line 51
  5. theorem OAI.CoboundaryExpanders.Averaging.exists_small_dual line 60
  6. lemma OAI.CoboundaryExpanders.Averaging.sum_smul line 130
  7. lemma OAI.CoboundaryExpanders.Averaging.action_average_eq line 134
  8. lemma OAI.CoboundaryExpanders.Averaging.transitive_average line 140
  9. theorem OAI.CoboundaryExpanders.Averaging.occupation_le_incidence line 153
  10. def OAI.CoboundaryExpanders.InfiniteChains.Cone.eval line 179
  11. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.eval_single line 182
  12. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.eval_support line 186
  13. def OAI.CoboundaryExpanders.InfiniteChains.Cone.delta line 197
  14. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.eval_delta line 200
  15. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.delta_eq_sum line 213
  16. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.delta_delta line 216
  17. def OAI.CoboundaryExpanders.InfiniteChains.Cone.correction line 222
  18. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.eval_correction line 226
  19. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.correction_identity line 239
  20. def OAI.CoboundaryExpanders.InfiniteChains.Cone.pull line 252
  21. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.eval_pull line 254
  22. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.delta_pull line 264
  23. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.pull_inv line 273
  24. def OAI.CoboundaryExpanders.InfiniteChains.Cone.movedCorrection line 277
  25. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.movedCorrection_identity line 280
  26. def OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.weight line 301
  27. lemma OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.weight_nonneg line 304
  28. lemma OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.cofaces_eq_sum line 308
  29. lemma OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.subsets_level line 312
  30. lemma OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.sum_cofaces line 320
  31. lemma OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.weight_sum line 332
  32. def OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.Invariant line 343
  33. lemma OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.invariant_iff line 347
  34. lemma OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.level_smul_iff line 355
  35. lemma OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.cofaces_smul line 360
  36. lemma OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.weight_smul line 377
  37. lemma OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.norm_pull line 382
  38. def OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.faceAction line 393
  39. instance OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.faceFintype line 404
  40. lemma OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.card_faces line 407
  41. lemma OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.count_incident line 415
  42. lemma OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.occupancy line 430
  43. theorem OAI.CoboundaryExpanders.InfiniteChains.FiniteWeights.weighted_correction line 470