OAI/NumberTheory/SiegelZeros/EntireFunctions/NormalizedHadamardTransfer.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SiegelZeros.WeightedTorusJets.W63.NormalizedZeroSumAt line 12
2. theorem OAI.SiegelZeros.WeightedTorusJets.W63.parity_complex_cast line 20
3. theorem OAI.SiegelZeros.WeightedTorusJets.W63.normalized_logDerivative_real line 25
4. theorem OAI.SiegelZeros.WeightedTorusJets.W63.NormalizedZeroSumAt.to_HadamardFormulaAt line 47
5. theorem OAI.SiegelZeros.WeightedTorusJets.W63.normalizedZeroSum_of_regularized_identity line 58
6. theorem OAI.SiegelZeros.WeightedTorusJets.W63.exists_good_mass_of_normalizedZeroSum line 90