OAI/NumberTheory/Jacobsthal/Analysis/RieszMajorantIntegrals.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.arctan_le_self_nonneg line 13
2. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.rieszMajorant_upper_tail line 22
3. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.rieszMajorant_lower_tail line 31
4. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.rieszMajorant_interval_le line 41