OAI/Combinatorics/Progressions/Estimates/NativeDilationObservable.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.signedTensorProduct line 14
  2. theorem OAI.Erdos3.signedTensorProduct_norm line 17
  3. theorem OAI.Erdos3.signedTensorProduct_norm_le line 22
  4. theorem OAI.Erdos3.signedTensorProduct_phase line 27
  5. theorem OAI.Erdos3.signed_power_phase_cancellation line 47
  6. theorem OAI.Erdos3.signedTensorProduct_lipschitz line 57
  7. def OAI.Erdos3.integerDilationVector line 81
  8. def OAI.Erdos3.signedTensorVector line 84
  9. def OAI.Erdos3.dilationTensorCrossProduct line 88
  10. theorem OAI.Erdos3.NilpotentLieFiltration.realDilationPair_top_group_relation line 107
  11. theorem OAI.Erdos3.MultidegreeLieFiltration.realDilationPairProjection_mem line 131
  12. theorem OAI.Erdos3.MultidegreeLieFiltration.realDilationPair_top_group_relation line 142
  13. theorem OAI.Erdos3.NativeIntegerVectorEquivalence.of_dilation_family line 169
  14. def OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.dilationObservable line 204
  15. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.dilationObservable_mk line 209
  16. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.dilationObservable_norm_le line 216
  17. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.dilationSpaceProjection_top_smul line 225
  18. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.dilationObservable_component_top line 235
  19. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.dilationObservable_top_invariant line 248