OAI/Combinatorics/Progressions/Estimates/AllocatedRecoveredPreparedFreeze.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerSupported_polynomial_bound line 27
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineDensity_small_integer_remainder line 60
  3. theorem OAI.Erdos3.allocated_prepared_freezing line 108
  4. def OAI.Erdos3.VectorPolynomial.AllocatedCenteredFramedRecoveredSampleAt line 182
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedCentered_recovered_sample_ae line 200
  6. theorem OAI.Erdos3.VectorPolynomial.AllocatedCenteredFramedRecoveredSampleAt.freezing_lifts line 265
  7. instance OAI.Erdos3.VectorPolynomial.coefficientTorus_zeroLayer_subsingleton line 325
  8. def OAI.Erdos3.VectorPolynomial.allocatedZeroLayerFramedRead line 340
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedZeroLayerFramedRead_noise line 347
  10. def OAI.Erdos3.VectorPolynomial.allocatedZeroLayerSample line 352
  11. def OAI.Erdos3.VectorPolynomial.allocatedZeroLayerCenterLift line 361
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedZeroLayerCenterLift_spec line 364
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedZeroLayer_recovered_sample line 379
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedZeroLayer_recovered line 393
  15. theorem OAI.Erdos3.PolynomialPatch.LowestLayerModel.exists_freeze_allocated_recovered_sample line 424