OAI/Combinatorics/Progressions/Geometry/AllocatedRowSlicedIdealCoordinates.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.coordinateAffine_norm_le_one line 11
  2. theorem OAI.Erdos3.partitionedSlicedRegularizedIdeal_zero_outside line 29
  3. theorem OAI.Erdos3.activeAveragedSlicedProfileIdeal_zero_outside line 48
  4. theorem OAI.Erdos3.activeScaledSlicedIdeal_bounds line 60
  5. theorem OAI.Erdos3.activeScaledSlicedIdeal_zero_outside line 74
  6. def OAI.Erdos3.realRowsSiteValue line 98
  7. theorem OAI.Erdos3.realRowsSiteValue_coefficient line 103
  8. theorem OAI.Erdos3.realRowsSiteValue_bound line 117
  9. def OAI.Erdos3.VectorPolynomial.allocatedRowIdealCoordinates line 139
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedRowIdealCoordinates_jet line 146
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedRowIdealCoordinates_physical_jets line 155
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedRowIdealCoordinates_density line 166
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedRowIdealCoordinates_bound line 181
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedRowIdealCoordinates_mixed_value line 198
  15. def OAI.Erdos3.VectorPolynomial.allocatedRowSlicedIdeal line 257
  16. def OAI.Erdos3.VectorPolynomial.allocatedRowSlicedSiteRadius line 263
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedRowSlicedSiteRadius_one_le line 269
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedRowSlicedSiteRadius_pos line 275
  19. theorem OAI.Erdos3.VectorPolynomial.allocatedRowSlicedSiteRadius_dominates line 281
  20. theorem OAI.Erdos3.VectorPolynomial.allocatedRowSlicedIdealCoordinates_density line 292
  21. theorem OAI.Erdos3.VectorPolynomial.allocatedRowSlicedIdealCoordinates_bound line 310