OAI/Probability/SKFluctuations/ScalarFiniteInvariant.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Scalar Finite Invariant.

  1. theorem OAI.SKFluctuations.Hierarchy.scalarClock_realJet_zero line 19
  2. theorem OAI.SKFluctuations.Hierarchy.scalarSourceJet_schedule_curvature_pos line 37
  3. theorem OAI.SKFluctuations.Hierarchy.scalarSourceJet_schedule_curvature_le_one line 45
  4. theorem OAI.SKFluctuations.Hierarchy.scalarClock_polynomialSigns line 53
  5. theorem OAI.SKFluctuations.Hierarchy.scalar_schedule_polynomialSigns line 108
  6. theorem OAI.SKFluctuations.Scalar.UniformSpatialTail.bounded_mul line 129
  7. theorem OAI.SKFluctuations.Scalar.third_barrier_source_nonpos line 140
  8. theorem OAI.SKFluctuations.Scalar.third_uniform_tail line 166
  9. theorem OAI.SKFluctuations.Scalar.third_barrier_evolve line 180
  10. theorem OAI.SKFluctuations.Scalar.PolynomialSigns.limit line 256
  11. theorem OAI.SKFluctuations.Hierarchy.scalarProfileJet_polynomialSigns line 285
  12. theorem OAI.SKFluctuations.Hierarchy.scalarSourceJet_schedule_gradient_zero line 304
  13. theorem OAI.SKFluctuations.Hierarchy.scalarSourceJet_schedule_gradient_nonneg line 311
  14. theorem OAI.SKFluctuations.Hierarchy.scalarClock_third_barrier line 317
  15. theorem OAI.SKFluctuations.Hierarchy.scalar_schedule_third_barrier line 354
  16. theorem OAI.SKFluctuations.Hierarchy.scalarProfileJet_third_barrier line 373
  17. theorem OAI.SKFluctuations.Hierarchy.scalarProfileJet_four_zero_upper line 384
  18. theorem OAI.SKFluctuations.Hierarchy.scalarProfileJet_four_zero_neg line 406
  19. theorem OAI.SKFluctuations.Scalar.jet_tendstoUniformly_of_limit line 420
  20. def OAI.SKFluctuations.Hierarchy.scalarClockCappedJets line 445
  21. theorem OAI.SKFluctuations.Hierarchy.scalarClockCappedJets_ordered line 455
  22. theorem OAI.SKFluctuations.Hierarchy.scalarClockCappedJets_zero_tendsto line 461
  23. theorem OAI.SKFluctuations.Hierarchy.scalarClockCappedJets_tendstoUniformly line 482
  24. theorem OAI.SKFluctuations.Hierarchy.scalarClockProfile_polynomialSigns line 498
  25. theorem OAI.SKFluctuations.Hierarchy.scalarClockProfile_relative_spin line 506
  26. theorem OAI.SKFluctuations.Hierarchy.scalarClockProfile_third_barrier line 515
  27. theorem OAI.SKFluctuations.Hierarchy.scalarClockProfile_relative_curvature line 525
  28. theorem OAI.SKFluctuations.Hierarchy.scalarProfileJet_window_tendsto line 553
  29. theorem OAI.SKFluctuations.Hierarchy.scalarProfileJet_window_continuous line 573
  30. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_spatial_continuous line 598
  31. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_F_continuous line 609
  32. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_square_continuous line 613
  33. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_square_bound line 617
  34. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_lipschitz line 624
  35. theorem OAI.SKFluctuations.Hierarchy.HeatJet.observedSquare_continuous line 627
  36. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_observedSquare_continuous line 638
  37. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_endpoint_le line 647