OAI/Probability/SKFluctuations/MapCLM.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Map C L M.

  1. theorem OAI.SKFluctuations.Hierarchy.ExponentialIncrement.mapCLM line 22
  2. theorem OAI.SKFluctuations.Hierarchy.BddSmooth.affine_zero line 36
  3. def OAI.SKFluctuations.Hierarchy.linearGaussian line 45
  4. instance OAI.SKFluctuations.Hierarchy.linearGaussian_probability line 48
  5. theorem OAI.SKFluctuations.Hierarchy.exponentialIncrement_linearGaussian line 53
  6. def OAI.SKFluctuations.Hierarchy.linearClockContinuation line 57
  7. def OAI.SKFluctuations.Hierarchy.linearClockTest line 60
  8. def OAI.SKFluctuations.Hierarchy.linearClockRoot line 63
  9. theorem OAI.SKFluctuations.Hierarchy.linearClockContinuation_eq line 66
  10. theorem OAI.SKFluctuations.Hierarchy.linearClockTest_eq line 76
  11. theorem OAI.SKFluctuations.Hierarchy.linearClockRoot_eq line 90
  12. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyMean_linear_components line 108
  13. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchy_linear_feature_derivatives line 126
  14. def OAI.SKFluctuations.Hierarchy.linearFeaturePenalty line 147
  15. theorem OAI.SKFluctuations.Hierarchy.linearFeaturePenalty_smooth line 151
  16. theorem OAI.SKFluctuations.Hierarchy.linear_feature_trace_telescope line 157
  17. def OAI.SKFluctuations.Hierarchy.linearClockDerivative line 181
  18. theorem OAI.SKFluctuations.Hierarchy.parametric_linear_clock line 188
  19. theorem OAI.SKFluctuations.Hierarchy.parametric_continuous_linear_clock line 248
  20. theorem OAI.SKFluctuations.Hierarchy.linearClockDerivative_feature_trace line 276
  21. theorem OAI.SKFluctuations.Hierarchy.rootedHierarchy_linear_clock line 305
  22. theorem OAI.SKFluctuations.Hierarchy.rootedHierarchy_corrected_linear_clock line 327
  23. theorem OAI.SKFluctuations.Hierarchy.rootedHierarchy_corrected_linear_clock_nonneg line 362
  24. theorem OAI.SKFluctuations.Hierarchy.hierarchyPenalty_upper line 399
  25. theorem OAI.SKFluctuations.Hierarchy.linearFeaturePenalty_bounds line 414
  26. theorem OAI.SKFluctuations.Hierarchy.linearFeaturePenalty_abs_le line 434
  27. theorem OAI.SKFluctuations.Hierarchy.prefixTest_abs_le line 448
  28. theorem OAI.SKFluctuations.Hierarchy.zeroContinuation_abs_le line 462
  29. theorem OAI.SKFluctuations.Hierarchy.BddSmooth.prod line 477
  30. inductive OAI.SKFluctuations.Hierarchy.ProductTree line 490
  31. def OAI.SKFluctuations.Hierarchy.ProductTree.leaves line 495
  32. def OAI.SKFluctuations.Hierarchy.ProductTree.mean line 500
  33. def OAI.SKFluctuations.Hierarchy.ProductTree.row line 509
  34. theorem OAI.SKFluctuations.Hierarchy.ProductTree.mean_smooth line 521
  35. theorem OAI.SKFluctuations.Hierarchy.ProductTree.row_smooth line 532
  36. theorem OAI.SKFluctuations.Hierarchy.sum_product_fork line 554
  37. theorem OAI.SKFluctuations.Hierarchy.ProductTree.hasDerivAt_mean line 569