OAI/Probability/SphericalField/Cascade/Blocks.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptron.markedBlockProbability line 28
  2. lemma OAI.SphericalPerceptron.markedBlockProbability_measurable line 35
  3. lemma OAI.SphericalPerceptron.markedBlockProbability_moment line 55
  4. lemma OAI.SphericalPerceptron.markedBlockProbability_ordered line 111
  5. lemma OAI.SphericalPerceptron.markedTotalBiasedLaw_absolutelyContinuous line 125
  6. lemma OAI.SphericalPerceptron.markedBlockProbability_factor line 129
  7. lemma OAI.SphericalPerceptron.markedStableTotal_map_shift line 161
  8. def OAI.SphericalPerceptron.weightedTotalBiasedLaw line 167
  9. lemma OAI.SphericalPerceptron.weightedTotalBiasedLaw_shift line 172
  10. lemma OAI.SphericalPerceptron.weightedTotalBiasedLaw_add_const line 189
  11. lemma OAI.SphericalPerceptron.weightedBranchMass_map line 206
  12. def OAI.SphericalPerceptron.exponentialMarkTilt line 215
  13. def OAI.SphericalPerceptron.centeredLogMark line 218
  14. lemma OAI.SphericalPerceptron.centeredLogMark_measurable line 222
  15. lemma OAI.SphericalPerceptron.exponentialMarkTilt_probability line 226
  16. lemma OAI.SphericalPerceptron.centeredLogMark_density line 237
  17. lemma OAI.SphericalPerceptron.weightedTotalBiasedLaw_centered line 258
  18. lemma OAI.SphericalPerceptron.weightedRootBlock_factor line 265