OAI/Probability/SKFluctuations/CompletedFeatureKernel.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

Completed Feature Kernel.

  1. theorem OAI.SKFluctuations.sum_square_edges line 16
  2. theorem OAI.SKFluctuations.completedCovariance line 27
  3. abbrev OAI.SKFluctuations.Hierarchy.HamiltonianStep line 73
  4. def OAI.SKFluctuations.Hierarchy.hamiltonianHierarchy line 75
  5. def OAI.SKFluctuations.Hierarchy.hamiltonianHierarchyMean line 79
  6. theorem OAI.SKFluctuations.Hierarchy.hamiltonianHierarchy_measurable line 85
  7. theorem OAI.SKFluctuations.Hierarchy.hamiltonianHierarchyMean_measurable line 99
  8. def OAI.SKFluctuations.Hierarchy.featureLaw line 114
  9. def OAI.SKFluctuations.Hierarchy.featureSteps line 118
  10. theorem OAI.SKFluctuations.Hierarchy.featureLaw_integral line 122
  11. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchy_featureLaw line 127
  12. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyMean_featureLaw line 142
  13. theorem OAI.SKFluctuations.Hierarchy.hamiltonianHierarchyMean_jointMeasurable line 170
  14. def OAI.SKFluctuations.Hierarchy.hamiltonianPrefixTest line 191
  15. theorem OAI.SKFluctuations.Hierarchy.hamiltonianPrefixTest_measurable line 196
  16. theorem OAI.SKFluctuations.Hierarchy.prefixTest_featureLaw line 211
  17. def OAI.SKFluctuations.Hierarchy.hamiltonianPairTest line 232
  18. theorem OAI.SKFluctuations.Hierarchy.hamiltonianPairTest_measurable line 235
  19. theorem OAI.SKFluctuations.Hierarchy.stepPairMean_featureLaw line 240
  20. theorem OAI.SKFluctuations.Hierarchy.stepPairDisorder_featureLaw line 253
  21. theorem OAI.SKFluctuations.Hierarchy.stepPairDisorder_eq_of_featureLaws line 274
  22. def OAI.SKFluctuations.Hierarchy.splitHamiltonianSteps line 284
  23. theorem OAI.SKFluctuations.Hierarchy.featureSteps_split line 289
  24. theorem OAI.SKFluctuations.Hierarchy.stepPairMoment_eq_of_featureLaws line 304
  25. theorem OAI.SKFluctuations.Hierarchy.sampleFeatureSteps_eq line 317
  26. theorem OAI.SKFluctuations.Hierarchy.retainedPairSample_eq_of_featureLaws line 343
  27. theorem OAI.SKFluctuations.Hierarchy.pathPairMoment_eq_of_featureLaws line 353
  28. def OAI.SKFluctuations.completedPathClock line 377
  29. theorem OAI.SKFluctuations.completedPathClock_monotone line 380
  30. theorem OAI.SKFluctuations.ordered_completed_featureLaw line 387
  31. theorem OAI.SKFluctuations.ordered_completed_incrementLaw line 402
  32. theorem OAI.SKFluctuations.orderedPathPair_eq_completed line 412
  33. theorem OAI.SKFluctuations.physicalFieldDuration_take_coordinate line 432
  34. theorem OAI.SKFluctuations.splitClockSteps_take line 447
  35. theorem OAI.SKFluctuations.physicalFieldDuration_split line 454
  36. theorem OAI.SKFluctuations.sampledFieldDuration line 462
  37. theorem OAI.SKFluctuations.sampledFieldClock_aligned line 476
  38. theorem OAI.SKFluctuations.pathMassDifferences_eq_cutMass line 498
  39. theorem OAI.SKFluctuations.physicalCutMass_sampleClockSteps line 517
  40. theorem OAI.SKFluctuations.sampledFieldDuration_index line 529
  41. def OAI.SKFluctuations.Hierarchy.cutPredecessor line 553
  42. def OAI.SKFluctuations.Hierarchy.cutIncrement line 557
  43. theorem OAI.SKFluctuations.Hierarchy.cutIncrement_zero line 560
  44. theorem OAI.SKFluctuations.Hierarchy.cutIncrement_succ line 563
  45. theorem OAI.SKFluctuations.Hierarchy.weightedPathIncrements_eq_sum line 567
  46. theorem OAI.SKFluctuations.Hierarchy.sum_cutIncrement line 576
  47. theorem OAI.SKFluctuations.Hierarchy.dot_cutIncrement line 585