Source indexedlemma · leanprover/lean4:v4.32.0

CH2.conj_intVSeg_of_antisymm

PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2178 to 2194

Mathematical statement

Exact Lean statement

lemma conj_intVSeg_of_antisymm (c a b : ℝ) (F : ℂ → ℂ) (hF : ∀ s, starRingEnd ℂ (F s) = -F (starRingEnd ℂ s)) :
    starRingEnd ℂ (intVSeg c a b F) = intVSeg c (-b) (-a) F

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma conj_intVSeg_of_antisymm (c a b : ℝ) (F : ℂ → ℂ) (hF : ∀ s, starRingEnd ℂ (F s) = -F (starRingEnd ℂ s)) :    starRingEnd ℂ (intVSeg c a b F) = intVSeg c (-b) (-a) F := by  unfold intVSeg  rw [← intervalIntegral_conj]  have h_integrand : ∀ t : ℝ, starRingEnd ℂ (F (↑c + ↑t * I) * I) = F (↑c + ↑(-t) * I) * I := by    intro t    rw [map_mul, conj_I]    have h1 : starRingEnd ℂ (↑c + ↑t * I) = ↑c + ↑(-t) * I := by      rw [map_add, map_mul, conj_ofReal, conj_ofReal, conj_I]      push_cast      ring    have h2 := hF (↑c + ↑t * I)    rw [h1] at h2    rw [h2]    ring  simp_rw [h_integrand]  rw [← intervalIntegral.integral_comp_neg]