OAI/Combinatorics/Progressions/Probability/FiniteProbabilityLipschitz.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Erdos3.FiniteProbabilityWeights line 15
  2. def OAI.Erdos3.FiniteProbabilityWeights.mean line 24
  3. def OAI.Erdos3.FiniteProbabilityWeights.correlation line 26
  4. theorem OAI.Erdos3.FiniteProbabilityWeights.mean_nonneg line 29
  5. theorem OAI.Erdos3.FiniteProbabilityWeights.mean_mono line 32
  6. theorem OAI.Erdos3.FiniteProbabilityWeights.mean_const line 35
  7. theorem OAI.Erdos3.FiniteProbabilityWeights.mean_mul_sq_le line 38
  8. theorem OAI.Erdos3.FiniteProbabilityWeights.mean_square_le line 47
  9. theorem OAI.Erdos3.FiniteProbabilityWeights.norm_correlation_sq_le line 51
  10. theorem OAI.Erdos3.FiniteProbabilityWeights.correlation_self line 63
  11. theorem OAI.Erdos3.FiniteProbabilityWeights.norm_correlation_symm line 75
  12. theorem OAI.Erdos3.FiniteProbabilityWeights.mean_single_norm line 85
  13. def OAI.Erdos3.centeredFiniteWeightDensity line 111
  14. theorem OAI.Erdos3.centeredFiniteWeightDensity_measurable line 114
  15. theorem OAI.Erdos3.centeredFiniteWeightDensity_nonneg line 120
  16. theorem OAI.Erdos3.centeredFiniteWeightDensity_le_one line 124
  17. theorem OAI.Erdos3.centeredFiniteWeightDensity_integrable line 130
  18. theorem OAI.Erdos3.centeredFiniteWeightDensity_integral line 140
  19. theorem OAI.Erdos3.finiteProbability_tensor_comparison line 159
  20. theorem OAI.Erdos3.finiteSource_density_error_measurable line 218
  21. theorem OAI.Erdos3.finiteSource_density_l1_of_uniform_bound line 230
  22. theorem OAI.Erdos3.FiniteProbabilityWeights.mean_lipschitz_uniform line 268
  23. theorem OAI.Erdos3.FiniteProbabilityWeights.mean_lipschitz_uniform_emetric line 282