OAI/Probability/SKFluctuations/NonnegativeProfileValueStep.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

Nonnegative Profile Value Step.

  1. theorem OAI.SKFluctuations.Hierarchy.HeatJet.nonnegativeProfileValue_step line 21
  2. theorem OAI.SKFluctuations.Scalar.gaussian_cosh_integrable line 73
  3. theorem OAI.SKFluctuations.Scalar.gaussian_cosh line 83
  4. theorem OAI.SKFluctuations.Hierarchy.integral_gaussian_eval line 107
  5. theorem OAI.SKFluctuations.Hierarchy.scalarTerminal_mass_one line 118
  6. def OAI.SKFluctuations.GaussianCalculus.ExpBounded line 136
  7. theorem OAI.SKFluctuations.GaussianCalculus.standardGaussian_exp_abs_integrable line 139
  8. theorem OAI.SKFluctuations.GaussianCalculus.affine_exp_bound line 153
  9. theorem OAI.SKFluctuations.GaussianCalculus.affine_z_exp_bound line 163
  10. theorem OAI.SKFluctuations.GaussianCalculus.ExpBounded.affine_integrable line 174
  11. theorem OAI.SKFluctuations.GaussianCalculus.ExpBounded.affine_z_integrable line 183
  12. theorem OAI.SKFluctuations.GaussianCalculus.hasDerivAt_gaussian_affine line 194
  13. theorem OAI.SKFluctuations.GaussianCalculus.hasDerivAt_gaussian_affine_heat line 223
  14. theorem OAI.SKFluctuations.GaussianCalculus.hasDerivAt_gaussian_variance line 237
  15. theorem OAI.SKFluctuations.GaussianCalculus.ExpBounded.exp_lipschitz line 253
  16. theorem OAI.SKFluctuations.GaussianCalculus.ExpBounded.of_lipschitz line 265
  17. theorem OAI.SKFluctuations.GaussianCalculus.ExpBounded.bdd_mul line 279
  18. theorem OAI.SKFluctuations.GaussianCalculus.hasDerivAt_scalar_heat_continuation line 289
  19. theorem OAI.SKFluctuations.GaussianCalculus.ExpBounded.continuous_gaussian_affine line 336
  20. theorem OAI.SKFluctuations.GaussianCalculus.ExpBounded.continuous_gaussian_variance line 360
  21. theorem OAI.SKFluctuations.GaussianCalculus.hasDerivWithinAt_gaussian_variance_zero line 366
  22. theorem OAI.SKFluctuations.GaussianCalculus.hasDerivWithinAt_gaussian_variance line 387
  23. def OAI.SKFluctuations.Scalar.logCosh line 405
  24. def OAI.SKFluctuations.Scalar.curvature line 406
  25. def OAI.SKFluctuations.Scalar.third line 407
  26. def OAI.SKFluctuations.Scalar.fourth line 408
  27. theorem OAI.SKFluctuations.Scalar.tanh_derivative line 410
  28. theorem OAI.SKFluctuations.Scalar.logCosh_derivative line 418
  29. theorem OAI.SKFluctuations.Scalar.curvature_derivative line 424
  30. theorem OAI.SKFluctuations.Scalar.third_derivative line 431
  31. theorem OAI.SKFluctuations.Scalar.tanh_continuous line 438
  32. theorem OAI.SKFluctuations.Scalar.curvature_continuous line 441
  33. theorem OAI.SKFluctuations.Scalar.third_continuous line 444
  34. theorem OAI.SKFluctuations.Scalar.fourth_continuous line 447
  35. theorem OAI.SKFluctuations.Scalar.logCosh_lipschitz line 450
  36. theorem OAI.SKFluctuations.Scalar.curvature_bounds line 456
  37. theorem OAI.SKFluctuations.Scalar.logCosh_expBounded line 461
  38. theorem OAI.SKFluctuations.Scalar.tanh_expBounded line 465
  39. theorem OAI.SKFluctuations.Scalar.curvature_expBounded line 470
  40. theorem OAI.SKFluctuations.Scalar.third_expBounded line 475
  41. theorem OAI.SKFluctuations.Scalar.fourth_expBounded line 483
  42. def OAI.SKFluctuations.Scalar.rsHeat line 499
  43. def OAI.SKFluctuations.Scalar.rsHeatSlope line 500
  44. theorem OAI.SKFluctuations.Scalar.rsHeat_derivative line 502
  45. theorem OAI.SKFluctuations.Scalar.rsHeatSlope_derivative_zero line 509
  46. theorem OAI.SKFluctuations.Scalar.rsHeat_zero line 518
  47. theorem OAI.SKFluctuations.Scalar.rsHeatSlope_zero line 519
  48. def OAI.SKFluctuations.Scalar.rsVariation line 521
  49. def OAI.SKFluctuations.Scalar.rsVariationSlope line 522
  50. theorem OAI.SKFluctuations.Scalar.rsVariation_zero line 524
  51. theorem OAI.SKFluctuations.Scalar.rsVariationSlope_zero line 525
  52. theorem OAI.SKFluctuations.Scalar.rsVariation_derivative line 527
  53. theorem OAI.SKFluctuations.Scalar.rsVariationSlope_derivative_zero line 539
  54. theorem OAI.SKFluctuations.Scalar.rsVariation_strictly_negative line 558
  55. def OAI.SKFluctuations.Hierarchy.diracMassProfile line 592
  56. theorem OAI.SKFluctuations.Hierarchy.diracMassProfile_mem line 602
  57. theorem OAI.SKFluctuations.Hierarchy.scalarPenalty_dirac line 609
  58. theorem OAI.SKFluctuations.Hierarchy.scalarRoot_mass_one line 632