OAI/Geometry/NilpotentCharts/Filtrations.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Closed lower-central filtrations and monotone positive coordinate weights.

  1. lemma OAI.StretchedFiltration.rotate_le line 16
  2. theorem OAI.StretchedFiltration.lower_bracket line 33
  3. def OAI.StretchedFiltration.stretch line 58
  4. lemma OAI.StretchedFiltration.stretch_antitone line 61
  5. lemma OAI.StretchedFiltration.stretch_zero line 65
  6. lemma OAI.StretchedFiltration.stretch_one line 68
  7. lemma OAI.StretchedFiltration.stretch_eq_top line 71
  8. lemma OAI.StretchedFiltration.stretch_terminal line 76
  9. lemma OAI.StretchedFiltration.stretch_bracket line 81
  10. lemma OAI.RawClosedFiltration.closure_commutator_le line 110
  11. def OAI.RawClosedFiltration.level line 128
  12. lemma OAI.RawClosedFiltration.antitone_level line 129
  13. lemma OAI.RawClosedFiltration.bracket_level line 132
  14. lemma OAI.RawClosedFiltration.level_zero line 136
  15. lemma OAI.RawClosedFiltration.level_one line 140
  16. lemma OAI.RawClosedFiltration.level_terminal line 144
  17. lemma OAI.RawClosedFiltration.comap_closure_map line 153
  18. lemma OAI.RawClosedFiltration.comap_level line 171
  19. lemma OAI.RawFilteredWeights.append_monotone line 180
  20. lemma OAI.RawFilteredWeights.append_pos line 200
  21. lemma OAI.RawFilteredWeights.append_bound line 206
  22. lemma OAI.RawFilteredWeights.append_zero_iff line 212