OAI/NumberTheory/DirichletL/Reflection/OriginalWeights.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SevenEighths.InverseReflectedPhase.frozenInactiveWeightline 11 - lemma
OAI.SevenEighths.InverseReflectedPhase.one_sub_inverse_norm_le_oneline 15 - lemma
OAI.SevenEighths.InverseReflectedPhase.frozenInactiveWeight_normline 25 - lemma
OAI.SevenEighths.InverseReflectedPhase.original_fourier_frozen_weight_normline 38