OAI/Probability/Perceptron/Variational/Trial.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SphericalPerceptronFreeEnergy.timeLaw_eq_volume line 14
  2. instance OAI.SphericalPerceptronFreeEnergy.(instance at line 16) line 16
  3. instance OAI.SphericalPerceptronFreeEnergy.(instance at line 20) line 20
  4. theorem OAI.SphericalPerceptronFreeEnergy.progressive_zero line 24
  5. theorem OAI.SphericalPerceptronFreeEnergy.controlCost_zero line 29
  6. theorem OAI.SphericalPerceptronFreeEnergy.controlPayoff_zero line 33
  7. theorem OAI.SphericalPerceptronFreeEnergy.abs_integral_reward_le line 37
  8. theorem OAI.SphericalPerceptronFreeEnergy.controlPayoff_le_norm line 45
  9. theorem OAI.SphericalPerceptronFreeEnergy.controlPayoffs_nonempty line 54
  10. theorem OAI.SphericalPerceptronFreeEnergy.controlPayoffs_bddAbove line 59
  11. theorem OAI.SphericalPerceptronFreeEnergy.controlValue_le_norm line 67
  12. theorem OAI.SphericalPerceptronFreeEnergy.zero_payoff_le_controlValue line 73
  13. theorem OAI.SphericalPerceptronFreeEnergy.neg_norm_le_controlValue line 79
  14. theorem OAI.SphericalPerceptronFreeEnergy.abs_controlValue_le line 84
  15. def OAI.SphericalPerceptronFreeEnergy.oneTrial line 88
  16. theorem OAI.SphericalPerceptronFreeEnergy.oneTrial_apply line 95
  17. theorem OAI.SphericalPerceptronFreeEnergy.tailIntegral_oneTrial line 97
  18. theorem OAI.SphericalPerceptronFreeEnergy.entropy_oneTrial line 101
  19. instance OAI.SphericalPerceptronFreeEnergy.(instance at line 104) line 104
  20. instance OAI.SphericalPerceptronFreeEnergy.(instance at line 110) line 110
  21. lemma OAI.SphericalPerceptronFreeEnergy.continuous_patternField line 114
  22. lemma OAI.SphericalPerceptronFreeEnergy.continuous_hamiltonian line 125
  23. lemma OAI.SphericalPerceptronFreeEnergy.abs_hamiltonian_le line 132
  24. lemma OAI.SphericalPerceptronFreeEnergy.log_integral_exp_sub_le line 143
  25. lemma OAI.SphericalPerceptronFreeEnergy.abs_log_integral_exp_sub_le line 162
  26. lemma OAI.SphericalPerceptronFreeEnergy.abs_energy_le line 179
  27. lemma OAI.SphericalPerceptronFreeEnergy.integrable_partition line 185
  28. lemma OAI.SphericalPerceptronFreeEnergy.partition_bounds line 198
  29. lemma OAI.SphericalPerceptronFreeEnergy.partition_pos line 217
  30. lemma OAI.SphericalPerceptronFreeEnergy.continuous_partition line 222
  31. lemma OAI.SphericalPerceptronFreeEnergy.continuous_pressure line 241
  32. lemma OAI.SphericalPerceptronFreeEnergy.abs_pressure_le line 247
  33. lemma OAI.SphericalPerceptronFreeEnergy.integrable_pressure line 262
  34. lemma OAI.SphericalPerceptronFreeEnergy.continuous_integral_of_bounded line 276
  35. lemma OAI.SphericalPerceptronFreeEnergy.abs_integral_of_bounded line 291
  36. lemma OAI.SphericalPerceptronFreeEnergy.variance_prod_le line 297
  37. lemma OAI.SphericalPerceptronFreeEnergy.variance_le_of_oscillation line 337
  38. lemma OAI.SphericalPerceptronFreeEnergy.continuous_fin_cons line 350
  39. lemma OAI.SphericalPerceptronFreeEnergy.measurePreserving_fin_cons line 360
  40. lemma OAI.SphericalPerceptronFreeEnergy.measurableEmbedding_fin_cons line 368
  41. theorem OAI.SphericalPerceptronFreeEnergy.variance_pi_le_of_bounded_differences line 374