OAI/Probability/SKSupport/Parabolic/AffineEvolution.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ZeroTemperatureSK.Heat.AffineSmoothFamily.mul_bounded line 12
  2. lemma OAI.ZeroTemperatureSK.Heat.integral_affine_rate line 22
  3. lemma OAI.ZeroTemperatureSK.Heat.integral_affine_rate_derivative line 33
  4. lemma OAI.ZeroTemperatureSK.Heat.hasDerivAt_affine_evolution_jet line 47
  5. lemma OAI.ZeroTemperatureSK.Heat.tiltedMean_add line 73
  6. lemma OAI.ZeroTemperatureSK.Heat.tiltedMean_const_mul line 85
  7. lemma OAI.ZeroTemperatureSK.Heat.tiltedMean_const line 92
  8. lemma OAI.ZeroTemperatureSK.Heat.tiltedMean_nonneg line 100
  9. lemma OAI.ZeroTemperatureSK.Heat.tiltedMean_pos line 105
  10. lemma OAI.ZeroTemperatureSK.Heat.tiltedMean_variance_nonneg line 120
  11. lemma OAI.ZeroTemperatureSK.Heat.deriv_logSemigroup_tilted line 136
  12. lemma OAI.ZeroTemperatureSK.Heat.logSemigroup_curvature_pos line 148