OAI/Probability/SKFluctuations/ScalarSlopeInvariant.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

Scalar Slope Invariant.

  1. def OAI.SKFluctuations.Hierarchy.scalarSlopeJ line 19
  2. def OAI.SKFluctuations.Hierarchy.scalarSlopeJ₁ line 22
  3. def OAI.SKFluctuations.Hierarchy.scalarSlopeZ line 28
  4. theorem OAI.SKFluctuations.Hierarchy.scalarSlopeJ_eq_quotient line 31
  5. theorem OAI.SKFluctuations.Hierarchy.scalarSlopeJ_hasDerivAt line 40
  6. theorem OAI.SKFluctuations.Hierarchy.scalarSlopeZ_hasDerivAt line 64
  7. theorem OAI.SKFluctuations.Hierarchy.scalarSlopeInverse_nonneg line 70
  8. theorem OAI.SKFluctuations.Hierarchy.scalarSlopeJ_nonneg line 77
  9. theorem OAI.SKFluctuations.Hierarchy.scalarSlopeJ₁_nonneg line 82
  10. theorem OAI.SKFluctuations.Hierarchy.scalarSlopeJ₁_upper line 88
  11. def OAI.SKFluctuations.Hierarchy.scalarSlopeK line 117
  12. theorem OAI.SKFluctuations.Hierarchy.scalarSlopeZ_zero line 120
  13. theorem OAI.SKFluctuations.Hierarchy.scalarSlopeJ_monotoneOn line 124
  14. theorem OAI.SKFluctuations.Hierarchy.scalarSlopeK_eq_intermediate_J line 137
  15. theorem OAI.SKFluctuations.Hierarchy.scalarSlopeK_bounds line 153
  16. theorem OAI.SKFluctuations.Hierarchy.scalarSlopeK_hasDerivAt line 164
  17. theorem OAI.SKFluctuations.Hierarchy.scalarSlopeK_deriv_nonneg line 178
  18. theorem OAI.SKFluctuations.Hierarchy.shiftedGrid_integral line 195
  19. theorem OAI.SKFluctuations.Hierarchy.shiftedGrid_integral_truncated line 223
  20. def OAI.SKFluctuations.Scalar.slopeJet line 246
  21. theorem OAI.SKFluctuations.Scalar.spatialJet_one_injective line 249
  22. theorem OAI.SKFluctuations.Scalar.slopeJet_at_image line 259
  23. theorem OAI.SKFluctuations.Scalar.slopeJet_contDiffAt line 265
  24. theorem OAI.SKFluctuations.Scalar.slopeJet_space_hasDerivAt line 280
  25. theorem OAI.SKFluctuations.Scalar.slopeJet_time_hasDerivAt line 294
  26. def OAI.SKFluctuations.Scalar.slopeCurvatureSecond line 315
  27. theorem OAI.SKFluctuations.Scalar.slopeCurvature_timePDE line 320
  28. theorem OAI.SKFluctuations.Hierarchy.scalarClockProfileSlice_residual_uniform_root line 358
  29. theorem OAI.SKFluctuations.Hierarchy.scalarClockProfileSlice_exists_uniform_root_bound line 403
  30. def OAI.SKFluctuations.Hierarchy.terminalSpinKernel line 436
  31. theorem OAI.SKFluctuations.Hierarchy.terminalSpinDensity_measurable line 441
  32. theorem OAI.SKFluctuations.Hierarchy.terminalSpinKernel_apply line 447
  33. theorem OAI.SKFluctuations.Hierarchy.terminalSpinKernel_markov line 454
  34. def OAI.SKFluctuations.Hierarchy.plantedStepKernel line 467
  35. theorem OAI.SKFluctuations.Hierarchy.plantedStepDensity_measurable line 475
  36. theorem OAI.SKFluctuations.Hierarchy.plantedStepKernel_eq_tilted line 491
  37. theorem OAI.SKFluctuations.Hierarchy.plantedStepKernel_markov line 503
  38. def OAI.SKFluctuations.Hierarchy.ForwardPath line 514
  39. instance OAI.SKFluctuations.Hierarchy.forwardPathMeasurableSpace line 518
  40. def OAI.SKFluctuations.Hierarchy.hierarchyPathKernel line 523
  41. theorem OAI.SKFluctuations.Hierarchy.hierarchyPathKernel_markov line 531
  42. def OAI.SKFluctuations.Hierarchy.ForwardPath.spin line 545
  43. theorem OAI.SKFluctuations.Hierarchy.ForwardPath.spin_measurable line 549
  44. theorem OAI.SKFluctuations.Hierarchy.ForwardPath.integrable_spin line 557
  45. theorem OAI.SKFluctuations.Hierarchy.integral_terminalSpinKernel line 569
  46. theorem OAI.SKFluctuations.Hierarchy.integral_hierarchyPathKernel line 580
  47. theorem OAI.SKFluctuations.Hierarchy.condExp_compProd_first line 626