OAI/Probability/SKFluctuations/ClockRootMarginal.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Clock Root Marginal.

  1. theorem OAI.SKFluctuations.Hierarchy.ClockTree.markedAttach_preserves line 20
  2. theorem OAI.SKFluctuations.Hierarchy.ClockTree.rootExpect_integrable line 34
  3. theorem OAI.SKFluctuations.Hierarchy.ClockTree.rootExpect_mono line 45
  4. theorem OAI.SKFluctuations.Hierarchy.ClockTree.rootExpect_const_mul line 60
  5. theorem OAI.SKFluctuations.Hierarchy.ClockTree.rootExpect_nonneg line 67
  6. theorem OAI.SKFluctuations.Hierarchy.ClockTree.abs_rootExpect_le line 80
  7. theorem OAI.SKFluctuations.Hierarchy.ClockTree.markedAttach_rootPreserves line 94
  8. theorem OAI.SKFluctuations.Hierarchy.ClockTree.profilePairTest_root_abs_le line 114
  9. theorem OAI.SKFluctuations.Hierarchy.ClockTree.rootProfileJets_relative_abs_le line 136
  10. def OAI.SKFluctuations.Hierarchy.ClockTree.disorderProfileJets line 181
  11. theorem OAI.SKFluctuations.Hierarchy.ClockTree.disorderProfileJets_reindex line 190
  12. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.coordinateProfile_reindex line 202
  13. theorem OAI.SKFluctuations.Hierarchy.ClockTree.rootExpect_eq_disorderExpect line 215
  14. theorem OAI.SKFluctuations.Hierarchy.ClockTree.rootProfileJets_eq_disorderProfileJets line 226
  15. theorem OAI.SKFluctuations.Hierarchy.ClockTree.iteratedDeriv_disorderProfileJets line 237
  16. theorem OAI.SKFluctuations.Hierarchy.ClockTree.iteratedDeriv_finiteProfileJets line 279
  17. theorem OAI.SKFluctuations.Hierarchy.ClockTree.disorderProfileJets_abs_le line 306
  18. theorem OAI.SKFluctuations.Hierarchy.ClockTree.disorderProfileJets_relative_abs_le line 326
  19. theorem OAI.SKFluctuations.Hierarchy.continuous_listSum line 354
  20. theorem OAI.SKFluctuations.Hierarchy.ClockTree.disorderExpect_continuous line 367
  21. theorem OAI.SKFluctuations.Hierarchy.ClockTree.disorderProfileJets_continuous line 396
  22. theorem OAI.SKFluctuations.Hierarchy.ClockTree.hasDerivAt_finiteProfileJets line 425
  23. theorem OAI.SKFluctuations.Cavity.cutLowJet_eq_iteratedDeriv line 464
  24. theorem OAI.SKFluctuations.Cavity.cutLowJet_eq_profileJets line 482
  25. theorem OAI.SKFluctuations.Hierarchy.ClockTree.expect_fork line 522
  26. theorem OAI.SKFluctuations.Hierarchy.ClockTree.expect_step line 531
  27. theorem OAI.SKFluctuations.Hierarchy.ClockTree.expect_const line 547
  28. def OAI.SKFluctuations.Hierarchy.ClockTree.singleMean line 555
  29. theorem OAI.SKFluctuations.Hierarchy.ClockTree.singleMean_step line 559
  30. theorem OAI.SKFluctuations.Hierarchy.ClockTree.expect_atSlot line 570