Source indexedlemma · leanprover/lean4:v4.32.0

DiffVertRect_eq_UpperLowerUs

PrimeNumberTheoremAnd.ResidueCalcOnRectangles · PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean:112 to 131

Mathematical statement

Exact Lean statement

@[blueprint
  (title := "DiffVertRect-eq-UpperLowerUs")
  (statement := /--
  The difference of two vertical integrals and a rectangle is
  the difference of an upper and a lower U integrals.
  -/)
  (proof := /-- Follows directly from the definitions. -/)
  (proofUses := ["UpperUIntegral", "LowerUIntegral"])
  (latexEnv := "lemma")]
lemma DiffVertRect_eq_UpperLowerUs {σ σ' T : ℝ}
    (f_int_σ : Integrable (fun (t : ℝ) ↦ f (σ + t * I)))
    (f_int_σ' : Integrable (fun (t : ℝ) ↦ f (σ' + t * I))) :
    VerticalIntegral f σ' - VerticalIntegral f σ -
      RectangleIntegral f (σ - I * T) (σ' + I * T) =
    UpperUIntegral f σ σ' T - LowerUIntegral f σ σ' T

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  (title := "DiffVertRect-eq-UpperLowerUs")  (statement := /--  The difference of two vertical integrals and a rectangle is  the difference of an upper and a lower U integrals.  -/)  (proof := /-- Follows directly from the definitions. -/)  (proofUses := ["UpperUIntegral", "LowerUIntegral"])  (latexEnv := "lemma")]lemma DiffVertRect_eq_UpperLowerUs {σ σ' T : ℝ}    (f_int_σ : Integrable (fun (t : ℝ) ↦ f (σ + t * I)))    (f_int_σ' : Integrable (fun (t : ℝ) ↦ f (σ' + t * I))) :    VerticalIntegral f σ' - VerticalIntegral f σ -      RectangleIntegral f (σ - I * T) (σ' + I * T) =    UpperUIntegral f σ σ' T - LowerUIntegral f σ σ' T := by  rw [verticalIntegral_split_three (-T) T f_int_σ, verticalIntegral_split_three (-T) T f_int_σ']  simp only [RectangleIntegral, UpperUIntegral, LowerUIntegral]  simp only [sub_re, mul_re, I_re, add_re, ofReal_re, I_im, ofReal_im, sub_im, mul_im, add_im]  ring_nf  abel