OAI/Combinatorics/Progressions/Probability/AllocatedJointMaskedDensityComparison.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.dominatedDensityRatio line 11
  2. theorem OAI.Erdos3.dominatedDensityRatio_mul line 14
  3. theorem OAI.Erdos3.dominatedDensityRatio_nonneg line 23
  4. theorem OAI.Erdos3.dominatedDensityRatio_norm_le line 28
  5. theorem OAI.Erdos3.dominatedDensityRatio_measurable line 37
  6. theorem OAI.Erdos3.dominatedDensityRatio_integral line 42
  7. theorem OAI.Erdos3.selectedResidueDensityPMF_maskedMean line 49
  8. theorem OAI.Erdos3.selectedResidueDensityPMF_maskedMean_error line 63
  9. theorem OAI.Erdos3.selectedResidueDensityPMF_event_error line 87
  10. theorem OAI.Erdos3.maskedDensity_integral_of_sample_law line 130
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedMaskedCoefficientDensity_continuous line 184
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedMaskedCoefficientDensity_le_density line 195
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedMaskedCoefficientDensity_local line 222
  14. def OAI.Erdos3.VectorPolynomial.allocatedMaskedTiltedConstant line 247
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedMaskedTiltedConstant_ge_two line 250
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedMaskedCoefficientDensity_one line 262
  17. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_masked_density_tilted_comparison line 282
  18. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_joint_masked_density_comparison line 419