OAI/Probability/IsingPerceptron/ArrayGeometry.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

Array Geometry.

  1. lemma OAI.IsingPerceptron.spinOverlap_symm line 17
  2. lemma OAI.IsingPerceptron.spinOverlap_posSemidef line 20
  3. lemma OAI.IsingPerceptron.labeledCommonDepth_symm line 32
  4. lemma OAI.IsingPerceptron.labeledCommonDepth_ultra line 39
  5. lemma OAI.IsingPerceptron.treeOverlap_symm line 47
  6. lemma OAI.IsingPerceptron.treeOverlap_self line 50
  7. lemma OAI.IsingPerceptron.treeOverlap_ultra line 53
  8. lemma OAI.IsingPerceptron.labeledCommonDepth_sum line 62
  9. lemma OAI.IsingPerceptron.treeOverlap_posSemidef line 81
  10. lemma OAI.IsingPerceptron.replicaLaw_map_reindex line 109
  11. def OAI.IsingPerceptron.permuteJointArray line 121
  12. lemma OAI.IsingPerceptron.continuous_permuteJointArray line 124
  13. lemma OAI.IsingPerceptron.overlapArrayLaw_map_reindex line 128
  14. lemma OAI.IsingPerceptron.jointArray_limit_reindex line 141
  15. lemma OAI.IsingPerceptron.scalar_of_joint_exchangeable line 155
  16. lemma OAI.IsingPerceptron.ae_closed_of_weak_limit line 167
  17. lemma OAI.IsingPerceptron.HasGhirlandaGuerra.congr_ae line 191
  18. def OAI.IsingPerceptron.GramDiagonal line 212
  19. lemma OAI.IsingPerceptron.isClosed_gramDiagonal line 215
  20. lemma OAI.IsingPerceptron.GramDiagonal.symm line 226
  21. lemma OAI.IsingPerceptron.GramDiagonal.default line 232
  22. lemma OAI.IsingPerceptron.gg_ultrametric_ae line 247
  23. lemma OAI.IsingPerceptron.gg_pair_nonnegative_ae line 272
  24. def OAI.IsingPerceptron.spinArray line 301
  25. def OAI.IsingPerceptron.treeArray line 302
  26. lemma OAI.IsingPerceptron.continuous_spinArray line 304
  27. lemma OAI.IsingPerceptron.continuous_treeArray line 305
  28. lemma OAI.IsingPerceptron.isClosed_ultrametricArray line 307
  29. def OAI.IsingPerceptron.JointGeometry line 313
  30. lemma OAI.IsingPerceptron.isClosed_jointGeometry line 317
  31. lemma OAI.IsingPerceptron.sampledJoint_geometry line 322
  32. lemma OAI.IsingPerceptron.enrichedArrayLaw_geometry line 339
  33. lemma OAI.IsingPerceptron.enrichedArrayLaw_reindex line 348
  34. lemma OAI.IsingPerceptron.jointGeometry_sum line 356
  35. lemma OAI.IsingPerceptron.joint_limit_support_ordered line 364
  36. lemma OAI.IsingPerceptron.joint_limit_pair_nonnegative line 384
  37. lemma OAI.IsingPerceptron.enrichedArrayLaw_limit_geometry line 392
  38. theorem OAI.IsingPerceptron.enriched_minimizers_ordered line 422
  39. def OAI.IsingPerceptron.overlapQuantile line 458
  40. lemma OAI.IsingPerceptron.cdf_one_of_unit_support line 461
  41. lemma OAI.IsingPerceptron.quantileSet_nonempty line 471
  42. lemma OAI.IsingPerceptron.quantileSet_bddBelow line 476
  43. lemma OAI.IsingPerceptron.overlapQuantile_mem line 479
  44. lemma OAI.IsingPerceptron.le_cdf_overlapQuantile line 486
  45. lemma OAI.IsingPerceptron.overlapQuantile_le_iff line 495
  46. lemma OAI.IsingPerceptron.monotoneOn_overlapQuantile line 504
  47. def OAI.IsingPerceptron.quantileFunction line 511
  48. lemma OAI.IsingPerceptron.monotone_quantileFunction line 513
  49. lemma OAI.IsingPerceptron.quantileFunction_mem line 520
  50. lemma OAI.IsingPerceptron.cdf_of_lt_zero line 524
  51. lemma OAI.IsingPerceptron.quantileFunction_le_iff line 533
  52. def OAI.IsingPerceptron.unitUniform line 547
  53. instance OAI.IsingPerceptron.unitUniform_probability line 549
  54. lemma OAI.IsingPerceptron.unitUniform_Iic line 553
  55. lemma OAI.IsingPerceptron.quantile_preimage_Iic line 559
  56. lemma OAI.IsingPerceptron.quantileFunction_law line 566