OAI/Combinatorics/Progressions/Estimates/PhysicalPairAccuracyLogBounds.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.residualPointAccuracy_inverse_le_exp line 12
  2. theorem OAI.Erdos3.residualGridAccuracy_inverse_le_exp line 24
  3. theorem OAI.Erdos3.residualMeanAccuracy_inverse_le_exp line 30
  4. theorem OAI.Erdos3.partial_assignment_card_le_exp line 47
  5. theorem OAI.Erdos3.lowDegreeCoordinateSets_card_le_exp line 59
  6. theorem OAI.Erdos3.ProductCylinder.bounded_card_le_exp line 78
  7. theorem OAI.Erdos3.CylinderRemovalChain.length_le_exp line 98
  8. def OAI.Erdos3.scalarTransferBaseAccuracy line 125
  9. def OAI.Erdos3.scalarTransferMarginalAccuracy line 127
  10. def OAI.Erdos3.scalarTransferTail line 130
  11. theorem OAI.Erdos3.residueTruncationCap_le_exp line 132
  12. theorem OAI.Erdos3.scalarTransferAccuracy_spec line 149
  13. theorem OAI.Erdos3.scalarTransferMarginalAccuracy_cost line 161
  14. theorem OAI.Erdos3.scalarTransfer_combined_error_le line 169
  15. def OAI.Erdos3.residualCapEnvelope line 216
  16. theorem OAI.Erdos3.residualCapEnvelope_one_le line 219
  17. theorem OAI.Erdos3.residueTruncationCap_le_envelope line 224
  18. theorem OAI.Erdos3.residualCapEnvelope_le_exp line 232
  19. def OAI.Erdos3.physicalResidualPairBudget line 264
  20. theorem OAI.Erdos3.physicalResidualPairBudget_nonneg line 273
  21. theorem OAI.Erdos3.uniform_physical_residual_correlation line 282
  22. def OAI.Erdos3.physicalPairPointAccuracy line 332
  23. def OAI.Erdos3.physicalPairGridAccuracy line 337
  24. def OAI.Erdos3.physicalPairMeanAccuracy line 341
  25. theorem OAI.Erdos3.physicalPairPointAccuracy_spec line 346
  26. theorem OAI.Erdos3.physicalPairGridAccuracy_spec line 355
  27. theorem OAI.Erdos3.physicalPairMeanAccuracy_spec line 362
  28. theorem OAI.Erdos3.physicalResidualPairBudget_of_accuracies line 370
  29. theorem OAI.Erdos3.retained_physical_residual_correlation line 417
  30. def OAI.Erdos3.physicalPairCoefficientLog line 473
  31. theorem OAI.Erdos3.physicalPairCoefficientLog_bounds line 477
  32. theorem OAI.Erdos3.physicalPairPowerBounds line 496
  33. theorem OAI.Erdos3.physicalPairPointGridAccuracy_inverse_le_exp line 509
  34. def OAI.Erdos3.physicalPairMeanLog line 558
  35. theorem OAI.Erdos3.physicalPairMeanLog_bounds line 561
  36. theorem OAI.Erdos3.physicalPairMeanAccuracy_inverse_le_exp line 570