OAI/Probability/SphericalField/Cascade/Recursion.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptron.finiteCascadeLogRecursion line 17
  2. lemma OAI.SphericalPerceptron.finiteCascadeLogRecursion_measurable line 24
  3. lemma OAI.SphericalPerceptron.finiteCascadeLogRecursion_abs_le line 32
  4. def OAI.SphericalPerceptron.finiteCascadeShifts line 43
  5. lemma OAI.SphericalPerceptron.finiteCascadeShifts_measurable line 52
  6. lemma OAI.SphericalPerceptron.finiteCascadeShifts_normalized line 64
  7. lemma OAI.SphericalPerceptron.decoratedTerminalTotalE_telescoping line 83
  8. lemma OAI.SphericalPerceptron.decoratedTerminalTotalE_zero line 110
  9. lemma OAI.SphericalPerceptron.decoratedTerminalTotal_telescoping line 123
  10. lemma OAI.SphericalPerceptron.decoratedTerminalTotal_zero line 132
  11. theorem OAI.SphericalPerceptron.finiteCascade_terminal_log_recursion line 137
  12. def OAI.SphericalPerceptron.finiteCascadeFractionalIntegrable line 151
  13. lemma OAI.SphericalPerceptron.finiteCascadeFractionalIntegrable_of_bounded line 159
  14. lemma OAI.SphericalPerceptron.finiteCascadeShifts_normalized_of_fractional line 175
  15. theorem OAI.SphericalPerceptron.finiteCascade_terminal_log_recursion_of_fractional line 191
  16. lemma OAI.SphericalPerceptron.stableIntensity_descendant_transform_marked line 205