OAI/Geometry/NilpotentCharts/FilteredBasis.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Filtered lattice bases and rational charts for simply connected nilpotent Lie groups.

  1. lemma OAI.RawLieIntegration.centralSubspace_smul line 22
  2. lemma OAI.RawLieIntegration.centralSubspace_add line 27
  3. lemma OAI.RawLieIntegration.centralSubspace_sum line 32
  4. lemma OAI.RawLieIntegration.centralSubspace_basis line 38
  5. lemma OAI.RawLieIntegration.centralSubspace_eq_exp line 49
  6. def OAI.RawLieIntegration.centralSubspaceHomeomorph line 55
  7. lemma OAI.RawLieIntegration.centralSubspaceHomeomorph_apply line 60
  8. lemma OAI.RawLieIntegration.centralSubspace_lattice_discrete line 63
  9. lemma OAI.RawLieIntegration.centralSubspace_lattice_cocompact line 76
  10. lemma OAI.RawLieIntegration.exists_subspace_lattice_basis line 105
  11. lemma OAI.RawLieIntegration.subspace_tangent_projection_kernel line 130
  12. def OAI.RawLieIntegration.HasFilteredLatticeBasis line 166
  13. theorem OAI.RawLieIntegration.filteredBasis_of_subspace_quotient line 177
  14. theorem OAI.RawLieIntegration.filteredBasis_class_induction line 341
  15. theorem OAI.RawLieIntegration.filteredBasis_of_nilpotent line 416
  16. theorem OAI.RawLieIntegration.rawChart_of_nilpotent line 430
  17. theorem OAI.SourceRawChartGap.rawChartExists line 493
  18. theorem OAI.raw_chart_reference line 499