OAI/Probability/IsingPerceptron/NodalGaussianLipschitz.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Nodal Gaussian Lipschitz.

  1. theorem OAI.IsingPerceptron.nodalGaussianFold_lipschitz_strict line 16
  2. theorem OAI.IsingPerceptron.nodalGaussianFold_lipschitz line 63
  3. lemma OAI.IsingPerceptron.uniformCellAverage_le_on line 113
  4. lemma OAI.IsingPerceptron.uniformPattern_ordered_bound line 124
  5. theorem OAI.IsingPerceptron.patternFunctional_ordered_bound line 153
  6. def OAI.IsingPerceptron.lowerTrial line 170
  7. lemma OAI.IsingPerceptron.lowerTrial_ae line 173
  8. lemma OAI.IsingPerceptron.lowerTrial_step line 176
  9. lemma OAI.IsingPerceptron.lowerTrial_value_lt_one line 181
  10. lemma OAI.IsingPerceptron.lowerTrial_entropy_le line 187
  11. lemma OAI.IsingPerceptron.patternFunctional_lowerTrial_tendsto line 195
  12. theorem OAI.IsingPerceptron.gaussian_path_upper_tolerance line 216
  13. def OAI.IsingPerceptron.boundedC2DataOfSmoothCompact line 240
  14. lemma OAI.IsingPerceptron.pressure_eq_finiteLogIntegral line 263
  15. lemma OAI.IsingPerceptron.pressure_abs_bound line 269
  16. lemma OAI.IsingPerceptron.expectedPressure_abs_bound line 291
  17. lemma OAI.IsingPerceptron.isingEntropy_ne_bot line 305
  18. lemma OAI.IsingPerceptron.gaussian_upper_bound_C2 line 313
  19. theorem OAI.IsingPerceptron.gaussian_upper_bound line 332
  20. theorem OAI.IsingPerceptron.gaussian_upper_variational line 338
  21. lemma OAI.IsingPerceptron.Main.bounded_integrable line 350
  22. lemma OAI.IsingPerceptron.Main.bounded_memLp line 355
  23. lemma OAI.IsingPerceptron.Main.bounded_squared line 360
  24. lemma OAI.IsingPerceptron.Main.bounded_mean line 364
  25. lemma OAI.IsingPerceptron.Main.variance_prod_le line 370
  26. theorem OAI.IsingPerceptron.Main.variance_pi_bounded_differences line 406