OAI/Combinatorics/Progressions/Estimates/AllocatedRecenteredIdealError.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedProductChartIdealApproximation line 63
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedProductChartIdealApproximation_measurable line 71
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedProductChartIdealApproximation_eq_mixed line 96
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedProductChartIdealApproximation_zero_outside line 112
  5. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_global_masked_ideal_approximation line 125
  6. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_global_masked_ideal_approximation_cutoff line 245
  7. def OAI.Erdos3.VectorPolynomial.AllocatedLongPhysicalExpansionIdentity line 356
  8. def OAI.Erdos3.VectorPolynomial.AllocatedGridPhysicalExpansionIdentity line 363
  9. def OAI.Erdos3.VectorPolynomial.AllocatedModelPhysicalExpansionIdentity line 371
  10. theorem OAI.Erdos3.VectorPolynomial.join_allocated_physical_expansions line 381
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedProductChartIdealApproximation_physical line 442
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedProductPrefactor_physical_site_error line 453
  13. structure OAI.Erdos3.VectorPolynomial.AllocatedFiniteIdealData line 478
  14. abbrev OAI.Erdos3.VectorPolynomial.AllocatedFiniteIdealData.Term line 483
  15. def OAI.Erdos3.VectorPolynomial.AllocatedFiniteIdealData.Bounds line 523
  16. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_finite_ideal_data line 572
  17. theorem OAI.Erdos3.BooleanCubeKernel.finiteProbability_weightedError_test_le line 595
  18. theorem OAI.Erdos3.BooleanCubeKernel.selectedResidue_weightedError_test_le line 613
  19. theorem OAI.Erdos3.BooleanCubeKernel.allocatedProductIdealError_sampled line 661
  20. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_global_masked_ideal_approximation_sampled line 753
  21. theorem OAI.Erdos3.BooleanCubeKernel.finite_weighted_window_norm_mono line 820
  22. theorem OAI.Erdos3.BooleanCubeKernel.allocatedProductIdealError_recentered_mass line 879