OAI/NumberTheory/DirichletL/Reflection/NormalizedColumns.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.InverseReflectedPhase.actualFrozenPhase line 12
2. lemma OAI.SevenEighths.InverseReflectedPhase.sourceFrozenPhase_eq_actual line 18
3. lemma OAI.SevenEighths.InverseReflectedPhase.frozenExtracted_ne_zero line 34
4. lemma OAI.SevenEighths.InverseReflectedPhase.frozenBranchScale_pos line 41
5. def OAI.SevenEighths.InverseReflectedPhase.normalizedFrozenColumn line 48
6. lemma OAI.SevenEighths.InverseReflectedPhase.normalizedFrozenColumn_norm_le_one line 52
7. lemma OAI.SevenEighths.InverseReflectedPhase.frozenBranchColumn_eq_normalized line 62