OAI/Combinatorics/Progressions/Estimates/NativeDilationDescent.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.MultidegreeLieFiltration.realifiedAdditiveTripleOrbit line 21
  2. theorem OAI.Erdos3.MultidegreeLieFiltration.realifiedAdditiveTripleOrbit_eval line 32
  3. theorem OAI.Erdos3.MultidegreeLieFiltration.realifiedAdditiveTripleOrbit_zero line 45
  4. theorem OAI.Erdos3.MultidegreeLieFiltration.exists_real_normalized_addition_orbit line 56
  5. def OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.tripleObservable line 108
  6. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.tripleObservable_mk line 113
  7. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.tripleObservable_norm_le line 119
  8. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.tripleSpaceProjection_top_smul line 128
  9. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.tripleObservable_component_top line 138
  10. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.tripleObservable_top_invariant line 151
  11. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.exists_native_addition_orbit line 187
  12. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.tripleObservable_of_addition_values line 222
  13. theorem OAI.Erdos3.real_top_frequency_mul line 253
  14. theorem OAI.Erdos3.MultidegreeLieFiltration.realAdditiveTriple_frequency_phase line 263
  15. theorem OAI.Erdos3.MultidegreeLieFiltration.realAdditiveTriple_omitted_frequency_phase line 278
  16. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.unitVertical_top_action line 304
  17. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.unitVertical_triple_top_invariant line 315
  18. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.exists_lipschitz_unitVertical_triple_descent line 371
  19. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.exists_unitVertical_triple_quotient_niltest line 426
  20. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.unitVertical_dilation_top_invariant line 476
  21. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.exists_unitVertical_dilation_quotient_niltest line 534
  22. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.exists_dilation_niltest_of_data line 570