OAI/Combinatorics/Progressions/Probability/RestrictedComplexChartDensityComparison.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.realDensityMeasure_indicator line 13
  2. theorem OAI.Erdos3.realDensityMeasure_eq_indicator_of_ae line 25
  3. theorem OAI.Erdos3.mappedDensity_restrict_to_source_support line 31
  4. def OAI.Erdos3.restrictedChartDensity line 53
  5. theorem OAI.Erdos3.restrictedChartDensity_apply line 58
  6. theorem OAI.Erdos3.restrictedChartDensity_zero line 64
  7. theorem OAI.Erdos3.subtype_density_map line 70
  8. theorem OAI.Erdos3.restrictedChartDensity_law line 88
  9. theorem OAI.Erdos3.continuousDensity_zero_off_closed line 123
  10. theorem OAI.Erdos3.continuousDensity_zero_off_mapped_compact line 139
  11. theorem OAI.Erdos3.continuousDensity_open_chart line 163
  12. theorem OAI.Erdos3.realDensityMeasure_lintegral_of_map line 205
  13. theorem OAI.Erdos3.restrictedChartDensity_indicator line 215
  14. theorem OAI.Erdos3.restrictedChartDensity_measurable line 222
  15. theorem OAI.Erdos3.restrictedChartDensity_lintegral line 228
  16. def OAI.Erdos3.restrictedComplexChartDensity line 263
  17. theorem OAI.Erdos3.restrictedComplexChartDensity_apply line 267
  18. theorem OAI.Erdos3.restrictedComplexChartDensity_zero line 273
  19. theorem OAI.Erdos3.restrictedComplexChartDensity_real line 281
  20. theorem OAI.Erdos3.restrictedComplexChartDensity_sum line 292
  21. theorem OAI.Erdos3.restrictedComplexChartDensity_norm_sub line 306
  22. theorem OAI.Erdos3.restrictedComplexChartDensity_pointwise_error line 319
  23. theorem OAI.Erdos3.restrictedComplexChartDensity_re_mul_bounds line 342
  24. theorem OAI.Erdos3.restrictedComplexChartDensity_scaled_re_mul_bounds line 365