OAI/Probability/Perceptron/Variational/QuantileUpperTail.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.unit_valued_integrable line 13
  2. lemma OAI.SphericalPerceptronFreeEnergy.quantile_stoploss_integrable line 22
  3. lemma OAI.SphericalPerceptronFreeEnergy.time_tail_constant line 27
  4. lemma OAI.SphericalPerceptronFreeEnergy.upper_tail_le_stoploss line 33
  5. lemma OAI.SphericalPerceptronFreeEnergy.upper_tail_eq_stoploss line 52
  6. theorem OAI.SphericalPerceptronFreeEnergy.upper_tail_order_of_stoploss line 66
  7. lemma OAI.SphericalPerceptronFreeEnergy.boundedQuantile_stoploss line 73
  8. def OAI.SphericalPerceptronFreeEnergy.uniformQuantileLower line 78
  9. def OAI.SphericalPerceptronFreeEnergy.uniformQuantileUpper line 80
  10. def OAI.SphericalPerceptronFreeEnergy.sampleQuantileLower line 82
  11. def OAI.SphericalPerceptronFreeEnergy.sampleQuantileUpper line 84
  12. lemma OAI.SphericalPerceptronFreeEnergy.uniformQuantileLower_mono line 87
  13. lemma OAI.SphericalPerceptronFreeEnergy.uniformQuantileUpper_mono line 91
  14. lemma OAI.SphericalPerceptronFreeEnergy.sampleQuantileLower_mono line 95
  15. lemma OAI.SphericalPerceptronFreeEnergy.sampleQuantileUpper_mono line 98
  16. lemma OAI.SphericalPerceptronFreeEnergy.sampleQuantile_bracket line 101
  17. lemma OAI.SphericalPerceptronFreeEnergy.sampleQuantile_gap_integral line 105
  18. lemma OAI.SphericalPerceptronFreeEnergy.sampleQuantileLower_L1 line 116
  19. lemma OAI.SphericalPerceptronFreeEnergy.sampleQuantileUpper_L1 line 133
  20. lemma OAI.SphericalPerceptronFreeEnergy.uniformQuantileWeights_nonneg line 149
  21. lemma OAI.SphericalPerceptronFreeEnergy.uniformQuantileWeights_sum line 152
  22. lemma OAI.SphericalPerceptronFreeEnergy.sampleQuantile_trial line 157