OAI/Combinatorics/Progressions/Estimates/AllocatedOriginalSampleQuadratureUniformBounds.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.allocatedCoefficientSource_supported line 22
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedCoefficientSource_ambient_small line 33
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedSampleRestrictedProfileNoise_short_abs_le line 71
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedSampleRestrictedProfileNoise_short_ae_abs_le line 86
  5. def OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleInactiveCoefficients line 118
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleInactiveCoefficients_supported line 131
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSample_forecast_support_ae line 142
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedShortAxis_grid line 152
  9. def OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleLiftLip line 190
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSamplePrincipal_mass line 193
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleLiftMap_lipschitzOn line 203
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleLiftMap_supported_lipschitzOn line 237
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleLiftMap_affine line 250
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleLift_residue_riemann line 259
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleLift_residue_ae_riemann line 342
  16. def OAI.Erdos3.VectorPolynomial.AllocatedShortIntegerAxis line 394
  17. instance OAI.Erdos3.VectorPolynomial.(instance at line 397) line 397
  18. def OAI.Erdos3.VectorPolynomial.allocatedShortIntegerSelection line 401
  19. theorem OAI.Erdos3.VectorPolynomial.allocatedShortIntegerSelection_injective line 404
  20. def OAI.Erdos3.VectorPolynomial.allocatedShortIntegerAxisEquiv line 408
  21. theorem OAI.Erdos3.VectorPolynomial.allocatedShortIntegerAxis_card line 424
  22. theorem OAI.Erdos3.VectorPolynomial.allocatedShortIntegerSelection_small line 431
  23. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleLift_contained_residue_riemann line 467
  24. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleLift_contained_residue_riemann_of_supported line 518
  25. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleActiveInput_card_le line 573
  26. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleLiftLip_le_allAxis line 584
  27. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleQuadrature_mesh_bound line 591
  28. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleQuadrature_residue_sum_bound line 607