OAI/Combinatorics/Progressions/Estimates/PhysicalActiveIdealSite.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.activeAveragedIdealSiteFunction line 18
  2. theorem OAI.Erdos3.activeAveragedIdealSiteFunction_bound line 23
  3. theorem OAI.Erdos3.activeAveragedIdealSiteFunction_lipschitz line 33
  4. theorem OAI.Erdos3.exists_active_ideal_site_approximation line 56
  5. def OAI.Erdos3.physicalActiveProfileIdeal line 114
  6. theorem OAI.Erdos3.physicalActiveProfileIdeal_eq line 118
  7. theorem OAI.Erdos3.physicalActiveProfileIdeal_measurable line 126
  8. theorem OAI.Erdos3.physicalActiveProfileIdeal_probability line 131
  9. theorem OAI.Erdos3.physicalActiveProfileIdeal_test_integral line 141
  10. theorem OAI.Erdos3.exists_buffered_active_ideal_site_approximation line 157
  11. theorem OAI.Erdos3.physicalActiveProfileIdeal_bound line 206
  12. theorem OAI.Erdos3.physicalActiveProfileIdeal_lipschitz line 216
  13. theorem OAI.Erdos3.physicalActiveProfileIdeal_zero_outside line 234
  14. theorem OAI.Erdos3.booleanSiteJets_axis_mul line 267
  15. theorem OAI.Erdos3.physicalActiveProfileIdeal_normalized_sites line 275
  16. theorem OAI.Erdos3.exists_masked_active_ideal_site_approximation line 306
  17. theorem OAI.Erdos3.inverseProduct_norm_le_exp line 357
  18. theorem OAI.Erdos3.diagonalProfileLip_le_exp line 368
  19. theorem OAI.Erdos3.partitionedIdealRadius_add_one_le_exp line 391
  20. theorem OAI.Erdos3.exists_masked_physical_active_ideal_site_approximation line 429