OAI/Combinatorics/Progressions/Geometry/AllocatedMaskedChartProduct.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.mixedCoveredSiteResidue line 29
  2. def OAI.Erdos3.VectorPolynomial.allocatedMaskedSiteChartFactor line 33
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedMaskedSiteChartFactor_apply line 41
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedMaskedSiteChartFactor_norm line 53
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedMaskedSiteChartFactor_zero_of_cutoff_zero line 66
  6. theorem OAI.Erdos3.VectorPolynomial.mixedCoveredSiteResidue_measurable line 81
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedMaskedSiteChartFactor_measurable line 95
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedProductMaskedIdealSiteFactor_zero line 147
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedMaskedChartProduct_zero_of_cutoff_zero line 158
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedMaskedMixedProduct_zero_of_cutoff_zero line 170
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedMaskedChartProduct_eq_mixed line 188
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedMaskedChartProduct_zero_outside line 209