OAI/Analysis/StrictMeans/SpectralGrowth.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.StrictInverseFirstPower.logNormPower_subadditive line 41
2. def OAI.StrictInverseFirstPower.logNormGrowth line 51
3. lemma OAI.StrictInverseFirstPower.logNormPower_div_bddBelow line 54
4. lemma OAI.StrictInverseFirstPower.tendsto_logNormGrowth line 60
5. lemma OAI.StrictInverseFirstPower.logNormGrowth_nonneg line 64
6. lemma OAI.StrictInverseFirstPower.normPower_eventually_le_exp line 69
7. lemma OAI.StrictInverseFirstPower.logNormGrowth_le_of_power_bound line 78
8. lemma OAI.StrictInverseFirstPower.summable_resolventPower line 95