OAI/Combinatorics/Progressions/Estimates/AllocatedReferencePrescribeData.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.AllocatedReferenceActualIdealAt line 22
  2. def OAI.Erdos3.VectorPolynomial.AllocatedReferenceChosenIdealAt line 131
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealMeshEnvelope_mono_smoothing line 236
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedActualProfileInput_mono_smoothing line 248
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedProfileFourierInput_nonneg line 254
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedProfileFourierInput_mono line 260
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedProfileFourierOutput_nonneg line 265

    Distinct definitions of this name: OAI/Combinatorics/Progressions/Sampling/AllocatedSiteSamplingBudget.lean:131 (different declaration text). Qualify references as OAI.Erdos3.VectorPolynomial.allocatedProfileFourierOutput_nonneg@path.

  8. theorem OAI.Erdos3.VectorPolynomial.allocatedProfileFourierOutput_mono line 271
  9. theorem OAI.Erdos3.VectorPolynomial.AllocatedReferenceActualIdealAt.mono_smoothing line 285
  10. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_reference_actual_ideal line 342
  11. def OAI.Erdos3.VectorPolynomial.AllocatedReferenceAtScale line 443
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedReferenceActualIdealAt_chooseScale line 568
  13. def OAI.Erdos3.VectorPolynomial.AllocatedReferencePrescribedIdealAt line 626
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedReferenceChosenIdealAt_prescribeData line 664