OAI/Combinatorics/Progressions/Sampling/ForecastNativePullbackBudget.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.forecastNormalizedSpatialCoordinates line 15
  2. theorem OAI.Erdos3.VectorPolynomial.forecastNormalizedSpatialCoordinates_lipschitz line 19
  3. theorem OAI.Erdos3.VectorPolynomial.forecastNormalizedSpatialCoordinates_eval line 34
  4. def OAI.Erdos3.VectorPolynomial.forecastNormalizedInactiveCoordinates line 46
  5. theorem OAI.Erdos3.VectorPolynomial.forecastNormalizedInactiveCoordinates_lipschitz line 49
  6. def OAI.Erdos3.VectorPolynomial.forecastNormalizedActiveCoordinates line 62
  7. theorem OAI.Erdos3.VectorPolynomial.forecastNormalizedActiveCoordinates_lipschitz line 65
  8. theorem OAI.Erdos3.VectorPolynomial.forecastNormalizedInactiveCoordinates_mixed line 77
  9. def OAI.Erdos3.VectorPolynomial.forecastActiveAxisEquiv line 108
  10. def OAI.Erdos3.VectorPolynomial.forecastActiveCoordinateJoin line 120
  11. theorem OAI.Erdos3.VectorPolynomial.forecastActiveCoordinateJoin_continuous line 125
  12. theorem OAI.Erdos3.VectorPolynomial.forecastActiveCoordinateJoin_integer line 132
  13. theorem OAI.Erdos3.VectorPolynomial.forecastActiveCoordinateJoin_lipschitz line 138
  14. theorem OAI.Erdos3.VectorPolynomial.forecastActiveCoordinateJoin_joint_lipschitz line 150
  15. theorem OAI.Erdos3.VectorPolynomial.forecastActiveCoordinateJoin_joint_continuous line 163
  16. theorem OAI.Erdos3.VectorPolynomial.forecastActiveCoordinateJoin_norm_le line 168
  17. theorem OAI.Erdos3.VectorPolynomial.forecastActiveCoordinateJoin_continuous_norm_le line 177
  18. theorem OAI.Erdos3.VectorPolynomial.forecastActiveCoordinateJoin_integer_norm_le line 186
  19. theorem OAI.Erdos3.VectorPolynomial.forecastActiveCoordinateJoin_norm line 195
  20. theorem OAI.Erdos3.VectorPolynomial.forecastActiveCoordinateJoin_mixed line 202
  21. def OAI.Erdos3.VectorPolynomial.forecastNativeMixedRow line 235
  22. def OAI.Erdos3.VectorPolynomial.forecastNativeAmbientLinear line 240
  23. def OAI.Erdos3.VectorPolynomial.forecastNativeAmbientLip line 247
  24. theorem OAI.Erdos3.VectorPolynomial.forecastNativeAmbientLinear_lipschitz line 250
  25. theorem OAI.Erdos3.VectorPolynomial.forecastNativeAmbientLinear_mixed line 254
  26. def OAI.Erdos3.VectorPolynomial.forecastNativeFillAxes line 275
  27. theorem OAI.Erdos3.VectorPolynomial.forecastNativeFillAxes_lipschitz line 279
  28. theorem OAI.Erdos3.VectorPolynomial.forecastNativeFillAxes_restrict line 291
  29. def OAI.Erdos3.VectorPolynomial.forecastNativeSpatialInverse line 301
  30. theorem OAI.Erdos3.VectorPolynomial.forecastNativeSpatialInverse_lipschitz line 304
  31. theorem OAI.Erdos3.VectorPolynomial.forecastNativeSpatialInverse_integer line 316
  32. def OAI.Erdos3.VectorPolynomial.forecastNativeTorusInverse line 327
  33. theorem OAI.Erdos3.VectorPolynomial.forecastNativeTorusInverse_lipschitz line 334
  34. theorem OAI.Erdos3.VectorPolynomial.forecastNativeTorusInverse_mixed line 356
  35. theorem OAI.Erdos3.VectorPolynomial.forecastNativeCoveredChart_ambient line 369
  36. theorem OAI.Erdos3.VectorPolynomial.forecastNative_physical_cover_ambient line 394
  37. def OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.forecastPullback line 409
  38. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.forecastPullback_norm_le line 418
  39. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.forecastPullback_lipschitz line 427
  40. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.forecastPullback_mixed line 446
  41. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.forecastPullback_covered_mixed line 464
  42. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.forecastPullback_eval_of_chart line 488
  43. def OAI.Erdos3.VectorPolynomial.forecastNormalizedAmbientCoordinates line 541
  44. theorem OAI.Erdos3.VectorPolynomial.forecastNormalizedAmbientCoordinates_lipschitz line 547
  45. theorem OAI.Erdos3.VectorPolynomial.forecastNormalizedAmbientCoordinates_mixed line 577
  46. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleForecastDensity_supported_zero_off_ball line 636
  47. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleForecastDensity_nonzero_active_bounds line 652
  48. def OAI.Erdos3.VectorPolynomial.forecastNativePrimitiveBudget line 693
  49. theorem OAI.Erdos3.VectorPolynomial.forecastNativeAmbientLip_le_basis_bound line 697
  50. theorem OAI.Erdos3.VectorPolynomial.forecastNativeAmbientLip_le_explicit line 744
  51. theorem OAI.Erdos3.VectorPolynomial.forecastNativeAmbientLip_le_polynomial line 755
  52. theorem OAI.Erdos3.VectorPolynomial.forecastNativeAmbientLip_le_exp line 777