OAI/Combinatorics/Progressions/Estimates/AllocatedJointWindowIntegral.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.allocatedJointPlateau_family_error line 39
  2. def OAI.Erdos3.VectorPolynomial.allocatedSelectedNaturalWindow line 125
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedSelectedNaturalWindow_outside line 130
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedSelectedNaturalWindow_card_le line 140
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedJointPhysical_zero_off_window line 153
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedJointPlateau_zero_off_window line 172
  7. def OAI.Erdos3.VectorPolynomial.allocatedGridL1PointTolerance line 219
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedGridL1PointTolerance_spec line 227
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedJointPlateau_family_l1_error line 237
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedJointPlateau_family_test_error line 285
  11. def OAI.Erdos3.VectorPolynomial.allocatedActivePlateauProduct line 374
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedActivePlateauProduct_zero line 377
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedActivePlateauProduct_error line 390
  14. def OAI.Erdos3.VectorPolynomial.allocatedJointNaturalVolume line 470
  15. def OAI.Erdos3.VectorPolynomial.allocatedJointPhysicalKernel line 473
  16. def OAI.Erdos3.VectorPolynomial.allocatedJointPlateauProduct line 477
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedJointWindow_data_support line 489
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedJointWindow_data_error line 509
  19. theorem OAI.Erdos3.VectorPolynomial.allocatedJointPlateau_residue_integral_error line 581