OAI/Probability/Perceptron/Cascade/DecoratedWeightedTotal.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.decoratedWeightedTotalE_measurable line 15
  2. lemma OAI.SphericalPerceptronFreeEnergy.decoratedWeightedTotalE_counting line 24
  3. def OAI.SphericalPerceptronFreeEnergy.decoratedWeightedTotal line 39
  4. lemma OAI.SphericalPerceptronFreeEnergy.decoratedWeightedTotal_transform line 43
  5. lemma OAI.SphericalPerceptronFreeEnergy.decoratedWeightedTotal_identDistrib line 49
  6. theorem OAI.SphericalPerceptronFreeEnergy.decoratedCascade_log_identity line 67
  7. lemma OAI.SphericalPerceptronFreeEnergy.decoratedCascade_log_difference_memLp line 102
  8. def OAI.SphericalPerceptronFreeEnergy.fractionalLogMoment line 120
  9. lemma OAI.SphericalPerceptronFreeEnergy.fractionalLogMoment_measurable line 124
  10. lemma OAI.SphericalPerceptronFreeEnergy.bounded_fractional_exp_integrable line 129
  11. lemma OAI.SphericalPerceptronFreeEnergy.fractionalLogMoment_abs_le line 138
  12. lemma OAI.SphericalPerceptronFreeEnergy.fractionalLogMoment_centered line 166
  13. def OAI.SphericalPerceptronFreeEnergy.finiteCascadeLogRecursion line 187
  14. lemma OAI.SphericalPerceptronFreeEnergy.finiteCascadeLogRecursion_measurable line 194
  15. lemma OAI.SphericalPerceptronFreeEnergy.finiteCascadeLogRecursion_abs_le line 202
  16. def OAI.SphericalPerceptronFreeEnergy.finiteCascadeShifts line 213
  17. lemma OAI.SphericalPerceptronFreeEnergy.finiteCascadeShifts_measurable line 222
  18. lemma OAI.SphericalPerceptronFreeEnergy.finiteCascadeShifts_normalized line 234
  19. def OAI.SphericalPerceptronFreeEnergy.decoratedTerminalTotalE line 253
  20. lemma OAI.SphericalPerceptronFreeEnergy.decoratedTerminalTotalE_telescoping line 259
  21. lemma OAI.SphericalPerceptronFreeEnergy.decoratedTerminalTotalE_zero line 286
  22. def OAI.SphericalPerceptronFreeEnergy.decoratedTerminalTotal line 299
  23. lemma OAI.SphericalPerceptronFreeEnergy.decoratedTerminalTotal_telescoping line 303
  24. lemma OAI.SphericalPerceptronFreeEnergy.decoratedTerminalTotal_zero line 312
  25. theorem OAI.SphericalPerceptronFreeEnergy.finiteCascade_terminal_log_recursion line 317
  26. def OAI.SphericalPerceptronFreeEnergy.finiteCascadeFractionalIntegrable line 331
  27. lemma OAI.SphericalPerceptronFreeEnergy.finiteCascadeFractionalIntegrable_of_bounded line 339
  28. lemma OAI.SphericalPerceptronFreeEnergy.finiteCascadeShifts_normalized_of_fractional line 355
  29. theorem OAI.SphericalPerceptronFreeEnergy.finiteCascade_terminal_log_recursion_of_fractional line 371
  30. lemma OAI.SphericalPerceptronFreeEnergy.stableIntensity_descendant_transform_marked line 385
  31. lemma OAI.SphericalPerceptronFreeEnergy.stablePoisson_descendant_transform_marked line 408