OAI/Probability/SKFluctuations/CenteredMonotoneIntegral.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

Centered Monotone Integral.

  1. theorem OAI.SKFluctuations.Scalar.halfLine_integral_pos line 19
  2. theorem OAI.SKFluctuations.Scalar.onePeak_nonneg line 30
  3. theorem OAI.SKFluctuations.Scalar.centered_weight_exists_zero line 61
  4. theorem OAI.SKFluctuations.Scalar.centered_weight_mul_nonneg line 84
  5. theorem OAI.SKFluctuations.Scalar.centered_weight_mul_pos line 104
  6. structure OAI.SKFluctuations.Scalar.PhysicalSlopeSlice line 143
  7. def OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.A line 163
  8. def OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.Φ line 164
  9. def OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.L line 165
  10. def OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.R₀ line 166
  11. def OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.R₁ line 167
  12. def OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.G line 168
  13. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.continuous_B line 170
  14. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.continuous_C line 171
  15. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.continuous_z line 172
  16. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.continuous_κ line 173
  17. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.dA line 175
  18. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.continuous_A line 178
  19. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.A_nonneg line 180
  20. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.z_strictMono line 190
  21. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.z_pos line 198
  22. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.z_nonneg line 201
  23. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.dΦ line 206
  24. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.continuous_Φ line 209
  25. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.Φ_strictMono line 211
  26. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.Φ_zero_neg line 219
  27. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.dL line 224
  28. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.L_strictAnti line 230
  29. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.dR₀ line 243
  30. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.dR₁ line 247
  31. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.R₁_monotone line 252
  32. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.weighted_tail_bounds line 262
  33. def OAI.SKFluctuations.Scalar.physicalSlopeOfJets line 294
  34. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.dC₂Φ line 340
  35. def OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.thirdTest line 355
  36. def OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.fluxCore line 358
  37. def OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.rootIntegrand line 361
  38. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.dfluxCore line 364
  39. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.dweightedFlux line 373
  40. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.fluxCore_zero line 379
  41. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.dweightedPrimitive line 382
  42. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.correction_nonneg line 388
  43. def OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.rootPrimitive line 412
  44. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.rootPrimitive_zero line 415
  45. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.rootPrimitive_hasDerivAt line 418
  46. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.rootPrimitive_tendsto line 427
  47. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.rootIntegral_pos line 434
  48. def OAI.SKFluctuations.Scalar.PolyBounded line 529
  49. theorem OAI.SKFluctuations.Scalar.PolyBounded.of_absBounded line 533
  50. theorem OAI.SKFluctuations.Scalar.PolyBounded.const line 537
  51. theorem OAI.SKFluctuations.Scalar.PolyBounded.id line 539
  52. theorem OAI.SKFluctuations.Scalar.PolyBounded.add line 544
  53. theorem OAI.SKFluctuations.Scalar.PolyBounded.neg line 557
  54. theorem OAI.SKFluctuations.Scalar.PolyBounded.sub line 561
  55. theorem OAI.SKFluctuations.Scalar.PolyBounded.mul line 564
  56. theorem OAI.SKFluctuations.Scalar.PolyBounded.const_mul line 573
  57. theorem OAI.SKFluctuations.Scalar.PolyBounded.div_const line 575
  58. theorem OAI.SKFluctuations.Scalar.PolyBounded.pow line 578
  59. def OAI.SKFluctuations.Scalar.GaussianDominated line 585
  60. theorem OAI.SKFluctuations.Scalar.gaussian_nat_integrable line 588
  61. theorem OAI.SKFluctuations.Scalar.gaussian_nat_tendsto line 593
  62. theorem OAI.SKFluctuations.Scalar.polynomial_gaussian_majorant line 598
  63. theorem OAI.SKFluctuations.Scalar.GaussianDominated.mul_poly_integrable line 605
  64. theorem OAI.SKFluctuations.Scalar.GaussianDominated.mul_poly_tendsto line 622