Source indexedlemma · leanprover/lean4:v4.32.0

verticalIntegral_split_three_finite'

PrimeNumberTheoremAnd.MediumPNT · PrimeNumberTheoremAnd/MediumPNT.lean:1330 to 1345

Mathematical statement

Exact Lean statement

lemma verticalIntegral_split_three_finite' {s a b e σ : ℝ} {f : ℂ → ℂ}
    (hf : IntegrableOn (fun t : ℝ ↦ f (σ + t * I)) (Icc s e))
    (hab: s < a ∧ a < b ∧ b < e):
    (1 : ℂ) / (2 * π * I) * (VIntegral f σ s e) =
    (1 : ℂ) / (2 * π * I) * (VIntegral f σ s a) +
    (1 : ℂ) / (2 * π * I) * (VIntegral f σ a b) +
    (1 : ℂ) / (2 * π * I) * (VIntegral f σ b e)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma verticalIntegral_split_three_finite' {s a b e σ : ℝ} {f : ℂ → ℂ}    (hf : IntegrableOn (fun t : ℝ ↦ f (σ + t * I)) (Icc s e))    (hab: s < a ∧ a < b ∧ b < e):    (1 : ℂ) / (2 * π * I) * (VIntegral f σ s e) =    (1 : ℂ) / (2 * π * I) * (VIntegral f σ s a) +    (1 : ℂ) / (2 * π * I) * (VIntegral f σ a b) +    (1 : ℂ) / (2 * π * I) * (VIntegral f σ b e) := by  have : (1 : ℂ) / (2 * π * I) * (VIntegral f σ s a) +      (1 : ℂ) / (2 * π * I) * (VIntegral f σ a b) +      (1 : ℂ) / (2 * π * I) * (VIntegral f σ b e) =        (1 : ℂ) / (2 * π * I) * ((VIntegral f σ s a) +    (VIntegral f σ a b) +    (VIntegral f σ b e)) := by ring  rw [this]  clear this  rw [← verticalIntegral_split_three_finite hf hab]