OAI/Combinatorics/Progressions/Estimates/ObservedUnitTruncation.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.productTruncatedGram_bound line 16
  2. theorem OAI.Erdos3.productSection_truncatedGram_bound line 97
  3. theorem OAI.Erdos3.productNormalizedSection_truncatedGram_bound line 117
  4. theorem OAI.Erdos3.observedProductDensity_truncatedGram_bound line 151
  5. theorem OAI.Erdos3.observedProductDensity_section_truncatedGram_bound line 164
  6. theorem OAI.Erdos3.observedProductDensity_small_mass_energy line 181
  7. theorem OAI.Erdos3.productSection_truncatedGram_uniform line 204
  8. theorem OAI.Erdos3.observedProductDensity_section_norm_uniform line 228
  9. theorem OAI.Erdos3.productCouplingPairing_truncation_sqrt_le line 259
  10. theorem OAI.Erdos3.productCouplingPairing_truncation_small_energy line 270
  11. theorem OAI.Erdos3.observedProductDensity_small_mass_pairing line 279
  12. theorem OAI.Erdos3.observedProductDensity_section_norm_le_three line 305
  13. theorem OAI.Erdos3.observedProductDensity_scaled_section_norm line 323
  14. theorem OAI.Erdos3.observed_unit_truncation_control line 351