OAI/Probability/SphericalField/Cascade/LogFluctuations.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptron.cascadeTotal_log_memLp_two line 17
  2. def OAI.SphericalPerceptron.decoratedWeightedTotalE line 37
  3. lemma OAI.SphericalPerceptron.decoratedWeightedTotalE_transform line 45
  4. lemma OAI.SphericalPerceptron.decoratedWeightedTotalE_measurable line 72
  5. lemma OAI.SphericalPerceptron.decoratedWeightedTotalE_counting line 81
  6. def OAI.SphericalPerceptron.decoratedWeightedTotal line 96
  7. lemma OAI.SphericalPerceptron.decoratedWeightedTotal_transform line 100
  8. lemma OAI.SphericalPerceptron.decoratedWeightedTotal_identDistrib line 106
  9. theorem OAI.SphericalPerceptron.decoratedCascade_log_identity line 124
  10. lemma OAI.SphericalPerceptron.decoratedCascade_log_difference_memLp line 159
  11. def OAI.SphericalPerceptron.fractionalLogMoment line 177
  12. lemma OAI.SphericalPerceptron.fractionalLogMoment_measurable line 181
  13. lemma OAI.SphericalPerceptron.bounded_fractional_exp_integrable line 186
  14. lemma OAI.SphericalPerceptron.fractionalLogMoment_abs_le line 195
  15. lemma OAI.SphericalPerceptron.fractionalLogMoment_centered line 223