OAI/Probability/SKSupport/Foundations/DerivWithinVarianceHeatWeightExp.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ZeroTemperatureSK.Heat.hasDerivWithinAt_varianceHeat_weightExp line 18
  2. lemma OAI.ZeroTemperatureSK.Heat.hasDerivWithinAt_varianceTilted line 32
  3. lemma OAI.ZeroTemperatureSK.Heat.varianceTilted_time_lipschitz line 49
  4. lemma OAI.ZeroTemperatureSK.Heat.varianceTilted_space_lipschitz line 79
  5. lemma OAI.ZeroTemperatureSK.Heat.varianceTilted_joint_bound line 95
  6. lemma OAI.ZeroTemperatureSK.Heat.varianceHeat_const_mul line 116
  7. lemma OAI.ZeroTemperatureSK.Heat.varianceTilted_zero line 120
  8. def OAI.ZeroTemperatureSK.Heat.generatorWeight line 124
  9. lemma OAI.ZeroTemperatureSK.Heat.boundedSmooth_generatorWeight line 127
  10. lemma OAI.ZeroTemperatureSK.Heat.deriv_exp_comp line 133
  11. lemma OAI.ZeroTemperatureSK.Heat.deriv_deriv_exp_comp line 139
  12. lemma OAI.ZeroTemperatureSK.Heat.varianceLogHeat_time_derivative line 149
  13. lemma OAI.ZeroTemperatureSK.Heat.varianceLogHeat_generator_identity line 178