OAI/Probability/SKFluctuations/RootedIncrements.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

Rooted Increments.

  1. def OAI.SKFluctuations.Hierarchy.rootedIncrements line 20
  2. def OAI.SKFluctuations.Hierarchy.rootedTransitions line 24
  3. def OAI.SKFluctuations.Hierarchy.rootedJointDensity line 31
  4. theorem OAI.SKFluctuations.Hierarchy.rootedJointDensity_factor line 37
  5. theorem OAI.SKFluctuations.Hierarchy.rootedJointDensity_normalized line 48
  6. theorem OAI.SKFluctuations.Hierarchy.rootedJointDensity_telescope line 65
  7. def OAI.SKFluctuations.Hierarchy.flattenDrivers line 83
  8. theorem OAI.SKFluctuations.Hierarchy.flattenDrivers_apply line 94
  9. theorem OAI.SKFluctuations.Hierarchy.flattenDrivers_symm_apply line 98
  10. theorem OAI.SKFluctuations.Hierarchy.flattenDrivers_measure line 101
  11. theorem OAI.SKFluctuations.Hierarchy.flattenDrivers_standard line 127
  12. theorem OAI.SKFluctuations.Hierarchy.flattenDrivers_volume line 132
  13. def OAI.SKFluctuations.Hierarchy.pathFrames line 145
  14. def OAI.SKFluctuations.Hierarchy.pathMassDifferences line 156
  15. theorem OAI.SKFluctuations.Hierarchy.pathMassDifferences_nonneg line 161
  16. theorem OAI.SKFluctuations.Hierarchy.sum_pathMassDifferences line 170
  17. theorem OAI.SKFluctuations.Hierarchy.pathFrames_cost line 182
  18. def OAI.SKFluctuations.Hierarchy.pathEndMap line 199
  19. theorem OAI.SKFluctuations.Hierarchy.pathEndMap_apply line 207
  20. theorem OAI.SKFluctuations.Hierarchy.pathFrames_potential line 220
  21. theorem OAI.SKFluctuations.Hierarchy.withDensity_equiv line 240
  22. theorem OAI.SKFluctuations.Hierarchy.gaussian_tilt_potentialLaw line 256
  23. def OAI.SKFluctuations.Hierarchy.flatLevelProjection line 299
  24. theorem OAI.SKFluctuations.Hierarchy.flatLevelProjection_apply line 304
  25. def OAI.SKFluctuations.Hierarchy.flatRootFrames line 308
  26. def OAI.SKFluctuations.Hierarchy.flatTerminalFeature line 315
  27. def OAI.SKFluctuations.Hierarchy.flatPinPotential line 321
  28. def OAI.SKFluctuations.Hierarchy.flatPlantedPinLaw line 330
  29. theorem OAI.SKFluctuations.Hierarchy.flatPin_likelihood line 336
  30. theorem OAI.SKFluctuations.Hierarchy.flatPinLaw_eq line 351
  31. theorem OAI.SKFluctuations.Hierarchy.flatPinLaw_normalized line 366
  32. theorem OAI.SKFluctuations.Hierarchy.flatPlanted_total_mass line 385
  33. def OAI.SKFluctuations.flatSKGauge line 406
  34. theorem OAI.SKFluctuations.scaleDriver_featureGauge line 410
  35. theorem OAI.SKFluctuations.flatLevelProjection_gauge line 417
  36. theorem OAI.SKFluctuations.pathEndMap_gauge line 424
  37. theorem OAI.SKFluctuations.pathFrames_gauge line 442
  38. theorem OAI.SKFluctuations.flatRootFrames_gauge line 487
  39. theorem OAI.SKFluctuations.flatTerminalFeature_gauge line 500
  40. theorem OAI.SKFluctuations.driverQuadratic_flatSKGauge line 513
  41. theorem OAI.SKFluctuations.flatPinPotential_gauge line 525
  42. theorem OAI.SKFluctuations.flatPinned_joint_test_gauge line 539
  43. abbrev OAI.SKFluctuations.actualPinFrames line 569
  44. abbrev OAI.SKFluctuations.actualPinPotential line 574
  45. def OAI.SKFluctuations.actualPinnedPair line 579
  46. theorem OAI.SKFluctuations.actualPinnedPair_continuous line 586
  47. def OAI.SKFluctuations.actualPlantedPairLaw line 594
  48. theorem OAI.SKFluctuations.actualPinnedPair_map_eq line 601
  49. theorem OAI.SKFluctuations.actualPlantedPairLaw_eq_pin line 629
  50. theorem OAI.SKFluctuations.actualPlantedPairLaw_probability line 658
  51. theorem OAI.SKFluctuations.actual_planted_variance_le line 669
  52. theorem OAI.SKFluctuations.actual_planted_centered_moment_le line 683