OAI/Combinatorics/Progressions/Estimates/NativeCommonModelQuadruples.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Erdos3.NativeCyclicModel line 12
  2. def OAI.Erdos3.NativeCyclicModel.smul line 31
  3. def OAI.Erdos3.nativeCyclicFunctions line 44
  4. theorem OAI.Erdos3.nativeCyclicFunctions_balanced line 47
  5. theorem OAI.Erdos3.nativeCyclicFunctions_norm line 52
  6. theorem OAI.Erdos3.nativeCyclicFunctions_zero line 58
  7. def OAI.Erdos3.CyclicNativeInverse line 87
  8. structure OAI.Erdos3.NativeCommonDerivativeModels line 103
  9. theorem OAI.Erdos3.exists_native_cyclic_model_of_detector line 139
  10. def OAI.Erdos3.NativeModelDetector line 180
  11. def OAI.Erdos3.NativeTwoSiteModelingData line 185
  12. theorem OAI.Erdos3.exists_native_two_site_models line 221
  13. def OAI.Erdos3.NativeCommonDerivativeModels.mono line 284
  14. theorem OAI.Erdos3.exists_normalized_native_common_models line 294
  15. theorem OAI.Erdos3.cyclicNativeInverse_one line 350
  16. theorem OAI.Erdos3.mean_norm_le_fourier_sum line 384
  17. theorem OAI.Erdos3.exists_quadratic_small_modulus_correlation line 393
  18. theorem OAI.Erdos3.exists_shift_native_two_site_models line 441
  19. structure OAI.Erdos3.NativeVerticalDerivativeData line 479
  20. def OAI.Erdos3.NativeVerticalDerivativeData.mono line 492
  21. theorem OAI.Erdos3.NativeCommonDerivativeModels.exists_correlated_quadruples line 516