OAI/Probability/Perceptron/Cavity/CavityShellPolar.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SphericalPerceptronFreeEnergy.PositiveRadius line 11
  2. def OAI.SphericalPerceptronFreeEnergy.cavityPolarRadius line 13
  3. lemma OAI.SphericalPerceptronFreeEnergy.cavityPolarRadius_measurable line 20
  4. def OAI.SphericalPerceptronFreeEnergy.cavityRadiusLaw line 24
  5. lemma OAI.SphericalPerceptronFreeEnergy.cavity_polar_data_preserving line 28
  6. lemma OAI.SphericalPerceptronFreeEnergy.cavity_polar_radius_preserving line 40
  7. theorem OAI.SphericalPerceptronFreeEnergy.cavitySphereLaw_polar line 50
  8. def OAI.SphericalPerceptronFreeEnergy.cavityRadiusShell line 72
  9. lemma OAI.SphericalPerceptronFreeEnergy.cavityRadiusShell_measurable line 75
  10. lemma OAI.SphericalPerceptronFreeEnergy.cavityShell_smul_preimage line 80
  11. theorem OAI.SphericalPerceptronFreeEnergy.cavitySphereLaw_shell_polar line 86
  12. lemma OAI.SphericalPerceptronFreeEnergy.cavityRadiusShell_bounds line 94
  13. lemma OAI.SphericalPerceptronFreeEnergy.cavity_shell_angular_integrable line 105
  14. lemma OAI.SphericalPerceptronFreeEnergy.cavitySphereLaw_shell_integral line 133
  15. lemma OAI.SphericalPerceptronFreeEnergy.cavitySphereLaw_shell_mass_polar line 150
  16. theorem OAI.SphericalPerceptronFreeEnergy.cavitySphereLaw_shell_lower line 156