OAI/Combinatorics/Progressions/Probability/ObservedProductDensity.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.FiniteProbabilityWeights.mean_mono_on_support line 13
  2. theorem OAI.Erdos3.FiniteProbabilityWeights.abs_mean_le_mean_abs line 21
  3. theorem OAI.Erdos3.FiniteProbabilityWeights.abs_mean_le_on_support line 30
  4. theorem OAI.Erdos3.FiniteProbabilityWeights.density_cauchy_schwarz line 35
  5. theorem OAI.Erdos3.FiniteProbabilityWeights.density_square_le line 44
  6. def OAI.Erdos3.ProductDependsOn line 63
  7. theorem OAI.Erdos3.ProductDependsOn.mono line 67
  8. theorem OAI.Erdos3.ProductDependsOn.mul line 71
  9. def OAI.Erdos3.productConditionalMean line 83
  10. theorem OAI.Erdos3.productConditionalMean_univ line 87
  11. theorem OAI.Erdos3.productConditionalMean_empty line 92
  12. theorem OAI.Erdos3.productConditionalMean_const line 96
  13. theorem OAI.Erdos3.productConditionalMean_add line 100
  14. theorem OAI.Erdos3.productConditionalMean_sub line 106
  15. theorem OAI.Erdos3.productConditionalMean_smul line 112
  16. theorem OAI.Erdos3.productConditionalMean_sum line 117
  17. theorem OAI.Erdos3.productConditionalMean_depends line 123
  18. theorem OAI.Erdos3.productConditionalMean_of_depends line 135
  19. theorem OAI.Erdos3.productConditionalMean_comp line 143
  20. theorem OAI.Erdos3.productConditionalMean_selfadjoint line 150
  21. def OAI.Erdos3.finiteWeightDensity line 172
  22. theorem OAI.Erdos3.finiteWeightDensity_nonneg line 175
  23. theorem OAI.Erdos3.finiteWeightDensity_mul line 179
  24. theorem OAI.Erdos3.mean_finiteWeightDensity line 187
  25. theorem OAI.Erdos3.FiniteProbabilityWeights.weighted_proxy_abs_mass_le line 205
  26. theorem OAI.Erdos3.density_sum_spatial_error line 245
  27. theorem OAI.Erdos3.finiteMean_spatial_error_of_mass line 265
  28. def OAI.Erdos3.productFiberIndicator line 289
  29. theorem OAI.Erdos3.productFiberIndicator_depends line 293
  30. theorem OAI.Erdos3.productFiberIndicator_self line 301
  31. def OAI.Erdos3.productFiberMass line 307
  32. theorem OAI.Erdos3.productFiberMass_nonneg line 310
  33. theorem OAI.Erdos3.weight_le_productFiberMass line 318
  34. theorem OAI.Erdos3.productFiberMass_empty line 326
  35. theorem OAI.Erdos3.productFiberMass_pos line 330
  36. theorem OAI.Erdos3.partition_weighted_mass_le line 344
  37. theorem OAI.Erdos3.productConditionalMean_fiber_identity line 377
  38. theorem OAI.Erdos3.productConditionalMean_eq_marginal_density line 404
  39. theorem OAI.Erdos3.productConditionalMean_close_of_marginal line 415
  40. def OAI.Erdos3.observedProductDensity line 445
  41. theorem OAI.Erdos3.productFiberMass_fiberMean line 450
  42. theorem OAI.Erdos3.observedProductDensity_fiber_identity line 464
  43. theorem OAI.Erdos3.observedProductDensity_conditional line 482