Source indexedlemma · leanprover/lean4:v4.32.0

verticalIntegral_split_three_finite

PrimeNumberTheoremAnd.MediumPNT · PrimeNumberTheoremAnd/MediumPNT.lean:1314 to 1328

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):
    VIntegral f σ s e =
    VIntegral f σ s a +
    VIntegral f σ a b +
    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):    VIntegral f σ s e =    VIntegral f σ s a +    VIntegral f σ a b +    VIntegral f σ b e := by  dsimp [VIntegral]  rw [← intervalIntegrable_iff_integrableOn_Icc_of_le (by linarith)] at hf  rw [← intervalIntegral.integral_add_adjacent_intervals (b := a),    ← intervalIntegral.integral_add_adjacent_intervals (a := a) (b := b)]  · ring  all_goals    apply IntervalIntegrable.mono_set hf    apply uIcc_subset_uIcc <;> apply mem_uIcc_of_le <;> linarith