Source indexedlemma · leanprover/lean4:v4.32.0

ZetaAppendix.lemma_abadsumas_integrable_explog

PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2005 to 2019

Mathematical statement

Exact Lean statement

lemma lemma_abadsumas_integrable_explog {s : ℂ} {a b : ℝ} (ha : 0 < a) (hab : a < b) (k : ℤ) :
    IntervalIntegrable
      (fun y => ↑(y ^ (-s.re)) * e (-(s.im / (2 * π)) * Real.log y) * e (↑k * y))
      MeasureTheory.volume a b

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma lemma_abadsumas_integrable_explog {s : ℂ} {a b : ℝ} (ha : 0 < a) (hab : a < b) (k : ℤ) :    IntervalIntegrable      (fun y => ↑(y ^ (-s.re)) * e (-(s.im / (2 * π)) * Real.log y) * e (↑k * y))      MeasureTheory.volume a b := by  apply ContinuousOn.intervalIntegrable_of_Icc (le_of_lt hab)  apply ContinuousOn.mul  · apply ContinuousOn.mul    · apply continuous_ofReal.comp_continuousOn      apply ContinuousOn.rpow continuousOn_id continuousOn_const      exact fun _ hx => Or.inl (ne_of_gt (lt_of_lt_of_le ha hx.1))    · apply continuousOn_e_comp      apply ContinuousOn.mul continuousOn_const      apply Real.continuousOn_log.mono      exact fun _ hx => ne_of_gt (lt_of_lt_of_le ha hx.1)  · dsimp [e]; fun_prop