OAI/Probability/SKFluctuations/ClockTestAbsLeMul.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Clock Test Abs Le Mul.

  1. theorem OAI.SKFluctuations.Hierarchy.clockTest_abs_le_mul line 19
  2. theorem OAI.SKFluctuations.Hierarchy.clockTest_nonneg line 26
  3. theorem OAI.SKFluctuations.Hierarchy.clockGradient_relative_abs_le line 32
  4. theorem OAI.SKFluctuations.Hierarchy.HeatJet.massSplitResponse_relative_abs_le line 56
  5. theorem OAI.SKFluctuations.Hierarchy.HeatJet.massSplit_exp_comparison line 115
  6. theorem OAI.SKFluctuations.Hierarchy.replicaFeatureJet_A₁_relative_abs_le line 135
  7. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.linearTestSplit_exp_comparison line 152
  8. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.linearClock_mass_relative line 180
  9. theorem OAI.SKFluctuations.Hierarchy.BoundaryTree.actual_mass_relative line 202
  10. theorem OAI.SKFluctuations.Hierarchy.ClockTree.atomicHead_mass_close line 241
  11. theorem OAI.SKFluctuations.Hierarchy.ClockTree.atomicHead_transfer_close line 270
  12. theorem OAI.SKFluctuations.Hierarchy.BoundaryTree.head_transfer_close line 285
  13. def OAI.SKFluctuations.Hierarchy.prependClock line 341
  14. theorem OAI.SKFluctuations.Hierarchy.ClockTree.step_head_transfer line 345
  15. theorem OAI.SKFluctuations.Hierarchy.ClockTree.local_boundary_transfer line 372
  16. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchy_local_boundary_transfer line 420
  17. theorem OAI.SKFluctuations.Hierarchy.ClockTree.step_head_close line 438
  18. theorem OAI.SKFluctuations.Hierarchy.ClockTree.local_boundary_close line 465
  19. theorem OAI.SKFluctuations.Hierarchy.BoundaryTree.budget_nonneg line 510
  20. theorem OAI.SKFluctuations.Hierarchy.BoundaryTree.budget_quadratic line 517
  21. theorem OAI.SKFluctuations.Hierarchy.ClockTree.cut_budget_one line 533
  22. theorem OAI.SKFluctuations.Hierarchy.ClockTree.cut_budget_forksAt line 539
  23. theorem OAI.SKFluctuations.Hierarchy.ClockTree.cut_budget_quadratic_forks line 568
  24. theorem OAI.SKFluctuations.Hierarchy.ClockTree.cut_boundary_transfer line 586