Source indexedtheorem · leanprover/lean4:v4.32.0

integrable_exp_neg_mul_sin_prod_Ioi

PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:1964 to 2029

Source documentation

Product-integrability of the damped sine kernel on (0,∞) × (a,∞). The proof integrates the u-tail first and bounds the inner norm by exp (-a*x) using |sin x| ≤ x for x > 0.

Exact Lean statement

theorem integrable_exp_neg_mul_sin_prod_Ioi (a : ℝ) (ha : 0 < a) :
    Integrable
      (Function.uncurry
        (fun x u : ℝ => Real.exp (-u * x) * Real.sin x))
      ((volume.restrict (Set.Ioi 0)).prod (volume.restrict (Set.Ioi a)))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem integrable_exp_neg_mul_sin_prod_Ioi (a : ℝ) (ha : 0 < a) :    Integrable      (Function.uncurry        (fun x u : ℝ => Real.exp (-u * x) * Real.sin x))      ((volume.restrict (Set.Ioi 0)).prod (volume.restrict (Set.Ioi a))) := by  let μ := volume.restrict (Set.Ioi (0 : ℝ))  let ν := volume.restrict (Set.Ioi a)  change Integrable      (Function.uncurry        (fun x u : ℝ => Real.exp (-u * x) * Real.sin x)) (μ.prod ν)  have hsm : AEStronglyMeasurable      (Function.uncurry        (fun x u : ℝ => Real.exp (-u * x) * Real.sin x)) (μ.prod ν) := by    exact (by fun_prop : AEStronglyMeasurable      (Function.uncurry        (fun x u : ℝ => Real.exp (-u * x) * Real.sin x)) (μ.prod ν))  rw [integrable_prod_iff hsm]  constructor  · dsimp [μ]    filter_upwards [ae_restrict_mem measurableSet_Ioi] with x hx    change Integrable (fun u : ℝ => Real.exp (-u * x) * Real.sin x) ν    have h_exp : Integrable (fun u : ℝ => Real.exp (-u * x)) ν := by      dsimp [ν]      change IntegrableOn (fun u : ℝ => Real.exp (-u * x)) (Set.Ioi a)      simpa [mul_comm] using integrableOn_exp_mul_Ioi (a := -x) (neg_lt_zero.mpr hx) a    exact h_exp.mul_const (Real.sin x)  · have h_exp_a : Integrable (fun x : ℝ => Real.exp (-a * x)) μ := by      dsimp [μ]      change IntegrableOn (fun x : ℝ => Real.exp (-a * x)) (Set.Ioi 0)      simpa [mul_comm] using exp_neg_integrableOn_Ioi (0 : ℝ) (b := a) ha    refine h_exp_a.mono ?_ ?_    · exact hsm.norm.integral_prod_right'    · filter_upwards [ae_restrict_mem measurableSet_Ioi] with x hx      have hx0 : 0 < x := hx      have h_exp_x : Integrable (fun y : ℝ => Real.exp (-y * x)) ν := by        dsimp [ν]        change IntegrableOn (fun y : ℝ => Real.exp (-y * x)) (Set.Ioi a)        simpa [mul_comm] using integrableOn_exp_mul_Ioi (a := -x) (neg_lt_zero.mpr hx0) a      have h_lhs : Integrable          (fun y : ℝ => ‖Function.uncurry            (fun x u : ℝ => Real.exp (-u * x) * Real.sin x) (x, y)‖) ν := by        simpa [Function.uncurry] using (h_exp_x.mul_const (Real.sin x)).norm      have h_rhs : Integrable (fun y : ℝ => Real.exp (-y * x) * x) ν :=        h_exp_x.mul_const x      calc        ‖∫ y : ℝ, ‖Function.uncurry            (fun x u : ℝ => Real.exp (-u * x) * Real.sin x) (x, y)‖ ∂ν‖            = ∫ y : ℝ, ‖Function.uncurry                (fun x u : ℝ => Real.exp (-u * x) * Real.sin x) (x, y)‖ ∂ν := by              rw [Real.norm_eq_abs, abs_of_nonneg]              exact integral_nonneg fun y => norm_nonneg _        _ ≤ ∫ y : ℝ, Real.exp (-y * x) * x ∂ν := by              refine integral_mono_ae h_lhs h_rhs ?_              filter_upwards with y              rw [Function.uncurry, Real.norm_eq_abs, abs_mul,                abs_of_pos (Real.exp_pos _)]              exact mul_le_mul_of_nonneg_left                (by simpa [abs_of_pos hx0] using (Real.abs_sin_le_abs (x := x)))                (Real.exp_pos _).le        _ = Real.exp (-a * x) := by              dsimp [ν]              rw [integral_mul_const]              rw [integral_Ioi_exp_neg_mul_const a x hx0]              field_simp [hx0.ne']        _ = ‖Real.exp (-a * x)‖ := by              rw [Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)]