OAI/Combinatorics/Progressions/Estimates/AllocatedExternalRetainedResidual.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.sliceTest line 42
  2. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.sliceTest_normBound line 46
  3. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.sliceTest_lipBound line 49
  4. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.sliceTest_observable line 52
  5. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.sliceTest_complexity line 55
  6. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.sliceTest_eval line 58
  7. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.sliceTest_eval_on_slice line 72
  8. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.sliceTest_correlation line 79
  9. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.normalizedSlicePacket line 131
  10. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.normalizedSlicePacket_weight line 146
  11. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.fixedNatural line 168
  12. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.fixedNatural_lt line 171
  13. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.frozenLongExtension_fixedNatural line 181
  14. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.admissibleFullPacket line 207
  15. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.admissibleFullPacket_expect line 224
  16. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.admissibleFullPacket_site_expect line 271
  17. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.localLaw_residual_le_of_uniform line 286
  18. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.localLaw_residual_le_exp_of_uniform line 304
  19. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.localLaw_residual_le_exp_of_uniform_budget line 317
  20. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.fullFixed line 363
  21. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.fullFixed_lt line 366
  22. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.frozenLongExtension_eq line 371
  23. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.retainedSliceTest line 399
  24. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.fullSliceTest line 413
  25. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.fullSliceTest_correlation line 422
  26. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.nativeSlicePacket line 488
  27. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.localLaw_residual_le_of_universal_niltest line 503
  28. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.localLaw_residual_le_exp_of_universal_native_budget line 592
  29. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Conclusion.retainedResidualPacket line 658
  30. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Conclusion.retainedResidualPacket_weight line 683
  31. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Conclusion.retainedResidualPacket_expect line 688
  32. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Conclusion.residualPacket line 719
  33. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Conclusion.residualPacket_weight line 727
  34. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Conclusion.residualPacket_retained line 735
  35. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Conclusion.retained_residual_mean_le_sampledSliceSeminorm line 740