OAI/NumberTheory/DirichletL/Reflection/ActualBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.InverseReflectedPhase.two_block_phase_bounds line 13
2. lemma OAI.SevenEighths.InverseReflectedPhase.actualRowPhase_norm_le_one line 39
3. lemma OAI.SevenEighths.InverseReflectedPhase.actualFrozenPhase_norm_le_one line 66