OAI/Probability/IsingPerceptron/VarianceOfConditionalCenterBound.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

Variance Of Conditional Center Bound.

  1. theorem OAI.IsingPerceptron.variance_of_conditional_center_bound line 14
  2. theorem OAI.IsingPerceptron.poisson_count_variance line 74
  3. lemma OAI.IsingPerceptron.infinite_prefix_preserving line 101
  4. abbrev OAI.IsingPerceptron.InfiniteRootData line 108
  5. def OAI.IsingPerceptron.rootPrefix line 110
  6. lemma OAI.IsingPerceptron.rootPrefix_preserving line 113
  7. lemma OAI.IsingPerceptron.patternBase_prefix_succ line 120
  8. lemma OAI.IsingPerceptron.rootEnergy_prefix_step line 126
  9. lemma OAI.IsingPerceptron.integral_difference_bound line 138
  10. lemma OAI.IsingPerceptron.cascadeEnergyLog_total_mean line 145
  11. def OAI.IsingPerceptron.infinitePatternRoot line 162
  12. lemma OAI.IsingPerceptron.measurable_infinitePatternRoot line 167
  13. lemma OAI.IsingPerceptron.infinitePatternRoot_fixed_variance line 180
  14. theorem OAI.IsingPerceptron.infinitePatternRoot_poisson_variance line 199
  15. lemma OAI.IsingPerceptron.enriched_poisson_root_variance line 224
  16. abbrev OAI.IsingPerceptron.EnrichedPoissonRoot line 252
  17. def OAI.IsingPerceptron.enrichedPoissonBase line 254
  18. lemma OAI.IsingPerceptron.measurable_enrichedPoissonBase line 258
  19. def OAI.IsingPerceptron.enrichedPoissonLog line 267
  20. lemma OAI.IsingPerceptron.enriched_poisson_unshifted line 273
  21. theorem OAI.IsingPerceptron.enriched_poisson_variance line 299
  22. lemma OAI.IsingPerceptron.perturbationScale_le_one line 316
  23. lemma OAI.IsingPerceptron.perturbationScale_nonneg line 321
  24. lemma OAI.IsingPerceptron.field_cap_arithmetic line 324
  25. lemma OAI.IsingPerceptron.l1_center_le_sqrt_variance line 342
  26. theorem OAI.IsingPerceptron.enriched_field_cap_variance line 356
  27. lemma OAI.IsingPerceptron.labeled_terminal_integral line 394
  28. lemma OAI.IsingPerceptron.cascadeEnergyLog_eq_leaf_integral line 409
  29. def OAI.IsingPerceptron.labeledEnergy line 438
  30. lemma OAI.IsingPerceptron.labeledEnergy_terminal line 443
  31. def OAI.IsingPerceptron.labeledSpinReference line 451
  32. instance OAI.IsingPerceptron.labeledSpinReference_probability line 454
  33. def OAI.IsingPerceptron.labeledEnergyLog line 459
  34. lemma OAI.IsingPerceptron.labeledEnergyLog_eq_leaf line 464
  35. theorem OAI.IsingPerceptron.labeledEnergyLog_eq_cascade line 484
  36. def OAI.IsingPerceptron.enrichedForestCoordinates line 530
  37. instance OAI.IsingPerceptron.enrichedForestCoordinates_probability line 534
  38. def OAI.IsingPerceptron.enrichedForest line 539
  39. lemma OAI.IsingPerceptron.measurable_enrichedForest line 544
  40. theorem OAI.IsingPerceptron.enrichedForest_law line 550
  41. theorem OAI.IsingPerceptron.labeledEnrichedCoordinates_law line 565
  42. lemma OAI.IsingPerceptron.measurable_labeledEnergy line 583
  43. lemma OAI.IsingPerceptron.measurable_labeledEnergyLog line 591
  44. theorem OAI.IsingPerceptron.labeledEnergyLog_eq_cascade_random line 609