OAI/Combinatorics/Progressions/Fourier/AllocatedExternalCandidateSpatialNativeFrequencyTransport.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.withFrequencies line 51
  2. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.withFrequencies_eta line 61
  3. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.withFrequencies_sourceChart line 63
  4. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.withFrequencies_sourceCandidate line 66
  5. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.withFrequencies_reference line 69
  6. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.withFrequencies_nativeValue line 72
  7. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.withFrequencies_native line 75
  8. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.withFrequencies_twist line 78
  9. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.withFrequencies_chart line 81
  10. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.withFrequencies_candidate line 84
  11. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.withFrequencies_localTest line 87
  12. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.withFrequencies_jointOrbit line 90
  13. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.withFrequencies_physicalBox line 93
  14. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.withFrequencies_sitePhysicalBox line 97
  15. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.withFrequencies_correlation line 100
  16. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.withFrequencies_withBudget line 103
  17. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.withFrequencies_withFactorBudget line 107