OAI/Probability/SKFluctuations/InvariantPropagation.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Invariant Propagation.

  1. structure OAI.SKFluctuations.Scalar.PolynomialSigns line 19
  2. theorem OAI.SKFluctuations.Scalar.PolynomialSigns.decrease line 25
  3. theorem OAI.SKFluctuations.Scalar.weightedP_tail line 44
  4. theorem OAI.SKFluctuations.Scalar.weightedQ_tail line 50
  5. theorem OAI.SKFluctuations.Scalar.weightedR_tail line 57
  6. theorem OAI.SKFluctuations.Scalar.polynomialSigns_evolve line 64
  7. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.sourceJet_sub line 191
  8. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.sourceJet_constant_replicate line 205
  9. theorem OAI.SKFluctuations.Hierarchy.scalarSourceJet_relative_spin line 224
  10. theorem OAI.SKFluctuations.Hierarchy.clockTest_sub_test_via_shiftedMean line 268
  11. def OAI.SKFluctuations.Hierarchy.HeatJet.ScalarStrong line 275
  12. theorem OAI.SKFluctuations.Hierarchy.HeatJet.ScalarStrong.evolve line 278
  13. theorem OAI.SKFluctuations.Hierarchy.scalar_schedule_strong line 295
  14. theorem OAI.SKFluctuations.Hierarchy.scalarSourceJet_relative_curvature line 308
  15. theorem OAI.SKFluctuations.Hierarchy.scalarSourceJet_bddSmooth_all line 336
  16. theorem OAI.SKFluctuations.Hierarchy.scalar_schedule_smoothG line 353
  17. theorem OAI.SKFluctuations.Hierarchy.scalar_schedule_smoothH line 367
  18. theorem OAI.SKFluctuations.Hierarchy.scalar_schedule_ordered_masses line 381
  19. def OAI.SKFluctuations.Hierarchy.clockPrepend line 394
  20. theorem OAI.SKFluctuations.Hierarchy.clockPrepend_ordered line 397
  21. theorem OAI.SKFluctuations.Hierarchy.scalarClock_realJet_eq_sourceJet line 402
  22. theorem OAI.SKFluctuations.Hierarchy.scalarSourceJet_schedule_parity line 419
  23. theorem OAI.SKFluctuations.Scalar.tangent_bound_of_monotone_derivative line 448
  24. theorem OAI.SKFluctuations.Scalar.spin_residual_tail line 464
  25. theorem OAI.SKFluctuations.Hierarchy.scalarSourceJet_schedule_gradient_monotone line 482
  26. theorem OAI.SKFluctuations.Hierarchy.scalarSourceJet_schedule_spin_tail line 490
  27. theorem OAI.SKFluctuations.Hierarchy.scalarSourceJet_schedule_jet_tail line 501
  28. theorem OAI.SKFluctuations.Hierarchy.scalarClock_realJet_uniform_tail line 511
  29. def OAI.SKFluctuations.Scalar.fifth line 541
  30. theorem OAI.SKFluctuations.Scalar.fourth_derivative line 543
  31. theorem OAI.SKFluctuations.Scalar.terminal_invariantP line 550
  32. theorem OAI.SKFluctuations.Scalar.terminal_invariantQ line 553
  33. theorem OAI.SKFluctuations.Scalar.terminal_invariantR line 556
  34. theorem OAI.SKFluctuations.Scalar.third_nonpos line 559
  35. theorem OAI.SKFluctuations.Hierarchy.scalar_nil_jet_two line 571
  36. theorem OAI.SKFluctuations.Hierarchy.scalar_nil_jet_three line 575
  37. theorem OAI.SKFluctuations.Hierarchy.scalar_nil_jet_four line 581
  38. theorem OAI.SKFluctuations.Hierarchy.scalar_nil_jet_five line 587
  39. theorem OAI.SKFluctuations.Hierarchy.scalar_nil_polynomialSigns line 593