OAI/Probability/SKFluctuations/ClockPairForkLedger.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Clock Pair Fork Ledger.

  1. def OAI.SKFluctuations.Hierarchy.ClockTree.pairAbsSum line 19
  2. theorem OAI.SKFluctuations.Hierarchy.ClockTree.pairAbsSum_mono line 24
  3. theorem OAI.SKFluctuations.Hierarchy.ClockTree.pairAbsSum_const_mul line 35
  4. theorem OAI.SKFluctuations.Hierarchy.ClockTree.pairAbsSum_add line 40
  5. theorem OAI.SKFluctuations.Hierarchy.ClockTree.pairAbsSum_nonneg line 45
  6. theorem OAI.SKFluctuations.Hierarchy.ClockTree.abs_list_sum_le line 53
  7. theorem OAI.SKFluctuations.Hierarchy.ClockTree.signedPair_abs_le_pairAbsSum line 59
  8. theorem OAI.SKFluctuations.Hierarchy.ClockTree.pairAbsSum_constant_le line 72
  9. def OAI.SKFluctuations.Hierarchy.ClockTree.pairForkVariation line 90
  10. theorem OAI.SKFluctuations.Hierarchy.ClockTree.pairForkVariation_nonneg line 92
  11. theorem OAI.SKFluctuations.Hierarchy.ClockTree.pairAbsSum_forkBudget_le line 97
  12. theorem OAI.SKFluctuations.weighted_holder line 126
  13. theorem OAI.SKFluctuations.list_weighted_holder line 158
  14. theorem OAI.SKFluctuations.Hierarchy.ClockTree.pairAbsSum_holder line 185
  15. def OAI.SKFluctuations.Hierarchy.ClockTree.errorJetVariation line 225
  16. theorem OAI.SKFluctuations.Hierarchy.ClockTree.errorJetVariation_nonneg line 229
  17. theorem OAI.SKFluctuations.Hierarchy.ClockTree.rootProfileJets_cons_abs_le line 236
  18. theorem OAI.SKFluctuations.Hierarchy.ClockTree.rootProfileJets_oneError_abs_le line 252
  19. def OAI.SKFluctuations.Hierarchy.ClockTree.rootAbsProfileJets line 339
  20. theorem OAI.SKFluctuations.Hierarchy.ClockTree.rootAbsProfileJets_nonneg line 347
  21. theorem OAI.SKFluctuations.Hierarchy.ClockTree.rootProfileJets_le_absoluteLedger line 357
  22. theorem OAI.SKFluctuations.Hierarchy.ClockTree.profilePairTest_mul line 370
  23. theorem OAI.SKFluctuations.Hierarchy.ClockTree.profilePairTest_abs_rpow line 380
  24. theorem OAI.SKFluctuations.Hierarchy.ClockTree.rootAbsProfileJets_holder line 390
  25. def OAI.SKFluctuations.Hierarchy.ClockTree.absJetVariation line 435
  26. theorem OAI.SKFluctuations.Hierarchy.ClockTree.absJetVariation_nonneg line 439
  27. theorem OAI.SKFluctuations.Hierarchy.ClockTree.rootAbsProfileJets_relative_le line 446
  28. def OAI.SKFluctuations.Hierarchy.ClockTree.absErrorJetVariation line 487
  29. theorem OAI.SKFluctuations.Hierarchy.ClockTree.absErrorJetVariation_nonneg line 491
  30. theorem OAI.SKFluctuations.Hierarchy.ClockTree.rootAbsProfileJets_oneError_le line 498
  31. def OAI.SKFluctuations.Hierarchy.ClockTree.edgeDensity line 586
  32. theorem OAI.SKFluctuations.Hierarchy.ClockTree.edgeDensity_integrable line 591
  33. theorem OAI.SKFluctuations.Hierarchy.ClockTree.edgeDensity_integral line 600
  34. theorem OAI.SKFluctuations.Hierarchy.ClockTree.edgeDensity_nonneg line 614
  35. theorem OAI.SKFluctuations.Hierarchy.ClockTree.edgeBudget_le_integral line 624
  36. theorem OAI.SKFluctuations.Hierarchy.ClockTree.forkLedger_integral_le line 634