OAI/Combinatorics/Progressions/Estimates/AllocatedSlicedRowsProjectedSource.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.containedProgressionCubeMap_injOn line 19
  2. theorem OAI.Erdos3.integerScalarCubeWeights_mean_finset line 32
  3. theorem OAI.Erdos3.containedScalarProgression_mean_le_card_ratio line 43
  4. theorem OAI.Erdos3.containedScalarProgression_weight_le_card_ratio line 59
  5. theorem OAI.Erdos3.integerScalarCubeSet_card_ratio_le line 69
  6. theorem OAI.Erdos3.containedProgressionCubeLaw_eventProbability_le line 97
  7. theorem OAI.Erdos3.containedProgressionKernel_explicit_probability_le line 126
  8. theorem OAI.Erdos3.BooleanCubeKernel.physicalRowsStandardEquiv_symm_sample line 180
  9. theorem OAI.Erdos3.BooleanCubeKernel.physicalCubePositiveTest_rows line 189
  10. def OAI.Erdos3.VectorPolynomial.allocatedSlicedTupleValue line 263
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedTupleValue_coordinates line 279
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedCubeSource_disintegrate line 306
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedTupleValue_pathLaw line 349
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedTupleValue_norm_le line 365
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedCubeSource_good_residue_selection line 381
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedCubeSource_good_kernel_residue line 430
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedTupleValue_select_base line 513
  18. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_sliced_projected_source line 554
  19. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_sliced_rows_projected_source line 658