Documentation

PrimeNumberTheoremAnd.ZetaConj

source
theorem deriv_conj_conj' (f : ℂ → ℂ) (p : ℂ) :
deriv (fun (z : ℂ) => (starRingEnd ℂ) (f ((starRingEnd ℂ) z))) ((starRingEnd ℂ) p) = (starRingEnd ℂ) (deriv f p)
Inspect dependencies

deriv_conj_conj' · compiled type and proof/definition references.

source
theorem deriv_riemannZeta_conj (s : ℂ) :
deriv riemannZeta ((starRingEnd ℂ) s) = (starRingEnd ℂ) (deriv riemannZeta s)
Inspect dependencies

deriv_riemannZeta_conj · compiled type and proof/definition references.

source
theorem logDerivZeta_conj (s : ℂ) :
(deriv riemannZeta / riemannZeta) ((starRingEnd ℂ) s) = (starRingEnd ℂ) ((deriv riemannZeta / riemannZeta) s)
Inspect dependencies

logDerivZeta_conj · compiled type and proof/definition references.

source
theorem logDerivZeta_conj' (s : ℂ) :
logDeriv riemannZeta ((starRingEnd ℂ) s) = (starRingEnd ℂ) (logDeriv riemannZeta s)
Inspect dependencies

logDerivZeta_conj' · compiled type and proof/definition references.

source
theorem intervalIntegral_conj {f : ℝ → ℂ} {a b : ℝ} :
∫ (x : ℝ) in a..b, (starRingEnd ℂ) (f x) = (starRingEnd ℂ) (∫ (x : ℝ) in a..b, f x)
Inspect dependencies

intervalIntegral_conj · compiled type and proof/definition references.