Source indexedlemma · leanprover/lean4:v4.32.0

I9I1

PrimeNumberTheoremAnd.MediumPNT · PrimeNumberTheoremAnd/MediumPNT.lean:2136 to 2148

Mathematical statement

Exact Lean statement

lemma I9I1 {SmoothingF : ℝ → ℝ} {ε X T : ℝ} (Xpos : 0 < X) :
    I₉ SmoothingF ε X T = conj (I₁ SmoothingF ε X T)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma I9I1 {SmoothingF : ℝ → ℝ} {ε X T : ℝ} (Xpos : 0 < X) :    I₉ SmoothingF ε X T = conj (I₁ SmoothingF ε X T) := by  unfold I₉ I₁  simp only [map_mul, map_div₀, conj_I, conj_ofReal, conj_ofNat, map_one]  rw [neg_mul, mul_neg, ← neg_mul]  congr  · ring  · rw [← integral_conj, ← integral_comp_neg_Ioi, integral_Ici_eq_integral_Ioi]    apply setIntegral_congr_fun <| measurableSet_Ioi    intro t ht    simp only    rw[← smoothedChebyshevIntegrand_conj Xpos]    simp