Source indexedlemma · leanprover/lean4:v4.32.0

I7I3

PrimeNumberTheoremAnd.MediumPNT · PrimeNumberTheoremAnd/MediumPNT.lean:2976 to 2988

Mathematical statement

Exact Lean statement

lemma I7I3 {SmoothingF : ℝ → ℝ} {ε X T σ₁ : ℝ} (Xpos : 0 < X) :
    I₇ SmoothingF ε T X σ₁ = conj (I₃ SmoothingF ε T X σ₁)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma I7I3 {SmoothingF : ℝ → ℝ} {ε X T σ₁ : ℝ} (Xpos : 0 < X) :    I₇ SmoothingF ε T X σ₁ = conj (I₃ SmoothingF ε T X σ₁) := 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 [← intervalIntegral_conj, ← intervalIntegral.integral_comp_neg]    apply intervalIntegral.integral_congr    intro t ht    simp only    rw [← smoothedChebyshevIntegrand_conj Xpos]    simp