Theorems · Theorem · number theory
Chebyshev.integrableOn_theta_div_id_mul_log_sq
∀ (x : ℝ), MeasureTheory.IntegrableOn (fun t => Chebyshev.theta t / (t * Real.log t ^ 2)) (Set.Icc 2 x) MeasureTheory.volume
Integrability for the integral in Chebyshev.primeCounting_eq_theta_div_log_add_integral.
- Defined in
- Mathlib.NumberTheory.Chebyshev
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 247 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites31
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setproof · cited by 53,352
- Realstatement and proof · cited by 25,697
- MeasureTheory.Measureproof · cited by 10,939
- Finset.sumproof · cited by 5,195
- Nat.cast_oneproof · cited by 2,501
- mul_commproof · cited by 2,262
- Nat.Primeproof · cited by 2,059
- Nat.cast_zeroproof · cited by 1,870
- Set.Iccstatement and proof · cited by 1,702
- MeasureTheory.MeasureSpace.volumestatement and proof · cited by 1,323
- Finset.filterproof · cited by 949
- Real.logstatement and proof · cited by 939
Cited by1
Results whose statement or proof uses this declaration.
- Chebyshev.integral_theta_div_log_sq_isBigOproof · cited by 2