OAI/Combinatorics/Progressions/Estimates/NativeCrossFactorization.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.fourPointProduct line 13
  2. theorem OAI.Erdos3.fourPointProduct_mul line 16
  3. structure OAI.Erdos3.NativeVectorCorrelation line 33
  4. def OAI.Erdos3.NativeVectorCorrelation.mono line 56
  5. theorem OAI.Erdos3.NativeVectorCorrelation.exists_of_mean line 63
  6. theorem OAI.Erdos3.NativeVectorCorrelation.exists_reindex line 80
  7. theorem OAI.Erdos3.NativeVectorCorrelation.exists_of_mean_approx line 104
  8. theorem OAI.Erdos3.NativeVectorCorrelation.exists_of_uniform_approx line 135
  9. def OAI.Erdos3.nativeCrossResidual line 156
  10. abbrev OAI.Erdos3.NativeCrossWitnesses line 160
  11. def OAI.Erdos3.NativeCrossWitnesses.product line 174
  12. def OAI.Erdos3.NativeCrossWitnesses.extension line 177
  13. theorem OAI.Erdos3.NativeCrossWitnesses.extension_of_mem line 180
  14. theorem OAI.Erdos3.NativeCrossWitnesses.extension_of_not_mem line 184
  15. theorem OAI.Erdos3.NativeCrossWitnesses.product_norm line 188
  16. theorem OAI.Erdos3.NativeCrossWitnesses.extension_norm line 195
  17. theorem OAI.Erdos3.NativeCrossWitnesses.product_correlation line 203
  18. def OAI.Erdos3.NativeCrossWitnesses.mono line 209
  19. theorem OAI.Erdos3.NativeCrossWitnesses.mono_extension line 212
  20. theorem OAI.Erdos3.exists_native_two_unit_comparison line 230
  21. theorem OAI.Erdos3.le_productNiltestBudget line 294
  22. theorem OAI.Erdos3.NativeVectorCorrelation.exists_absorb line 304
  23. theorem OAI.Erdos3.positive_le_vector_norm_iff line 368
  24. theorem OAI.Erdos3.NativeVectorCorrelation.norm_correlation line 385
  25. theorem OAI.Erdos3.NativeVectorCorrelation.exists_of_norm line 391
  26. def OAI.Erdos3.NativeCrossWitnesses.lower line 430
  27. theorem OAI.Erdos3.NativeCrossWitnesses.extension_quadruple_factored line 432
  28. theorem OAI.Erdos3.NativeCrossWitnesses.extension_quadruple_of_product line 448