OAI/Probability/SphericalField/Entropy/Trials.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptron.trial_integrable line 22
  2. lemma OAI.SphericalPerceptron.tailIntegral_mono line 28
  3. lemma OAI.SphericalPerceptron.entropy_antitone line 32
  4. def OAI.SphericalPerceptron.upperRoundedTrial line 38
  5. lemma OAI.SphericalPerceptron.le_upperRoundedTrial line 54
  6. lemma OAI.SphericalPerceptron.upperRoundedTrial_sub_le line 58
  7. lemma OAI.SphericalPerceptron.upperRoundedTrial_finite_range line 67
  8. def OAI.SphericalPerceptron.terminalTrial line 74
  9. lemma OAI.SphericalPerceptron.le_terminalTrial line 88
  10. lemma OAI.SphericalPerceptron.terminalTrial_finite_range line 92
  11. lemma OAI.SphericalPerceptron.terminalTrial_tail line 101
  12. lemma OAI.SphericalPerceptron.tailIntegral_antitone line 109
  13. lemma OAI.SphericalPerceptron.terminalTrial_entropy_finite line 115
  14. lemma OAI.SphericalPerceptron.terminalTrial_L1_le line 136
  15. lemma OAI.SphericalPerceptron.upperRoundedTrial_L1_le line 154
  16. lemma OAI.SphericalPerceptron.exists_finite_terminal_trial_approx line 165