OAI/Combinatorics/Progressions/Estimates/NativeResidualMultiplier.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Erdos3.NativeIntegerVectorEquivalence.ExpansionIndex line 17
  2. theorem OAI.Erdos3.NativeIntegerVectorEquivalence.expansionIndex_card_bound line 19
  3. def OAI.Erdos3.correlationInput line 44
  4. def OAI.Erdos3.mixedCorrelationDegree line 46
  5. def OAI.Erdos3.nativeCorrelationResidual line 48
  6. structure OAI.Erdos3.NativeCorrelationStructure line 55
  7. def OAI.Erdos3.NativeCorrelationStructure.mono line 69
  8. def OAI.Erdos3.NativeCorrelationStructure.selectedWitness line 99
  9. def OAI.Erdos3.NativeCorrelationStructure.selectedProduct line 103
  10. theorem OAI.Erdos3.NativeCorrelationStructure.selectedProduct_norm line 108
  11. theorem OAI.Erdos3.NativeCorrelationStructure.selectedProduct_correlation line 124
  12. def OAI.Erdos3.nativeMixedResidual line 137
  13. structure OAI.Erdos3.NativeMixedCorrelation line 142
  14. def OAI.Erdos3.NativeMixedCorrelation.mono line 155
  15. def OAI.Erdos3.NativeCorrelationStructure.boundedSelectedProduct line 180
  16. theorem OAI.Erdos3.NativeCorrelationStructure.boundedSelectedProduct_norm line 183
  17. theorem OAI.Erdos3.NativeCorrelationStructure.boundedSelectedProduct_mean line 192
  18. theorem OAI.Erdos3.NativeCorrelationStructure.boundedSelectedProduct_correlation line 201
  19. def OAI.Erdos3.NativeCorrelationStructure.boundedCorrelator line 213
  20. theorem OAI.Erdos3.NativeCorrelationStructure.boundedCorrelator_of_mem line 216
  21. theorem OAI.Erdos3.NativeCorrelationStructure.boundedCorrelator_of_not_mem line 220
  22. theorem OAI.Erdos3.NativeCorrelationStructure.boundedCorrelator_norm line 224
  23. theorem OAI.Erdos3.NativeCorrelationStructure.boundedCorrelator_correlation line 231
  24. def OAI.Erdos3.NativeCorrelationStructure.normalizedLower line 250
  25. theorem OAI.Erdos3.NativeCorrelationStructure.normalizedLower_of_mem line 255
  26. theorem OAI.Erdos3.NativeCorrelationStructure.normalizedLower_norm line 260
  27. def OAI.Erdos3.RationalFilteredNilmanifold.Niltest.normalizedRow line 287
  28. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.normalizedRow_norm line 292
  29. theorem OAI.Erdos3.NativeIntegerVectorEquivalence.exists_fixed_normalized_row line 310
  30. def OAI.Erdos3.NativeMultidegreeNilcharacter.HasMixedCorrelation line 388
  31. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.HasMixedCorrelation.mono line 392
  32. theorem OAI.Erdos3.NativeMixedCorrelation.hasMixedCorrelation line 400
  33. def OAI.Erdos3.NativeMixedCorrelation.residualWitness line 425
  34. def OAI.Erdos3.NativeMixedCorrelation.normalizedResidualRow line 429
  35. theorem OAI.Erdos3.NativeMixedCorrelation.normalizedResidualRow_norm line 435
  36. theorem OAI.Erdos3.NativeMixedCorrelation.normalizedResidualRow_correlation line 447
  37. theorem OAI.Erdos3.NativeMixedCorrelation.exists_fixed_normalized_residual_coordinate line 474
  38. def OAI.Erdos3.NativeMixedCorrelation.residualMultiplier line 521
  39. theorem OAI.Erdos3.NativeMixedCorrelation.residualMultiplier_norm line 524
  40. theorem OAI.Erdos3.NativeMixedCorrelation.normalizedResidualRow_factor line 534
  41. theorem OAI.Erdos3.NativeMixedCorrelation.residualMultiplier_expansion line 543