OAI/Probability/Perceptron/Cavity/CavityBlockProduct.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptronFreeEnergy.cavityRadialUnit line 11
  2. lemma OAI.SphericalPerceptronFreeEnergy.cavityRadialUnit_measurable line 14
  3. def OAI.SphericalPerceptronFreeEnergy.cavityUnitEmbed line 18
  4. lemma OAI.SphericalPerceptronFreeEnergy.cavityUnitEmbed_measurable line 21
  5. lemma OAI.SphericalPerceptronFreeEnergy.cavity_radial_rho line 25
  6. lemma OAI.SphericalPerceptronFreeEnergy.cavityRadialBlock_unitEmbed line 35
  7. lemma OAI.SphericalPerceptronFreeEnergy.cavityRadial_reorder_preserving line 42
  8. def OAI.SphericalPerceptronFreeEnergy.cavityUnitLaw line 55
  9. lemma OAI.SphericalPerceptronFreeEnergy.cavityUnitPair_preserving line 59
  10. theorem OAI.SphericalPerceptronFreeEnergy.sphereBlock_product_law line 71
  11. lemma OAI.SphericalPerceptronFreeEnergy.cavityUnitLaw_actual line 80
  12. lemma OAI.SphericalPerceptronFreeEnergy.cavitySphereLaw_unit line 92
  13. def OAI.SphericalPerceptronFreeEnergy.cavitySphereBlockEmbed line 101
  14. lemma OAI.SphericalPerceptronFreeEnergy.cavitySphereBlockEmbed_measurable line 104
  15. lemma OAI.SphericalPerceptronFreeEnergy.cavitySphereBlockEmbed_scaled line 109
  16. lemma OAI.SphericalPerceptronFreeEnergy.cavitySphereBlockEmbed_formula line 114
  17. theorem OAI.SphericalPerceptronFreeEnergy.sphereBlock_scaled_product_law line 121
  18. lemma OAI.SphericalPerceptronFreeEnergy.cavityRadialUnit_norm_lt line 139
  19. lemma OAI.SphericalPerceptronFreeEnergy.cavityUnitLaw_norm_lt line 151
  20. lemma OAI.SphericalPerceptronFreeEnergy.cavitySphereLaw_norm_lt line 157