OAI/Combinatorics/Progressions/Estimates/FiniteFiberTest.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.finiteMask line 15
  2. theorem OAI.Erdos3.finiteMask_apply line 21
  3. theorem OAI.Erdos3.FiniteProbabilityWeights.mean_add line 29
  4. theorem OAI.Erdos3.FiniteProbabilityWeights.mean_const_mul line 34
  5. def OAI.Erdos3.FiniteProbabilityWeights.mass line 41
  6. theorem OAI.Erdos3.FiniteProbabilityWeights.mass_nonneg line 44
  7. theorem OAI.Erdos3.FiniteProbabilityWeights.mass_le_one line 48
  8. theorem OAI.Erdos3.FiniteProbabilityWeights.weight_le_mass line 54
  9. theorem OAI.Erdos3.FiniteProbabilityWeights.mean_indicator line 57
  10. def OAI.Erdos3.FiniteProbabilityWeights.condition line 60
  11. theorem OAI.Erdos3.FiniteProbabilityWeights.condition_mean line 69
  12. theorem OAI.Erdos3.FiniteProbabilityWeights.mass_mul_condition_mean line 78
  13. theorem OAI.Erdos3.FiniteProbabilityWeights.mass_mul_condition_correlation line 83
  14. theorem OAI.Erdos3.FiniteProbabilityWeights.norm_correlation_mask line 97
  15. theorem OAI.Erdos3.FiniteProbabilityWeights.mean_mask_zero line 103
  16. theorem OAI.Erdos3.exists_productive_good_path line 125
  17. theorem OAI.Erdos3.exists_productive_model_transfer line 149
  18. theorem OAI.Erdos3.model_transfer_eighths line 171
  19. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_congr_support line 191
  20. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_sub line 199
  21. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_ofReal line 203
  22. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_ofReal_mul line 207
  23. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_finset_expect line 212
  24. theorem OAI.Erdos3.FiniteProbabilityWeights.norm_complexMean_le_mean_norm line 218
  25. theorem OAI.Erdos3.FiniteProbabilityWeights.norm_complexMean_sub_le line 225
  26. theorem OAI.Erdos3.exists_external_test_bins line 245
  27. theorem OAI.Erdos3.norm_complex_profile_sum_sub line 306
  28. theorem OAI.Erdos3.norm_nested_complex_profile_reference_sub line 315
  29. theorem OAI.Erdos3.finiteComplexMean_sum line 330
  30. theorem OAI.Erdos3.finiteComplexMean_const_mul line 337
  31. def OAI.Erdos3.FiniteProbabilityWeights.fiberMean line 358
  32. theorem OAI.Erdos3.FiniteProbabilityWeights.fiberMean_nonneg line 362
  33. theorem OAI.Erdos3.FiniteProbabilityWeights.sum_fiberMean line 371
  34. def OAI.Erdos3.FiniteProbabilityWeights.fiberLaw line 381
  35. theorem OAI.Erdos3.FiniteProbabilityWeights.fiberLaw_weight line 386
  36. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_fiber_factor line 389
  37. theorem OAI.Erdos3.FiniteProbabilityWeights.fiberMean_eq_mass_mul_condition line 402
  38. theorem OAI.Erdos3.FiniteProbabilityWeights.mean_measurable line 426
  39. theorem OAI.Erdos3.FiniteProbabilityWeights.mean_integrable line 430
  40. theorem OAI.Erdos3.FiniteProbabilityWeights.integral_mean line 435
  41. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_measurable line 442
  42. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_integrable line 446
  43. theorem OAI.Erdos3.FiniteProbabilityWeights.integral_complexMean line 451
  44. def OAI.Erdos3.FiniteProbabilityWeights.pointWeights line 467
  45. theorem OAI.Erdos3.FiniteProbabilityWeights.pointWeights_complexMean line 477
  46. def OAI.Erdos3.FiniteProbabilityWeights.positiveRestriction line 500
  47. theorem OAI.Erdos3.FiniteProbabilityWeights.positiveRestriction_mean line 511
  48. theorem OAI.Erdos3.FiniteProbabilityWeights.positiveRestriction_complexMean line 520
  49. def OAI.Erdos3.FiniteProbabilityWeights.fiberTest line 539
  50. theorem OAI.Erdos3.FiniteProbabilityWeights.fiberMean_le_mul_mass line 542
  51. theorem OAI.Erdos3.FiniteProbabilityWeights.fiberMean_zero_of_mass_zero line 553
  52. theorem OAI.Erdos3.FiniteProbabilityWeights.fiberTest_bounds line 561
  53. theorem OAI.Erdos3.FiniteProbabilityWeights.mass_mul_fiberTest line 572