OAI/Probability/IsingPerceptron/EnrichedCGF.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Enriched C G F.

  1. lemma OAI.IsingPerceptron.integral_comp_preserving_ae line 16
  2. def OAI.IsingPerceptron.enrichedMeanPressure line 24
  3. def OAI.IsingPerceptron.enrichedCGF line 29
  4. theorem OAI.IsingPerceptron.enrichedCGF_integral line 35
  5. theorem OAI.IsingPerceptron.enrichedCGF_center_bound line 71
  6. lemma OAI.IsingPerceptron.noise_energy_exp_integrable line 143
  7. lemma OAI.IsingPerceptron.labeled_energy_exp_integrable line 174
  8. def OAI.IsingPerceptron.cascadeCoordinateLaw line 219
  9. instance OAI.IsingPerceptron.cascadeCoordinateLaw_probability line 224
  10. lemma OAI.IsingPerceptron.cascadeCoordinates_preserving line 229
  11. def OAI.IsingPerceptron.cascadeCoordinateEnergy line 235
  12. lemma OAI.IsingPerceptron.cascadeCoordinateEnergy_eq line 240
  13. lemma OAI.IsingPerceptron.cascadeCoordinate_exp_integrable line 245
  14. lemma OAI.IsingPerceptron.cascadeCoordinate_log_integral line 254
  15. lemma OAI.IsingPerceptron.cylinder_weighted_variant_eq line 289
  16. lemma OAI.IsingPerceptron.dual_cylinderField line 296
  17. lemma OAI.IsingPerceptron.cylinder_finite_law_eq line 311
  18. theorem OAI.IsingPerceptron.cylinder_fields_law_eq line 333
  19. def OAI.IsingPerceptron.gaussianPair line 354
  20. lemma OAI.IsingPerceptron.gaussianPair_preserving line 357
  21. def OAI.IsingPerceptron.gaussianSumCoefficients line 366
  22. lemma OAI.IsingPerceptron.gaussianSumCoefficients_field line 369
  23. lemma OAI.IsingPerceptron.gaussianSumCoefficients_cross line 377
  24. theorem OAI.IsingPerceptron.cylinder_independent_sum_law line 387
  25. lemma OAI.IsingPerceptron.hasDerivAt_mean_cgf line 416
  26. lemma OAI.IsingPerceptron.integral_tilted_eq_single_replica line 451
  27. lemma OAI.IsingPerceptron.integrable_random_cylinder_tilted_mean line 461
  28. theorem OAI.IsingPerceptron.hasDerivAt_random_cylinder_cgf line 479
  29. lemma OAI.IsingPerceptron.cylinder_tilted_mean_eq_energy line 494
  30. theorem OAI.IsingPerceptron.hasDerivAt_random_cylinder_covariance line 510
  31. lemma OAI.IsingPerceptron.exp_mul_le_endpoints line 538
  32. lemma OAI.IsingPerceptron.continuous_bounded_exponential_integral line 546
  33. lemma OAI.IsingPerceptron.replica_all_exp line 563
  34. lemma OAI.IsingPerceptron.continuous_referenceReplicaMean line 569
  35. lemma OAI.IsingPerceptron.continuous_randomReplicaAverage line 587