OAI/Probability/Perceptron/Pressure/FiniteTerminal.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.le_terminalTrial line 20
  2. lemma OAI.SphericalPerceptronFreeEnergy.terminalTrial_finite_range line 24
  3. lemma OAI.SphericalPerceptronFreeEnergy.terminalTrial_tail line 33
  4. lemma OAI.SphericalPerceptronFreeEnergy.tailIntegral_antitone line 41
  5. lemma OAI.SphericalPerceptronFreeEnergy.terminalTrial_entropy_finite line 47
  6. lemma OAI.SphericalPerceptronFreeEnergy.terminalTrial_L1_le line 68
  7. lemma OAI.SphericalPerceptronFreeEnergy.upperRoundedTrial_L1_le line 86
  8. lemma OAI.SphericalPerceptronFreeEnergy.exists_finite_terminal_trial_approx line 97
  9. def OAI.SphericalPerceptronFreeEnergy.FiniteTerminal line 123
  10. def OAI.SphericalPerceptronFreeEnergy.finiteTerminalVariational line 126
  11. lemma OAI.SphericalPerceptronFreeEnergy.finiteTerminal_one line 130
  12. lemma OAI.SphericalPerceptronFreeEnergy.finiteTerminalVariational_bounds line 136
  13. lemma OAI.SphericalPerceptronFreeEnergy.finiteTerminalVariational_coe_toReal line 153
  14. lemma OAI.SphericalPerceptronFreeEnergy.terminalVariational_eq_finiteTerminal line 160
  15. def OAI.SphericalPerceptronFreeEnergy.Jet3.ofCompactSmooth line 200
  16. lemma OAI.SphericalPerceptronFreeEnergy.Jet3.ofCompactSmooth_apply line 213
  17. lemma OAI.SphericalPerceptronFreeEnergy.exists_bounded_smooth_terminal line 216
  18. lemma OAI.SphericalPerceptronFreeEnergy.exists_bounded_smooth_terminal_sequence line 246
  19. lemma OAI.SphericalPerceptronFreeEnergy.finiteTerminalVariational_toReal_sub_le line 271
  20. lemma OAI.SphericalPerceptronFreeEnergy.finiteTerminalVariational_abs_sub_le line 295
  21. lemma OAI.SphericalPerceptronFreeEnergy.terminalVariational_eq_finiteTerminal_continuous line 305
  22. abbrev OAI.SphericalPerceptronFreeEnergy.RadialSpace line 342
  23. def OAI.SphericalPerceptronFreeEnergy.radialNormalizer line 344
  24. def OAI.SphericalPerceptronFreeEnergy.canonicalRadialDensity line 346
  25. def OAI.SphericalPerceptronFreeEnergy.canonicalRadialMass line 349
  26. lemma OAI.SphericalPerceptronFreeEnergy.radialNormalizer_pos line 352
  27. lemma OAI.SphericalPerceptronFreeEnergy.canonicalRadialDensity_pos line 356
  28. lemma OAI.SphericalPerceptronFreeEnergy.canonicalRadialDensity_continuous line 359
  29. lemma OAI.SphericalPerceptronFreeEnergy.integrable_exp_neg_norm_sq line 362
  30. lemma OAI.SphericalPerceptronFreeEnergy.canonicalRadialDensity_integrable line 372
  31. lemma OAI.SphericalPerceptronFreeEnergy.canonicalRadialDensity_integral line 376
  32. instance OAI.SphericalPerceptronFreeEnergy.(instance at line 387) line 387
  33. lemma OAI.SphericalPerceptronFreeEnergy.canonicalRadialMass_apply line 396
  34. lemma OAI.SphericalPerceptronFreeEnergy.canonicalRadial_mass_le line 403