OAI/Probability/SKSupport/Parabolic/VarianceTilted.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ZeroTemperatureSK.Heat.varianceHeat_eq_semigroup_toNNReal line 19
  2. lemma OAI.ZeroTemperatureSK.Heat.varianceLogHeat_eq_logSemigroup_toNNReal line 27
  3. lemma OAI.ZeroTemperatureSK.Heat.uniform_logSemigroup_derivative_bounds line 36
  4. lemma OAI.ZeroTemperatureSK.Heat.regularDatum_varianceLogHeat line 58
  5. lemma OAI.ZeroTemperatureSK.Heat.uniform_varianceLogHeat_derivative_bounds line 66
  6. lemma OAI.ZeroTemperatureSK.Heat.varianceLogHeat_lipschitz line 76
  7. def OAI.ZeroTemperatureSK.Heat.varianceTilted line 83
  8. lemma OAI.ZeroTemperatureSK.Heat.varianceTilted_eq_tiltedMean line 87
  9. lemma OAI.ZeroTemperatureSK.Heat.varianceTilted_bound line 94
  10. lemma OAI.ZeroTemperatureSK.Heat.weightExp_iteratedDeriv_weight line 100
  11. lemma OAI.ZeroTemperatureSK.Heat.exponentialBound_weightExp_iteratedDeriv line 111