OAI/Probability/SKSupport/Foundations/Semigroup.lean
11 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.ZeroTemperatureSK.Heat.semigroupline 18 - def
OAI.ZeroTemperatureSK.Heat.logSemigroupline 21 - lemma
OAI.ZeroTemperatureSK.Heat.integrable_exp_absline 24 - lemma
OAI.ZeroTemperatureSK.Heat.integrable_translate_of_lipschitzline 39 - lemma
OAI.ZeroTemperatureSK.Heat.integrable_exp_translate_of_lipschitzline 53 - lemma
OAI.ZeroTemperatureSK.Heat.semigroup_exp_posline 71 - lemma
OAI.ZeroTemperatureSK.Heat.semigroup_lipschitzline 82 - lemma
OAI.ZeroTemperatureSK.Heat.logSemigroup_sub_leline 100 - lemma
OAI.ZeroTemperatureSK.Heat.logSemigroup_lipschitzline 125 - lemma
OAI.ZeroTemperatureSK.Heat.semigroup_evenline 145 - lemma
OAI.ZeroTemperatureSK.Heat.logSemigroup_evenline 161