OAI/Probability/SKFluctuations/LinearClockMassDifference.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Linear Clock Mass Difference.

  1. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.linearClock_mass_difference line 20
  2. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.linearPotential_mass_difference line 36
  3. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.clockTest_atomic_any_mass line 50
  4. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.atomic_mass_difference line 71
  5. theorem OAI.SKFluctuations.Hierarchy.abs_sub_le_of_bounded_derivative line 94
  6. theorem OAI.SKFluctuations.Hierarchy.HeatJet.potentialSplit_stability line 109
  7. theorem OAI.SKFluctuations.Hierarchy.HeatJet.massSplit_stability line 120
  8. theorem OAI.SKFluctuations.Hierarchy.linearClockContinuation_affine line 140
  9. theorem OAI.SKFluctuations.Hierarchy.linearClockTest_affine line 147
  10. def OAI.SKFluctuations.Hierarchy.linearPotentialSplit line 154
  11. def OAI.SKFluctuations.Hierarchy.linearTestSplit line 158
  12. theorem OAI.SKFluctuations.Hierarchy.linearPotentialSplit_eq line 163
  13. theorem OAI.SKFluctuations.Hierarchy.linearTestSplit_eq line 177
  14. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.linearTestSplit_stability line 208
  15. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.linearPotentialSplit_stability line 229
  16. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.linearTestSplit_smooth0 line 253
  17. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.linearTestSplit_atomic line 264
  18. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.atomic_split_probability line 288
  19. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.atomic_split_stability line 315
  20. theorem OAI.SKFluctuations.Hierarchy.BoundaryTree.actual_mass_change line 344
  21. theorem OAI.SKFluctuations.Hierarchy.BoundaryTree.actual_boundary_move line 387
  22. theorem OAI.SKFluctuations.Hierarchy.shiftedContinuation_productGaussian_add line 426
  23. theorem OAI.SKFluctuations.Hierarchy.shiftedContinuation_productGaussian_comm line 446
  24. theorem OAI.SKFluctuations.Hierarchy.shiftedMean_productGaussian_add line 457
  25. def OAI.SKFluctuations.Hierarchy.diagonalDriver line 494
  26. theorem OAI.SKFluctuations.Hierarchy.diagonalDriver_apply line 498
  27. theorem OAI.SKFluctuations.Hierarchy.linearGaussian_diagonal line 501
  28. theorem OAI.SKFluctuations.Hierarchy.diagonalDriver_single line 516
  29. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchy_diagonal_mass_difference line 527
  30. theorem OAI.SKFluctuations.Hierarchy.shiftedContinuation_mono line 551
  31. theorem OAI.SKFluctuations.Hierarchy.shiftedContinuation_add_const line 560
  32. theorem OAI.SKFluctuations.Hierarchy.shiftedContinuation_abs_sub_le line 569
  33. theorem OAI.SKFluctuations.Hierarchy.clockContinuation_abs_sub_le line 586
  34. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchy_covariance_transfer line 604