OAI/Combinatorics/Progressions/Estimates/AllocatedProfileDimensions.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.allocatedGoodKernel_prescribed_comparison line 31
  2. def OAI.Erdos3.VectorPolynomial.allocatedJetTestLog line 92
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedJetTestLog_nonneg line 97
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedJetTestAccuracy_spec line 104
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedGoodKernel_prescribed_test line 150
  6. structure OAI.Erdos3.VectorPolynomial.AllocatedComparisonDimensions line 211
  7. theorem OAI.Erdos3.VectorPolynomial.AllocatedComparisonDimensions.kernel_coefficients line 228
  8. theorem OAI.Erdos3.VectorPolynomial.AllocatedComparisonDimensions.nonkernel_coefficients line 235
  9. theorem OAI.Erdos3.VectorPolynomial.AllocatedComparisonDimensions.layer_degree line 242
  10. def OAI.Erdos3.VectorPolynomial.allocatedKernelEnvelope line 251
  11. def OAI.Erdos3.VectorPolynomial.allocatedDensityEnvelope line 254
  12. def OAI.Erdos3.VectorPolynomial.allocatedSupportEnvelope line 257
  13. def OAI.Erdos3.VectorPolynomial.allocatedTestEnvelope line 260
  14. def OAI.Erdos3.VectorPolynomial.allocatedAccuracyEnvelope line 263
  15. def OAI.Erdos3.VectorPolynomial.allocatedFrontEnvelope line 266
  16. def OAI.Erdos3.VectorPolynomial.allocatedTupleEnvelope line 270
  17. def OAI.Erdos3.VectorPolynomial.allocatedJointLengthEnvelope line 276
  18. def OAI.Erdos3.VectorPolynomial.allocatedTestLengthEnvelope line 280
  19. theorem OAI.Erdos3.VectorPolynomial.allocatedDensityEnvelope_nonneg line 285
  20. theorem OAI.Erdos3.VectorPolynomial.allocatedSupportEnvelope_nonneg line 291
  21. theorem OAI.Erdos3.VectorPolynomial.allocatedTestEnvelope_nonneg line 297
  22. theorem OAI.Erdos3.VectorPolynomial.allocatedTestLengthEnvelope_nonneg line 303
  23. theorem OAI.Erdos3.VectorPolynomial.allocatedKernelLog_le_envelope line 316
  24. theorem OAI.Erdos3.VectorPolynomial.allocatedDensityLog_le_envelope line 328
  25. theorem OAI.Erdos3.VectorPolynomial.allocatedJetSupportLog_le_envelope line 359
  26. theorem OAI.Erdos3.VectorPolynomial.allocatedJetTestLog_le_envelope line 378
  27. theorem OAI.Erdos3.VectorPolynomial.allocatedJointAccuracyLog_le_envelope line 387
  28. theorem OAI.Erdos3.VectorPolynomial.allocatedCoefficientFrontLog_le_envelope line 396
  29. theorem OAI.Erdos3.VectorPolynomial.allocatedKernelReplacementLog_le_envelope line 420
  30. theorem OAI.Erdos3.VectorPolynomial.allocatedTupleLog_le_envelope line 427
  31. theorem OAI.Erdos3.VectorPolynomial.allocatedJointLengthLog_le_envelope line 444
  32. theorem OAI.Erdos3.VectorPolynomial.allocatedTestLengthLog_le_envelope line 468
  33. def OAI.Erdos3.VectorPolynomial.comparisonProfileBound line 489
  34. def OAI.Erdos3.VectorPolynomial.allocatedComparisonDimension line 491
  35. theorem OAI.Erdos3.VectorPolynomial.allocatedComparisonDimension_bounds line 495
  36. theorem OAI.Erdos3.VectorPolynomial.allocatedPrincipalIndex_card_le_variables line 530
  37. theorem OAI.Erdos3.VectorPolynomial.allocatedKernelVariables_card_le_variables line 537
  38. theorem OAI.Erdos3.VectorPolynomial.allocatedJointParameter_card line 543
  39. theorem OAI.Erdos3.VectorPolynomial.allocatedAxes_card_le line 553
  40. theorem OAI.Erdos3.VectorPolynomial.allocatedComparisonDimensions_of_primitive line 563
  41. def OAI.Erdos3.VectorPolynomial.allocatedWitnessScaleLog line 615
  42. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedWitnessScale_of_bounded_source line 625
  43. theorem OAI.Erdos3.VectorPolynomial.allocatedComparisonDimensions_of_primitive_with_cutoff_unboosted line 690
  44. theorem OAI.Erdos3.VectorPolynomial.allocatedComparisonDimensions_of_primitive_with_cutoff line 739
  45. theorem OAI.Erdos3.VectorPolynomial.allocatedComparisonDimensions_of_primitive_withCutoff line 751
  46. theorem OAI.Erdos3.VectorPolynomial.emptyLayerSamplerVariables_card line 774
  47. theorem OAI.Erdos3.VectorPolynomial.emptyLayerCoefficientCount_le line 783
  48. theorem OAI.Erdos3.VectorPolynomial.emptyLayerCoefficientCount_le_exp line 792
  49. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedWitnessScale_with_late_floor line 826
  50. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedWitnessScale_with_exponential_floor line 888
  51. theorem OAI.Erdos3.VectorPolynomial.allocatedAmbientDimension_eq line 931
  52. theorem OAI.Erdos3.VectorPolynomial.allocatedAmbientDimension_le_axes line 937
  53. theorem OAI.Erdos3.VectorPolynomial.allocatedLatticeDimension_eq line 944
  54. theorem OAI.Erdos3.VectorPolynomial.allocatedProfile_dimensions line 953