OAI/Combinatorics/Progressions/Estimates/AllocatedOriginalSampleFullSliceLipschitz.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleFullSliceMap line 40
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleFullSliceMap_eq_eval line 46
  3. def OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleTailNoise line 53
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleFullSliceMap_eq_profile line 57
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleLiftMap_eq_tail_ideal line 99
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleFullSliceMap_measurable line 123
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSample_slice_real_perturbation line 135
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSample_slice_complex_perturbation line 176
  9. def OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleFullSliceLip line 262
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleFullSliceMap_affine line 269
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleFullSliceMap_supported_lipschitzOn line 284