OAI/Geometry/TamingCompatibility/Concentration/ActivationScales.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.SummableCutoff.stepSize line 13
2. lemma OAI.TamingCompatibility.SummableCutoff.stepSize_pos line 14
3. lemma OAI.TamingCompatibility.SummableCutoff.stepSize_le_one line 15
4. lemma OAI.TamingCompatibility.SummableCutoff.summable_stepSize line 16
5. lemma OAI.TamingCompatibility.SummableCutoff.tendsto_stepSize line 17
6. def OAI.TamingCompatibility.SummableCutoff.thresholdScale line 19
7. lemma OAI.TamingCompatibility.SummableCutoff.thresholdScale_pos line 20
8. lemma OAI.TamingCompatibility.SummableCutoff.logActivation_step_threshold line 21
9. lemma OAI.TamingCompatibility.SummableCutoff.exists_activation_scales line 26
10. lemma OAI.TamingCompatibility.SummableCutoff.logActivation_integral_bound line 45
11. lemma OAI.TamingCompatibility.SummableCutoff.weighted_nonneg_ratio_bound line 52