OAI/Geometry/Riemannian/HarmonicCore/Frequency.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicCounterexample.FrequencyArithmetic.bandNumerator line 19
2. def OAI.HarmonicCounterexample.FrequencyArithmetic.bandMean line 22
3. lemma OAI.HarmonicCounterexample.FrequencyArithmetic.weighted_round_sum line 25
4. lemma OAI.HarmonicCounterexample.FrequencyArithmetic.bandNumerator_eq line 35
5. lemma OAI.HarmonicCounterexample.FrequencyArithmetic.quotient_bound line 45
6. lemma OAI.HarmonicCounterexample.FrequencyArithmetic.bandMean_bound line 60
7. theorem OAI.HarmonicCounterexample.FrequencyArithmetic.arithmetic_frequency_margin line 70