OAI/Analysis/SymmetricDomains/PrimeZeroLocusFixed.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Release061.parameterPeak_log_norm line 35
2. lemma OAI.Release061.coordinateEnergy_sub_hasFDerivAt line 44
3. theorem OAI.Release061.parameterPeak_log_norm_hasFDerivAt line 51
4. theorem OAI.Release061.parameterPeak_log_differential line 63
5. theorem OAI.Release061.prime_zeroLocus_fixed_charts line 80