OAI/Probability/SphericalField/Entropy/StepDual.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SphericalPerceptron.finite_weighted_increment_identityline 13 - lemma
OAI.SphericalPerceptron.weightedStepTail_rootline 38 - lemma
OAI.SphericalPerceptron.weightedStepTail_cutline 45 - lemma
OAI.SphericalPerceptron.finite_sum_successive_differencesline 61 - lemma
OAI.SphericalPerceptron.stationary_field_shift_identityline 68 - lemma
OAI.SphericalPerceptron.stepFieldIncrement_sqline 117 - theorem
OAI.SphericalPerceptron.finiteSphericalFieldValue_stationaryline 127