OAI/Probability/IsingPerceptron/EnrichedFieldCap.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

Enriched Field Cap.

  1. def OAI.IsingPerceptron.finiteLogIntegral line 16
  2. lemma OAI.IsingPerceptron.finiteLogIntegral_eq_logMean line 19
  3. lemma OAI.IsingPerceptron.measurable_finiteLogIntegral line 22
  4. lemma OAI.IsingPerceptron.finiteLogIntegral_lipschitz line 28
  5. lemma OAI.IsingPerceptron.finiteLogIntegral_linearGrowth line 37
  6. lemma OAI.IsingPerceptron.finiteLogIntegral_add_const line 43
  7. def OAI.IsingPerceptron.energyRecursion line 49
  8. lemma OAI.IsingPerceptron.measurable_energyRecursion line 53
  9. lemma OAI.IsingPerceptron.energyRecursion_lipschitz line 59
  10. lemma OAI.IsingPerceptron.energyRecursion_linearGrowth line 68
  11. lemma OAI.IsingPerceptron.finite_gaussian_exponentialNormMoments line 77
  12. theorem OAI.IsingPerceptron.variance_of_conditional_center line 110
  13. def OAI.IsingPerceptron.cascadeEnergyLog line 173
  14. lemma OAI.IsingPerceptron.measurable_cascadeEnergyLog line 178
  15. theorem OAI.IsingPerceptron.cascadeEnergyLog_conditional line 187
  16. theorem OAI.IsingPerceptron.cascadeEnergyLog_variance line 199
  17. def OAI.IsingPerceptron.tagCoefficients line 220
  18. lemma OAI.IsingPerceptron.pair_left_injective line 222
  19. lemma OAI.IsingPerceptron.tagCoefficients_apply line 227
  20. lemma OAI.IsingPerceptron.tagCoefficients_other line 231
  21. lemma OAI.IsingPerceptron.cylinderCross_tag line 239
  22. lemma OAI.IsingPerceptron.cylinderCross_smul line 253
  23. lemma OAI.IsingPerceptron.cylinderCross_sum_right line 263
  24. lemma OAI.IsingPerceptron.cylinderCross_tagged_sum line 269
  25. def OAI.IsingPerceptron.monomialIndex line 280
  26. lemma OAI.IsingPerceptron.monomialIndex_nonzero line 282
  27. lemma OAI.IsingPerceptron.monomialIndex_surjective line 288
  28. def OAI.IsingPerceptron.perturbationScale line 299
  29. def OAI.IsingPerceptron.perturbationWeight line 300
  30. def OAI.IsingPerceptron.externalFieldCoefficients line 302
  31. lemma OAI.IsingPerceptron.externalFieldCoefficients_variance line 306
  32. def OAI.IsingPerceptron.enrichedCoefficients line 314
  33. lemma OAI.IsingPerceptron.perturbationWeight_sum line 321
  34. lemma OAI.IsingPerceptron.perturbationWeight_nonneg line 331
  35. lemma OAI.IsingPerceptron.perturbationWeight_le_one line 333
  36. lemma OAI.IsingPerceptron.enrichedCoefficients_variance_le line 336
  37. abbrev OAI.IsingPerceptron.EnrichedBlock line 377
  38. def OAI.IsingPerceptron.enrichedLevelCoefficient line 379
  39. lemma OAI.IsingPerceptron.spinValue_abs line 386
  40. lemma OAI.IsingPerceptron.spinCoordinate_abs line 390
  41. lemma OAI.IsingPerceptron.tensorFeature_spin_abs line 394
  42. lemma OAI.IsingPerceptron.enrichedLevelCoefficient_abs line 399
  43. lemma OAI.IsingPerceptron.sum_scaled_cross line 406
  44. lemma OAI.IsingPerceptron.enrichedLevelCoefficient_cross line 413
  45. lemma OAI.IsingPerceptron.enrichedLevelCoefficient_variance line 433
  46. lemma OAI.IsingPerceptron.enrichedRoot_envelope_sq line 442
  47. lemma OAI.IsingPerceptron.variance_le_square_about_const line 476
  48. lemma OAI.IsingPerceptron.gaussian_coord_memLp line 485
  49. lemma OAI.IsingPerceptron.gaussian_variance_of_slope line 502
  50. lemma OAI.IsingPerceptron.gaussian_slope_memLp line 528
  51. lemma OAI.IsingPerceptron.variance_prod_le_fiber line 539
  52. theorem OAI.IsingPerceptron.gaussian_variance_coordinate_bound line 563