OAI/Combinatorics/Progressions/Sampling/ActualFixedSpatialSlicedForecastSourceLaw.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastSetup.enlargeP line 25
  2. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastSetup.enlargeP_P line 40
  3. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastSetup.enlargeP_D line 41
  4. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastSetup.enlargeP_κ line 42
  5. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastSetup.enlargeP_Pbad line 43
  6. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastSetup.enlargeP_Ppres line 44
  7. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastSetup.withSliceWidth line 46
  8. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastSetup.withSliceWidth_P line 56
  9. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastSetup.withSliceWidth_κ line 57
  10. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastSetup.withSliceWidth_Pbad line 58
  11. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastSetup.withSliceWidth_Ppres line 59
  12. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.enlargeP line 75
  13. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.enlargeP_base line 89
  14. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.enlargeP_noise line 90
  15. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.enlargeP_sample line 91
  16. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.enlargeP_read line 92
  17. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.enlargeP_center line 93
  18. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.enlargeP_commonTuple line 94
  19. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.enlargeP_primes line 95
  20. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.enlargeP_exponent line 96
  21. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.enlargeP_prescribed line 97
  22. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.enlargeP_origin line 98
  23. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.enlargeP_lower line 99
  24. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.enlargeP_width line 100
  25. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.target_enlargeP line 102
  26. structure OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath line 145
  27. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.kernelLower line 181
  28. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.kernelWidth line 182
  29. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.kernelWidth_pos line 186
  30. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.kernelWidth_ne_zero line 193
  31. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.principalLaw line 196
  32. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.det_ne_zero_change_decidable line 202
  33. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.density line 208
  34. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.target line 224
  35. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.weakenSliceWidth line 288
  36. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.weakenSliceWidth_lower line 300
  37. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.weakenSliceWidth_width line 301
  38. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.target_weakenSliceWidth line 303
  39. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.enlargeP line 321
  40. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.weakenSliceWidth line 329
  41. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.enlargeP_path line 341
  42. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.weakenSliceWidth_path line 342
  43. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.enlargeP_kernelLower line 344
  44. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.enlargeP_kernelWidth line 345
  45. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.weakenSliceWidth_kernelLower line 346
  46. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.weakenSliceWidth_kernelWidth line 348
  47. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.enlargeP_principalLaw line 350
  48. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.weakenSliceWidth_principalLaw line 351
  49. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.density_enlargeP line 354
  50. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.density_weakenSliceWidth line 359
  51. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.target_enlargeP line 364
  52. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.target_weakenSliceWidth line 378
  53. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.principalSupport line 427
  54. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.principalLaw_eq_contained line 433
  55. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.kernel_bounds line 446
  56. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.kernelWidth_ge_half_density line 454