OAI/Combinatorics/Progressions/Linear/TruncatedProjectionError.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_sum line 11
  2. theorem OAI.Erdos3.FiniteProbabilityWeights.norm_weighted_complexMean_sub_le_mean_norm line 17
  3. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_weighted_expansion line 28
  4. theorem OAI.Erdos3.FiniteProbabilityWeights.weighted_expansion_discard_error line 41
  5. theorem OAI.Erdos3.FiniteProbabilityWeights.weighted_projection_tested_error line 70
  6. def OAI.Erdos3.projectionApproxTolerance line 104
  7. def OAI.Erdos3.projectionModeTolerance line 106
  8. theorem OAI.Erdos3.projectionErrorBudget_spec line 108
  9. theorem OAI.Erdos3.FiniteProbabilityWeights.weighted_projection_comparison line 133
  10. def OAI.Erdos3.finiteAverageMap line 164
  11. theorem OAI.Erdos3.finiteAverageMap_sub_norm_le line 168
  12. theorem OAI.Erdos3.finiteAverageMap_ofReal line 174
  13. theorem OAI.Erdos3.finiteAverageMap_real_unit_interval line 179
  14. theorem OAI.Erdos3.finiteAverageMap_expansion line 189
  15. theorem OAI.Erdos3.finiteAverageMap_tested_error line 207
  16. theorem OAI.Erdos3.uniform_complexMean_addChar line 236
  17. def OAI.Erdos3.finiteCosetAverage line 244
  18. theorem OAI.Erdos3.finiteCosetAverage_invariant line 248
  19. theorem OAI.Erdos3.finiteCosetAverage_idempotent line 258
  20. theorem OAI.Erdos3.finiteCosetAverage_character line 266
  21. theorem OAI.Erdos3.finiteCosetAverage_expansion line 276
  22. theorem OAI.Erdos3.finiteCosetAverage_tested_error line 289
  23. def OAI.Erdos3.finiteKernelAverage line 317
  24. theorem OAI.Erdos3.finiteKernelAverage_eq_of_map_eq line 320
  25. theorem OAI.Erdos3.finiteKernelAverage_factors line 333
  26. theorem OAI.Erdos3.character_trivial_on_kernel_iff line 342
  27. theorem OAI.Erdos3.finiteKernelAverage_character line 352
  28. theorem OAI.Erdos3.FiniteProbabilityWeights.weighted_projection_truncation_error line 367
  29. theorem OAI.Erdos3.finiteCosetAverage_truncation_tested_error line 385