OAI/Probability/Perceptron/Interpolation/FiniteOverlap.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.ultrametric_extension_row line 14
  2. lemma OAI.SphericalPerceptronFreeEnergy.finite_measure_eq_of_maximal_coordinates line 26
  3. lemma OAI.SphericalPerceptronFreeEnergy.finite_ultrametric_row_law_unique line 76
  4. abbrev OAI.SphericalPerceptronFreeEnergy.FiniteOverlap line 93
  5. abbrev OAI.SphericalPerceptronFreeEnergy.FiniteBlock line 94
  6. def OAI.SphericalPerceptronFreeEnergy.finiteBlock line 96
  7. def OAI.SphericalPerceptronFreeEnergy.finiteRow line 99
  8. def OAI.SphericalPerceptronFreeEnergy.FiniteGG line 102
  9. lemma OAI.SphericalPerceptronFreeEnergy.finiteBlock_measurable line 108
  10. lemma OAI.SphericalPerceptronFreeEnergy.finiteRow_measurable line 113
  11. def OAI.SphericalPerceptronFreeEnergy.finiteFiberRow line 118
  12. lemma OAI.SphericalPerceptronFreeEnergy.finiteFiberRow_real line 122
  13. lemma OAI.SphericalPerceptronFreeEnergy.finiteFiberRow_unique line 135
  14. lemma OAI.SphericalPerceptronFreeEnergy.map_pair_eq_of_fiber_map_eq line 199
  15. def OAI.SphericalPerceptronFreeEnergy.finiteExtension line 219
  16. lemma OAI.SphericalPerceptronFreeEnergy.finiteBlock_eq_extension line 224
  17. lemma OAI.SphericalPerceptronFreeEnergy.finiteBlock_succ_law_unique line 236
  18. theorem OAI.SphericalPerceptronFreeEnergy.finiteGG_block_law_unique line 266
  19. lemma OAI.SphericalPerceptronFreeEnergy.measureReal_atom_inter_of_ae_const line 297
  20. lemma OAI.SphericalPerceptronFreeEnergy.finiteGG_of_ge_two line 314
  21. lemma OAI.SphericalPerceptronFreeEnergy.poisson_power_integral line 349
  22. def OAI.SphericalPerceptronFreeEnergy.finitePointMeasure line 367
  23. lemma OAI.SphericalPerceptronFreeEnergy.finitePointMeasure_measurable line 370
  24. def OAI.SphericalPerceptronFreeEnergy.finitePoissonLaw line 375
  25. instance OAI.SphericalPerceptronFreeEnergy.finitePoissonLaw_probability line 380
  26. def OAI.SphericalPerceptronFreeEnergy.expNegENNReal line 394
  27. lemma OAI.SphericalPerceptronFreeEnergy.expNegENNReal_bound line 396
  28. lemma OAI.SphericalPerceptronFreeEnergy.expNegENNReal_continuous line 401