OAI/Probability/IsingPerceptron/DeviationRate.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

Deviation Rate.

  1. def OAI.IsingPerceptron.Main.sourceDeviationRate line 14
  2. lemma OAI.IsingPerceptron.Main.sourceDeviationRate_tendsto line 17
  3. lemma OAI.IsingPerceptron.Main.source_eta_eventually line 29
  4. lemma OAI.IsingPerceptron.Main.scale_rate_identity line 38
  5. lemma OAI.IsingPerceptron.Main.source_scale_inverse line 45
  6. theorem OAI.IsingPerceptron.Main.source_rawTensor_deviation_rate line 52
  7. lemma OAI.IsingPerceptron.Main.parameter_resampling_preserving line 84
  8. def OAI.IsingPerceptron.Main.parameterCoordinateLaw line 120
  9. instance OAI.IsingPerceptron.Main.parameterCoordinateLaw_probability line 122
  10. def OAI.IsingPerceptron.Main.sourceParameterLaw line 126
  11. instance OAI.IsingPerceptron.Main.sourceParameterLaw_probability line 128
  12. lemma OAI.IsingPerceptron.Main.parameterCoordinateLaw_mem line 132
  13. lemma OAI.IsingPerceptron.Main.sourceParameterLaw_mem line 135
  14. lemma OAI.IsingPerceptron.Main.integral_parameterCoordinateLaw line 140
  15. instance OAI.IsingPerceptron.Main.perturbedDisorderLaw_probability line 145
  16. def OAI.IsingPerceptron.Main.tensorMeanAt line 149
  17. def OAI.IsingPerceptron.Main.tensorDeviationAt line 153
  18. lemma OAI.IsingPerceptron.Main.tensorMeanAt_measurable line 157
  19. lemma OAI.IsingPerceptron.Main.tensorDeviationAt_measurable line 166
  20. def OAI.IsingPerceptron.Main.tensorMajorant line 188
  21. lemma OAI.IsingPerceptron.Main.tensorMajorant_memLp line 192
  22. lemma OAI.IsingPerceptron.Main.tensorMeanAt_bound line 204
  23. lemma OAI.IsingPerceptron.Main.tensorMeanAt_integrable line 209
  24. lemma OAI.IsingPerceptron.Main.tensorDeviationAt_bound line 217
  25. lemma OAI.IsingPerceptron.Main.tensorDeviationAt_integrable line 233
  26. def OAI.IsingPerceptron.Main.meanTensorDeviation line 241
  27. lemma OAI.IsingPerceptron.Main.meanTensorDeviation_measurable line 244
  28. lemma OAI.IsingPerceptron.Main.meanTensorDeviation_nonneg line 248
  29. lemma OAI.IsingPerceptron.Main.meanTensorDeviation_bound line 256
  30. lemma OAI.IsingPerceptron.Main.meanTensorDeviation_integrable line 271
  31. lemma OAI.IsingPerceptron.Main.integral_resample_parameter line 277
  32. lemma OAI.IsingPerceptron.Main.meanTensorDeviation_update line 292
  33. theorem OAI.IsingPerceptron.Main.source_parameter_deviation_rate line 299
  34. def OAI.IsingPerceptron.Main.sourceDeviation line 325
  35. lemma OAI.IsingPerceptron.Main.sourceDeviation_measurable line 331
  36. lemma OAI.IsingPerceptron.Main.sourceDeviation_integrable line 338
  37. lemma OAI.IsingPerceptron.Main.sourceDeviation_nonneg line 345
  38. theorem OAI.IsingPerceptron.Main.source_integrated_deviation_tendsto line 352
  39. def OAI.IsingPerceptron.Main.slowDiagonal line 371
  40. lemma OAI.IsingPerceptron.Main.slowDiagonal_le line 375
  41. lemma OAI.IsingPerceptron.Main.slowDiagonal_mono line 378
  42. lemma OAI.IsingPerceptron.Main.slowDiagonal_bound line 382
  43. lemma OAI.IsingPerceptron.Main.slowDiagonal_tendsto line 391
  44. lemma OAI.IsingPerceptron.Main.slowDiagonal_sum_tendsto line 405
  45. def OAI.IsingPerceptron.Main.sourceGoodCutoff line 418
  46. def OAI.IsingPerceptron.Main.sourceGoodError line 421
  47. def OAI.IsingPerceptron.Main.sourceGoodTolerance line 425
  48. def OAI.IsingPerceptron.Main.sourceGoodParameters line 428
  49. lemma OAI.IsingPerceptron.Main.sourceGoodCutoff_le line 433
  50. lemma OAI.IsingPerceptron.Main.sourceGoodCutoff_monotone line 436
  51. lemma OAI.IsingPerceptron.Main.sourceGoodCutoff_tendsto line 439
  52. lemma OAI.IsingPerceptron.Main.sourceGoodError_nonneg line 444
  53. lemma OAI.IsingPerceptron.Main.sourceGoodError_tendsto line 447
  54. lemma OAI.IsingPerceptron.Main.sourceGoodTolerance_pos line 453
  55. lemma OAI.IsingPerceptron.Main.sourceGoodTolerance_tendsto line 458
  56. lemma OAI.IsingPerceptron.Main.sourceGoodParameters_measurable line 467
  57. lemma OAI.IsingPerceptron.Main.sourceGoodParameters_bad_bound line 478
  58. lemma OAI.IsingPerceptron.Main.sourceGoodParameters_bad_sqrt line 510
  59. lemma OAI.IsingPerceptron.Main.sourceGoodParameters_probability line 520
  60. lemma OAI.IsingPerceptron.Main.sourceGoodParameters_uniform line 537
  61. theorem OAI.IsingPerceptron.Main.source_good_parameters line 543