Source indexedlemma · leanprover/lean4:v4.32.0

integrable_exp_neg_mul_I_smul

PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:413 to 424

Source documentation

Multiplying an integrable function by a negative unit-modulus exponential preserves integrability.

Exact Lean statement

lemma integrable_exp_neg_mul_I_smul {f : ℝ → E} (hf : Integrable f) (T : ℝ) :
    Integrable (fun v : ℝ => Complex.exp (-(((T * v : ℝ) : ℂ) * I)) • f v)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma integrable_exp_neg_mul_I_smul {f : ℝ → E} (hf : Integrable f) (T : ℝ) :    Integrable (fun v : ℝ => Complex.exp (-(((T * v : ℝ) : ℂ) * I)) • f v) := by  refine hf.mono ?_ ?_  · exact (by fun_prop : Continuous (fun v : ℝ =>        Complex.exp (-(((T * v : ℝ) : ℂ) * I))))      |>.aestronglyMeasurable.smul hf.aestronglyMeasurable  · filter_upwards with v    rw [norm_smul]    have harg : -(((T * v : ℝ) : ℂ) * I) = (((-(T * v) : ℝ) : ℂ) * I) := by      push_cast      ring    rw [harg, Complex.norm_exp_ofReal_mul_I, one_mul]