OAI/Combinatorics/Progressions/Probability/AllocatedPrescribedRefinedDensity.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedCoveredFixedFactor line 40
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedCoveredFixedFactor_nonneg line 49
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalDeckDensity_eq line 58
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalCoveredDensity_factorization line 73
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalCoveredDensity_mean line 99
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalCoveredDensity_residue_comparison line 124
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedRestrictedCoefficientError_mass_of_box line 213
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedRestrictedCoefficientError_mass line 292
  9. def OAI.Erdos3.VectorPolynomial.allocatedPhysicalKernelPivot line 340
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalKernelPivot_det line 346
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalDensityFamily_restricted line 394
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalDensityFamily_residue_comparison line 413
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalDensityFamily_refined_comparison line 516
  14. theorem OAI.Erdos3.FiniteProbabilityWeights.norm_spatial_density_product_error line 570
  15. theorem OAI.Erdos3.FiniteProbabilityWeights.norm_spatial_density_sum_error line 587
  16. theorem OAI.Erdos3.FiniteProbabilityWeights.norm_spatial_density_sum_error_normalized line 610
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginal_refined_density_comparison line 696
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedGoodKernel_prescribed_refined_density line 846