OAI/Combinatorics/Progressions/Estimates/StrongRefiltrationReconstruction.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.NilpotentLieFiltration.symbolPointwiseSubalgebra_mono line 21
  2. theorem OAI.Erdos3.NilpotentLieFiltration.symbolPointwiseSubalgebra_map_le line 26
  3. theorem OAI.Erdos3.NilpotentLieFiltration.symbolPointwiseSubalgebra_comap line 39
  4. theorem OAI.Erdos3.NilpotentLieFiltration.symbolPointwiseSubalgebra_map line 61
  5. theorem OAI.Erdos3.NilpotentLieFiltration.associatedGradedMap_image_graded line 82
  6. theorem OAI.Erdos3.NilpotentLieFiltration.associatedGradedMap_comap_graded line 90
  7. theorem OAI.Erdos3.RationalFilteredNilmanifold.quotient_markedDiagram_injective line 113
  8. theorem OAI.Erdos3.RationalFilteredNilmanifold.refiltered_markedDiagram_injective line 129
  9. theorem OAI.Erdos3.NilpotentLieFiltration.real_symbolPointwiseSubalgebra_map_mem line 169
  10. theorem OAI.Erdos3.NilpotentLieFiltration.homogeneousGradedProjection_image_eq line 204
  11. theorem OAI.Erdos3.NilpotentLieFiltration.projected_realSymbolRepresentative_mem_homogeneous_image line 216
  12. theorem OAI.Erdos3.NilpotentLieFiltration.projected_realSymbolRepresentative_coefficients_mem_homogeneous_image line 232
  13. theorem OAI.Erdos3.NilpotentLieFiltration.gradedRefiltrationLayer_map line 269
  14. theorem OAI.Erdos3.NilpotentLieFiltration.gradedRefiltrationLayer_top_kernel_eq_zero line 314
  15. theorem OAI.Erdos3.NilpotentLieFiltration.gradedRefiltrationLayer_map_mem line 330
  16. def OAI.Erdos3.NilpotentLieFiltration.gradedRefiltrationMap line 338
  17. theorem OAI.Erdos3.NilpotentLieFiltration.gradedRefiltrationMap_apply line 347
  18. theorem OAI.Erdos3.NilpotentLieFiltration.gradedRefiltrationMap_mem_layer line 351
  19. theorem OAI.Erdos3.NilpotentLieFiltration.gradedRefiltrationMap_layer_surjective line 360
  20. theorem OAI.Erdos3.RationalFilteredNilmanifold.allocatedMarkedDiagram_injective_of_top_kernel line 403
  21. theorem OAI.Erdos3.RationalFilteredNilmanifold.allocatedMarkedDiagram_injective_of_graded_top line 418
  22. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionNativePivotQuotientMap_mem_layer line 458
  23. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionNativePivotQuotientMap_layer_surjective line 475
  24. def OAI.Erdos3.RationalFilteredNilmanifold.optionNativeCommonPivotQuotientFast line 502
  25. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionNativeCommonPivotQuotientFast_layer_eq line 524
  26. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionNativeCommonPivotQuotientFast_graded line 540
  27. abbrev OAI.Erdos3.NilpotentLieFiltration.refilteredProjectionFiberProduct line 566
  28. def OAI.Erdos3.NilpotentLieFiltration.refilteredProjectionFiberEquiv line 582
  29. theorem OAI.Erdos3.NilpotentLieFiltration.refilteredProjectionFiberEquiv_apply line 593
  30. theorem OAI.Erdos3.NilpotentLieFiltration.refilteredProjectionFiberEquiv_symm_components line 599
  31. theorem OAI.Erdos3.NilpotentLieFiltration.refilteredProjectionFiberEquiv_layer_surjective line 609
  32. theorem OAI.Erdos3.NilpotentLieFiltration.refilteredProjectionFiberEquiv_mem_layer_iff line 626