OAI/NumberTheory/Ostmann/Characters/HigherBiasHarmonicTransfer.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Characters.eventually_higher_harmonic_band_le_of_no_biased_mass line 15
2. def OAI.Ostmann.Characters.higherHarmonicBandMass line 35
3. lemma OAI.Ostmann.Characters.higherHarmonicBandMass_nonneg line 38
4. theorem OAI.Ostmann.Characters.higherHarmonicBandMass_isLittleO_of_eventually line 42