OAI/Combinatorics/Progressions/Estimates/ScaledConditionedComparison.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.productANOVA_sum line 17
  2. theorem OAI.Erdos3.productANOVATruncation_sum line 23
  3. theorem OAI.Erdos3.productANOVATruncation_smul line 30
  4. theorem OAI.Erdos3.productCouplingPairing_smul line 38
  5. theorem OAI.Erdos3.productCouplingPairing_truncation_smul line 46
  6. theorem OAI.Erdos3.normalized_pairing_error_scale line 65
  7. def OAI.Erdos3.productAtomTruncatedPairing line 81
  8. theorem OAI.Erdos3.productAtomTruncatedPairing_smul line 86
  9. theorem OAI.Erdos3.productANOVA_add line 110
  10. theorem OAI.Erdos3.productANOVATruncation_add line 116
  11. def OAI.Erdos3.productTruncatedPairing line 125
  12. theorem OAI.Erdos3.productTruncatedPairing_add_left line 129
  13. theorem OAI.Erdos3.productTruncatedPairing_add_right line 136
  14. theorem OAI.Erdos3.productTruncatedPairing_smul line 143
  15. theorem OAI.Erdos3.productTruncatedPairing_sub_smul_right line 148
  16. theorem OAI.Erdos3.productTruncatedPairing_sum_right line 158
  17. theorem OAI.Erdos3.productAtomTruncatedPairing_sub_smul_right line 165
  18. theorem OAI.Erdos3.productTruncatedPairing_atom_sum_right line 192
  19. theorem OAI.Erdos3.ProductCylinder.indicator_density_cut line 207
  20. theorem OAI.Erdos3.ProductCylinder.truncated_pairing_atoms line 221
  21. theorem OAI.Erdos3.observedProductDensity_residual_difference line 242
  22. theorem OAI.Erdos3.CylinderRemovalChain.retained_pairing_sum_le line 282
  23. theorem OAI.Erdos3.productCouplingPairing_embedding line 327
  24. theorem OAI.Erdos3.productTruncatedPairing_embedding line 333
  25. theorem OAI.Erdos3.CylinderRemovalChain.truncated_pairing_decomposition line 365
  26. theorem OAI.Erdos3.CylinderRemovalChain.total_pairing_le line 403
  27. theorem OAI.Erdos3.CylinderRemovalChain.total_pairing_with_shell_budget line 448
  28. theorem OAI.Erdos3.weighted_pairing_error_compose line 496
  29. theorem OAI.Erdos3.productKernel_conditioned_mean_comparison line 504
  30. theorem OAI.Erdos3.productKernel_scaled_conditioned_mean_comparison line 555