OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/CardFourLeIntervalEnergy.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryCorrelations.SourceRoughRealScale.card_four_le_interval_energy line 29
2. lemma OAI.OrdinaryCorrelations.SourceRoughRealScale.energy_le_goodBox line 50
3. lemma OAI.OrdinaryCorrelations.SourceRoughRealScale.floor_geometry line 101
4. lemma OAI.OrdinaryCorrelations.SourceRoughRealScale.eventual_source_D_large line 121
5. theorem OAI.OrdinaryCorrelations.SourceRoughRealScale.eventual_real_energy line 132