OAI/Combinatorics/Progressions/Geometry/AllocatedExternalCandidateSpatialNativeBudget.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.spatialNativeVerticalParameter line 12
  2. def OAI.Erdos3.VectorPolynomial.spatialNativeFactorParameter line 15
  3. theorem OAI.Erdos3.VectorPolynomial.spatialNativeVerticalFactorBounds line 18
  4. def OAI.Erdos3.VectorPolynomial.fullTaggedSpatialIntegerChart line 61
  5. theorem OAI.Erdos3.VectorPolynomial.fullTaggedSpatialIntegerChart_support line 64
  6. def OAI.Erdos3.RationalFilteredNilmanifold.Niltest.fullTaggedSpatial line 84
  7. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.fullTaggedSpatial_eval line 88
  8. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.fullTaggedSpatial_eval_physical line 93
  9. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.fullTaggedSpatial_normBound line 100
  10. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.fullTaggedSpatial_complexity line 103
  11. def OAI.Erdos3.NativeSampleModel.fullTaggedSpatial line 122
  12. theorem OAI.Erdos3.NativeSampleModel.fullTaggedSpatial_test_independent line 135
  13. theorem OAI.Erdos3.NativeSampleModel.fullTaggedSpatial_orbit_independent line 138
  14. theorem OAI.Erdos3.exists_spatialNative_slice_tagged_vertical_partners line 157
  15. structure OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily line 268
  16. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.chart line 329
  17. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.candidate line 332
  18. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.localTest line 335
  19. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.jointOrbit line 338
  20. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.physicalBox line 346
  21. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.physicalBox_val line 351
  22. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.sitePhysicalBox line 355
  23. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.correlation line 359
  24. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.chart_localLaw line 365
  25. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.rawCorrelation_fullSliceLaw line 369
  26. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.selectedCorrelation_localLaw line 401
  27. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.exp_correlation_bound line 438
  28. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.exists_taggedPairFamily line 455
  29. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.exists_precenter_spatial_native_family line 585
  30. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.withBudget line 768
  31. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.withBudget_sourceChart line 800
  32. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.withBudget_sourceCandidate line 803
  33. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.withBudget_reference line 806
  34. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.withBudget_nativeValue line 809
  35. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.withBudget_native line 812
  36. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.withBudget_twist line 815
  37. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.withBudget_eta line 818
  38. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.withBudget_chart line 821
  39. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.withBudget_candidate line 824
  40. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.withBudget_jointOrbit line 827
  41. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.withBudget_correlation line 830
  42. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.withFactorBudget line 833
  43. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.withFactorBudget_sourceChart line 839
  44. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.withFactorBudget_sourceCandidate line 842
  45. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.withFactorBudget_native line 845
  46. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.withFactorBudget_twist line 847
  47. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.withFactorBudget_eta line 849
  48. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.withFactorBudget_correlation line 851
  49. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.factorBudget_bounds line 856