OAI/Combinatorics/Progressions/Estimates/AllocatedExternalCandidateLocalFixedCenterFront.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.exists_fixedCenter_universal_forecast_model line 43
  2. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.exists_fixedCenter_mask_models line 145
  3. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.exists_fixedCenter_uniform_forecast_model line 238
  4. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrecenterKernelSelection.contracted_member_net line 333
  5. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrecenterKernelSelection.mass_after_native_selection line 343
  6. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrecenterKernelSelection.exists_spatialNativeFamily line 355
  7. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrecenterKernelSelection.fixedCenter_residual_budget line 511
  8. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrecenterKernelSelection.fixedCenter_mass_after_native_selection line 529
  9. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrecenterKernelSelection.exists_fixedCenter_spatialNativeFamily line 544
  10. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrecenterKernelSelection.exists_actualFixedCenter_spatialNativeFamily line 715
  11. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrecenterKernelSelection.exists_localFixedCenter_spatialNativeFamily line 879