OAI/Probability/IsingPerceptron/JointGGClosure.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Joint G G Closure.

  1. def OAI.IsingPerceptron.jointMonomialResidual line 15
  2. lemma OAI.IsingPerceptron.jointMonomialResidual_weak_limit line 22
  3. theorem OAI.IsingPerceptron.jointGG_of_weak_monomial_residuals line 41
  4. lemma OAI.IsingPerceptron.replica_injective_map line 65
  5. lemma OAI.IsingPerceptron.replicaLaw_integral_injective line 75
  6. def OAI.IsingPerceptron.enrichedGibbs line 89
  7. instance OAI.IsingPerceptron.enrichedGibbs_probability line 94
  8. lemma OAI.IsingPerceptron.measurable_enrichedGibbs line 99
  9. lemma OAI.IsingPerceptron.spinOverlap_mem line 108
  10. lemma OAI.IsingPerceptron.treeOverlap_mem line 113
  11. def OAI.IsingPerceptron.enrichedJointEntry line 120
  12. def OAI.IsingPerceptron.enrichedReplicaLaw line 123
  13. instance OAI.IsingPerceptron.enrichedReplicaLaw_probability line 129
  14. def OAI.IsingPerceptron.enrichedArrayLaw line 135
  15. lemma OAI.IsingPerceptron.enrichedReplicaLaw_integral line 142
  16. lemma OAI.IsingPerceptron.enrichedArrayLaw_integral line 162
  17. def OAI.IsingPerceptron.enrichedCoordinateObjective line 184
  18. lemma OAI.IsingPerceptron.enriched_contact_cgf line 191
  19. theorem OAI.IsingPerceptron.enriched_gg_at_coordinate_minimum line 245
  20. lemma OAI.IsingPerceptron.gaussian_log_partition_mean_bounds line 322
  21. lemma OAI.IsingPerceptron.cylinder_cgf_mean_bounds line 370
  22. lemma OAI.IsingPerceptron.random_cylinder_cgf_mean_bounds line 384
  23. lemma OAI.IsingPerceptron.enriched_coordinate_pressure_cost line 403
  24. lemma OAI.IsingPerceptron.perturbationWeight_pos line 442
  25. lemma OAI.IsingPerceptron.perturbationAmplitude_sq line 446
  26. lemma OAI.IsingPerceptron.enriched_coordinate_minimum_penalty line 451
  27. lemma OAI.IsingPerceptron.enriched_coordinate_minimum_interior line 484
  28. def OAI.IsingPerceptron.contactStep line 515
  29. def OAI.IsingPerceptron.contactGGRate line 517
  30. lemma OAI.IsingPerceptron.contactGGRate_eq line 524
  31. lemma OAI.IsingPerceptron.tendsto_nat_rpow_neg line 566
  32. lemma OAI.IsingPerceptron.perturbationScale_tendsto line 570
  33. lemma OAI.IsingPerceptron.contactStep_tendsto line 574
  34. lemma OAI.IsingPerceptron.contactGGRate_tendsto line 578