OAI/Combinatorics/Progressions/Estimates/NativeSharedFrozenCorrelations.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.RationalFilteredNilmanifold.lipschitz_native_frozenCosetMap line 23
  2. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_positive_frozen_observable line 45
  3. theorem OAI.Erdos3.RationalFilteredNilmanifold.native_frozenCosetMap_dist_le line 83
  4. def OAI.Erdos3.RationalFilteredNilmanifold.conjugationPullback line 131
  5. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_uniform_conjugated_source_cover line 140
  6. theorem OAI.Erdos3.RationalFilteredNilmanifold.real_conjugationPullback_property line 238
  7. theorem OAI.Erdos3.mapped_normal_conjugation_mem line 272
  8. theorem OAI.Erdos3.RationalFilteredNilmanifold.normalized_right_compatibility line 287
  9. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_uniform_frozen_coset_map line 322
  10. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_uniform_frozen_map line 416
  11. theorem OAI.Erdos3.RationalFilteredNilmanifold.realificationMap_id_apply line 508
  12. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_uniform_unit_frozen_cover line 519
  13. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_shared_frozen_unit_observable line 589
  14. theorem OAI.Erdos3.NativeCorrelationStructure.replacedRankResidual_norm_sub_le line 663
  15. theorem OAI.Erdos3.exists_native_shared_frozen_correlations line 679