OAI/Probability/Perceptron/Variational/NormSquareBand.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.canonicalRadial_upper_tail line 21
  2. lemma OAI.SphericalPerceptronFreeEnergy.canonicalRadial_lower_tail line 47
  3. def OAI.SphericalPerceptronFreeEnergy.normSquareBand line 73
  4. lemma OAI.SphericalPerceptronFreeEnergy.normSquareBand_measurable line 76
  5. lemma OAI.SphericalPerceptronFreeEnergy.canonicalRadial_band_compl_le line 80
  6. lemma OAI.SphericalPerceptronFreeEnergy.exp_neg_mul_nat_succ_tendsto line 96
  7. lemma OAI.SphericalPerceptronFreeEnergy.canonicalRadial_band_eventually_half line 102
  8. lemma OAI.SphericalPerceptronFreeEnergy.canonicalRadialMass_real_apply line 124
  9. lemma OAI.SphericalPerceptronFreeEnergy.canonicalRadialDensity_tilt line 130
  10. lemma OAI.SphericalPerceptronFreeEnergy.normSquareBand_tilt_bounds line 137
  11. lemma OAI.SphericalPerceptronFreeEnergy.canonicalRadial_band_mass_bounds line 150
  12. lemma OAI.SphericalPerceptronFreeEnergy.canonicalRadial_band_log_bounds line 190
  13. lemma OAI.SphericalPerceptronFreeEnergy.canonicalRadial_band_log_eventually line 212
  14. lemma OAI.SphericalPerceptronFreeEnergy.unitSphere_continuous_integrable line 220
  15. def OAI.SphericalPerceptronFreeEnergy.sphericalExp line 226
  16. lemma OAI.SphericalPerceptronFreeEnergy.sphericalExp_even line 229
  17. lemma OAI.SphericalPerceptronFreeEnergy.sphericalExp_eq_cosh line 242
  18. lemma OAI.SphericalPerceptronFreeEnergy.sphericalExp_mono line 254
  19. lemma OAI.SphericalPerceptronFreeEnergy.one_le_sphericalExp line 264
  20. lemma OAI.SphericalPerceptronFreeEnergy.polar_lintegral line 276
  21. lemma OAI.SphericalPerceptronFreeEnergy.polar_lintegral_swap line 297
  22. def OAI.SphericalPerceptronFreeEnergy.normalizedAngular line 305
  23. def OAI.SphericalPerceptronFreeEnergy.haarRadiusMeasure line 308
  24. lemma OAI.SphericalPerceptronFreeEnergy.angular_total_ne_zero line 311
  25. lemma OAI.SphericalPerceptronFreeEnergy.polar_lintegral_normalized line 314
  26. lemma OAI.SphericalPerceptronFreeEnergy.polar_radial_lintegral line 324
  27. lemma OAI.SphericalPerceptronFreeEnergy.polar_weighted_lintegral line 335
  28. lemma OAI.SphericalPerceptronFreeEnergy.polar_weighted_bounds line 348
  29. def OAI.SphericalPerceptronFreeEnergy.linearFieldFactor line 373
  30. def OAI.SphericalPerceptronFreeEnergy.angularFieldFactor line 376
  31. lemma OAI.SphericalPerceptronFreeEnergy.linearFieldFactor_measurable line 380
  32. lemma OAI.SphericalPerceptronFreeEnergy.angularFieldFactor_eq line 385
  33. lemma OAI.SphericalPerceptronFreeEnergy.angularFieldFactor_mono line 396
  34. lemma OAI.SphericalPerceptronFreeEnergy.one_le_angularFieldFactor line 402
  35. def OAI.SphericalPerceptronFreeEnergy.canonicalBandRadiusWeight line 410
  36. lemma OAI.SphericalPerceptronFreeEnergy.canonicalBandRadiusWeight_measurable line 414
  37. lemma OAI.SphericalPerceptronFreeEnergy.canonicalBandRadiusWeight_integral line 420