OAI/Combinatorics/Progressions/Estimates/NativeModelOrbit.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.RationalFilteredNilmanifold.rationalModelEquiv line 16
  2. theorem OAI.Erdos3.RationalFilteredNilmanifold.rationalModelEquiv_repr line 33
  3. theorem OAI.Erdos3.RationalFilteredNilmanifold.rationalModelEquiv_basis line 37
  4. theorem OAI.Erdos3.RationalFilteredNilmanifold.rationalModelEquiv_paddedLayerVector line 43
  5. theorem OAI.Erdos3.RationalFilteredNilmanifold.rationalModelEquiv_layer_succ line 50
  6. theorem OAI.Erdos3.RationalFilteredNilmanifold.rationalModelEquiv_layer line 59
  7. def OAI.Erdos3.RationalFilteredNilmanifold.rationalModelGroupEquiv line 93
  8. theorem OAI.Erdos3.RationalFilteredNilmanifold.rationalModelGroupEquiv_coordinates line 103
  9. theorem OAI.Erdos3.RationalFilteredNilmanifold.rationalModelGroupEquiv_mem_layer line 108
  10. theorem OAI.Erdos3.RationalFilteredNilmanifold.rationalModelGroupEquiv_mem_integral_lattice line 120
  11. theorem OAI.Erdos3.RationalFilteredNilmanifold.rationalModelGroupEquiv_map_integral_lattice line 129
  12. structure OAI.Erdos3.RationalFilteredNilmanifold.NativeModelEquiv line 156
  13. def OAI.Erdos3.RationalFilteredNilmanifold.NativeModelEquiv.symm line 167
  14. def OAI.Erdos3.RationalFilteredNilmanifold.nativeModelEquivOfCoordinates line 188
  15. theorem OAI.Erdos3.realificationLieEquiv_inverse line 203
  16. def OAI.Erdos3.RationalFilteredNilmanifold.NativeModelEquiv.realGroupEquiv line 228
  17. theorem OAI.Erdos3.RationalFilteredNilmanifold.NativeModelEquiv.symm_realGroupEquiv_apply line 240
  18. theorem OAI.Erdos3.RationalFilteredNilmanifold.NativeModelEquiv.map_real_layer line 244
  19. theorem OAI.Erdos3.RationalFilteredNilmanifold.NativeModelEquiv.real_lattice_le line 250
  20. def OAI.Erdos3.RationalFilteredNilmanifold.NativeModelEquiv.spaceMap line 255
  21. theorem OAI.Erdos3.RationalFilteredNilmanifold.NativeModelEquiv.spaceMap_mk line 258
  22. theorem OAI.Erdos3.RationalFilteredNilmanifold.NativeModelEquiv.spaceMap_smul line 261
  23. theorem OAI.Erdos3.RationalFilteredNilmanifold.NativeModelEquiv.symm_spaceMap_apply line 265
  24. theorem OAI.Erdos3.RationalFilteredNilmanifold.NativeModelEquiv.spaceMap_lipschitz line 275
  25. def OAI.Erdos3.RationalFilteredNilmanifold.NativeModelEquiv.mapOrbit line 307
  26. theorem OAI.Erdos3.RationalFilteredNilmanifold.NativeModelEquiv.mapOrbit_log line 316
  27. theorem OAI.Erdos3.RationalFilteredNilmanifold.NativeModelEquiv.mapOrbit_eval line 320
  28. theorem OAI.Erdos3.RationalFilteredNilmanifold.NativeModelEquiv.mapOrbit_realEval line 327