OAI/Geometry/TamingCompatibility/Charts/SlowLogCutoff.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.SummableCutoff.logActivation line 12
2. lemma OAI.TamingCompatibility.SummableCutoff.logActivation_nonneg line 14
3. lemma OAI.TamingCompatibility.SummableCutoff.logActivation_le line 21
4. lemma OAI.TamingCompatibility.SummableCutoff.hasDerivAt_logActivation line 27
5. lemma OAI.TamingCompatibility.SummableCutoff.logActivation_deriv_bound line 36
6. lemma OAI.TamingCompatibility.SummableCutoff.logActivation_threshold line 46
7. lemma OAI.TamingCompatibility.SummableCutoff.threshold_scale_pos line 57
8. lemma OAI.TamingCompatibility.SummableCutoff.tendsto_of_summable_activation line 63