OAI/Probability/IsingPerceptron/MemLpOfAbsBound.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

Mem Lp Of Abs Bound.

  1. lemma OAI.IsingPerceptron.memLp_of_abs_bound line 13
  2. lemma OAI.IsingPerceptron.integral_abs_le_bound line 19
  3. lemma OAI.IsingPerceptron.variance_le_of_oscillation line 26
  4. lemma OAI.IsingPerceptron.variance_prod_le line 43
  5. lemma OAI.IsingPerceptron.variance_pi_boundedDifferences line 72
  6. lemma OAI.IsingPerceptron.finite_linear_vector_bound line 139
  7. def OAI.IsingPerceptron.rootEnergy line 150
  8. lemma OAI.IsingPerceptron.measurable_rootEnergy line 154
  9. lemma OAI.IsingPerceptron.rootEnergy_gaussian_slope line 160
  10. theorem OAI.IsingPerceptron.rootEnergy_gaussian_variance line 174
  11. lemma OAI.IsingPerceptron.rootEnergy_base_lipschitz line 183
  12. def OAI.IsingPerceptron.patternBase line 198
  13. lemma OAI.IsingPerceptron.patternBase_bound line 201
  14. lemma OAI.IsingPerceptron.patternBase_one_change line 212
  15. theorem OAI.IsingPerceptron.pattern_root_energy_variance line 225
  16. def OAI.IsingPerceptron.enrichedCoefficientsFin line 292
  17. def OAI.IsingPerceptron.enrichedIncrement line 296
  18. lemma OAI.IsingPerceptron.measurable_enrichedIncrement line 300
  19. def OAI.IsingPerceptron.enrichedIncrementLaw line 305
  20. lemma OAI.IsingPerceptron.enrichedIncrementLaw_moments line 310
  21. theorem OAI.IsingPerceptron.enriched_root_variance line 317
  22. lemma OAI.IsingPerceptron.pattern_root_energy_memLp line 347
  23. abbrev OAI.IsingPerceptron.EnrichedRootSize line 389
  24. abbrev OAI.IsingPerceptron.EnrichedRootData line 390
  25. def OAI.IsingPerceptron.enrichedBaseEnergy line 392
  26. lemma OAI.IsingPerceptron.measurable_enrichedBaseEnergy line 396
  27. def OAI.IsingPerceptron.enrichedFixedCountLog line 405
  28. lemma OAI.IsingPerceptron.enrichedBaseEnergy_memLp line 411
  29. lemma OAI.IsingPerceptron.enriched_fixed_count_unshifted line 430
  30. lemma OAI.IsingPerceptron.memLp_variance_shift line 457
  31. theorem OAI.IsingPerceptron.enriched_fixed_count_variance line 465
  32. def OAI.IsingPerceptron.poissonMass line 483
  33. lemma OAI.IsingPerceptron.poissonMass_succ line 485
  34. lemma OAI.IsingPerceptron.poisson_first_hasSum line 493
  35. lemma OAI.IsingPerceptron.poisson_second_hasSum line 505
  36. lemma OAI.IsingPerceptron.poisson_cast_memLp line 521
  37. lemma OAI.IsingPerceptron.poisson_cast_mean line 527
  38. lemma OAI.IsingPerceptron.poisson_cast_second line 531
  39. lemma OAI.IsingPerceptron.poisson_cast_variance line 535
  40. lemma OAI.IsingPerceptron.integral_prod_sub_sq line 540
  41. lemma OAI.IsingPerceptron.variance_of_distance_bound line 567
  42. lemma OAI.IsingPerceptron.nat_abs_step_bound line 582
  43. lemma OAI.IsingPerceptron.nat_step_memLp line 602