OAI/Probability/SphericalField/Perceptron/TimeLaw.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.SphericalPerceptron.(instance at line 16) line 16
  2. instance OAI.SphericalPerceptron.(instance at line 20) line 20
  3. theorem OAI.SphericalPerceptron.progressive_zero line 24
  4. theorem OAI.SphericalPerceptron.controlCost_zero line 29
  5. theorem OAI.SphericalPerceptron.controlPayoff_zero line 33
  6. theorem OAI.SphericalPerceptron.abs_integral_reward_le line 37
  7. theorem OAI.SphericalPerceptron.controlPayoff_le_norm line 45
  8. theorem OAI.SphericalPerceptron.controlPayoffs_nonempty line 54
  9. theorem OAI.SphericalPerceptron.controlPayoffs_bddAbove line 59
  10. theorem OAI.SphericalPerceptron.controlValue_le_norm line 67
  11. theorem OAI.SphericalPerceptron.zero_payoff_le_controlValue line 73
  12. theorem OAI.SphericalPerceptron.neg_norm_le_controlValue line 79
  13. theorem OAI.SphericalPerceptron.abs_controlValue_le line 84
  14. def OAI.SphericalPerceptron.oneTrial line 88
  15. theorem OAI.SphericalPerceptron.oneTrial_apply line 95
  16. theorem OAI.SphericalPerceptron.tailIntegral_oneTrial line 97
  17. theorem OAI.SphericalPerceptron.entropy_oneTrial line 101
  18. instance OAI.SphericalPerceptron.(instance at line 104) line 104
  19. instance OAI.SphericalPerceptron.(instance at line 110) line 110
  20. lemma OAI.SphericalPerceptron.continuous_patternField line 117
  21. lemma OAI.SphericalPerceptron.continuous_hamiltonian line 128
  22. lemma OAI.SphericalPerceptron.abs_hamiltonian_le line 135