Source indexedlemma · leanprover/lean4:v4.32.0

I8I2

PrimeNumberTheoremAnd.MediumPNT · PrimeNumberTheoremAnd/MediumPNT.lean:2353 to 2377

Mathematical statement

Exact Lean statement

@[blueprint
  (title := "I8I2")
  (statement := /--
  Symmetry between $I_2$ and $I_8$:
  $$
  I_8(\nu, \epsilon, X, T) = -\overline{I_2(\nu, \epsilon, X, T)}
  .
  $$
  -/)
  (proof := /-- This is a direct consequence of the definitions of $I_2$ and $I_8$. -/)
  (latexEnv := "lemma")]
lemma I8I2 {SmoothingF : ℝ → ℝ}
    {X ε T σ₁ : ℝ} (T_gt : 3 < T) :
    I₈ SmoothingF ε X T σ₁ = -conj (I₂ SmoothingF ε X T σ₁)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  (title := "I8I2")  (statement := /--  Symmetry between $I_2$ and $I_8$:  $$  I_8(\nu, \epsilon, X, T) = -\overline{I_2(\nu, \epsilon, X, T)}  .  $$  -/)  (proof := /-- This is a direct consequence of the definitions of $I_2$ and $I_8$. -/)  (latexEnv := "lemma")]lemma I8I2 {SmoothingF : ℝ → ℝ}    {X ε T σ₁ : ℝ} (T_gt : 3 < T) :    I₈ SmoothingF ε X T σ₁ = -conj (I₂ SmoothingF ε X T σ₁) := by  unfold I₂ I₈  rw[map_mul, ← neg_mul]  congr  · simp[conj_ofNat]  · rw[← intervalIntegral_conj]    apply intervalIntegral.integral_congr    intro σ hσ    simp only []    rw[← smoothedChebyshevIntegrand_conj]    · simp only [map_sub, conj_ofReal, map_mul, conj_I, mul_neg, sub_neg_eq_add]    · exact lt_trans (by norm_num) T_gt