OAI/Combinatorics/Progressions/Estimates/AllocatedSlicedProductPrefactorCap.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedSlicedPhysical_supported_site_expansion line 30
  2. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedSlicedIdeal_bounded_site_expansion line 105
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedWholeMaskedCoveredProfile_measurable line 177
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedWholeMaskedCoveredProfile_mean_measurable line 188
  5. def OAI.Erdos3.oneCubeRowsEquiv line 206
  6. theorem OAI.Erdos3.realRowsSiteValue_oneCube line 213
  7. theorem OAI.Erdos3.oneCube_rows_scale_product line 224
  8. def OAI.Erdos3.VectorPolynomial.allocatedOneCubeRowFullJets line 245
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedOneCubeNormalizedSites_rows line 248
  10. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedSlicedIdeal_row_site_expansion line 293
  11. def OAI.Erdos3.VectorPolynomial.allocatedSlicedRowIdeal line 410
  12. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_global_masked_sliced_approximation line 416
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedRowIdeal_measurable line 497
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedWholeMaskedSlicedProfile_mean_measurable line 502
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedRowIdeal_normalized_cap line 546
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedProductPrefactor_cap line 643