OAI/Combinatorics/Progressions/Probability/AllocatedMassTupleComparison.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.allocatedTuple_integral_residues line 40
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedTuple_integral_comparison line 64
  3. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_div_const line 91
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedTuple_mean_residue_comparison line 121
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedTuple_normalized_residue_comparison line 141
  6. def OAI.Erdos3.VectorPolynomial.allocatedOriginalSpatialOutputLaw line 165
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSpatialOutputLaw_join line 172
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalTuple_spatial_density_comparison line 178
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedGoodKernel_original_refined_tuple_density line 235
  10. def OAI.Erdos3.VectorPolynomial.allocatedRefinedTupleMassEstimate line 468
  11. def OAI.Erdos3.VectorPolynomial.allocatedMassTupleStatement line 555
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedGoodKernel_original_mass_tuple_density line 653