OAI/Analysis/StrictMeans/Spectrum.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.StrictInverseFirstPower.integralMean_neg_one_pos line 11
2. lemma OAI.StrictInverseFirstPower.boundary_log_inverse_tendsto line 24
3. lemma OAI.StrictInverseFirstPower.growthExponent_le_of_mean_bound line 37