PoissonKernel.lean

1 import KomorebiPaperVI.SpectralPackets
2 import Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
3 
4 /-! Author: Komorebi P. Normalized subordination density and convergence, including the zero mode.
5 The positive-mode Laplace identity is proved in PoissonSubordination. -/
6 namespace KomorebiPaperVI.PoissonKernel
7 open Set MeasureTheory
8 open scoped BigOperators
9 
10 noncomputable def kernel (t s : ℝ) : ℝ :=
11   t/(2*Real.sqrt Real.pi)*s^(-3/2:ℝ)*Real.exp (-t^2/(4*s))
12 noncomputable def heatIntegrand (t lam s : ℝ) : ℝ := kernel t s*Real.exp (-s*lam)
13 
14 theorem inverse_half_square (s : ℝ) (hs : 0 ≤ s) : (s^(-1/2:ℝ))^2=s⁻¹ := by
15   rw [← Real.rpow_natCast,← Real.rpow_mul hs]
16   norm_num [Real.rpow_neg_one]
17 
18 theorem kernel_substitution (t s : ℝ) (hs : 0 ≤ s) :
19     kernel t s=t/Real.sqrt Real.pi *
20       ((|(-1/2:ℝ)| *s^((-1/2:ℝ)-1)) • Real.exp (-(t^2/4)*(s^(-1/2:ℝ))^2)) := by
21   unfold kernel
22   rw [inverse_half_square s hs]
23   norm_num
24   have he : -(t^2/4*s⁻¹)=-t^2/(4*s) := by ring
25   rw [he]
26   ring
27 
28 theorem kernel_integrable (t : ℝ) (ht : 0 < t) : IntegrableOn (kernel t) (Ioi 0) := by
29   have hg := (integrable_exp_neg_mul_sq (b := t^2/4) (by positivity)).integrableOn (s := Ioi 0)
30   have hi := (integrableOn_Ioi_comp_rpow_iff (fun u : ℝ => Real.exp (-(t^2/4)*u^2))
31     (p := -1/2) (by norm_num)).mpr hg
32   rw [integrableOn_congr_fun (fun s hs => kernel_substitution t s hs.le) measurableSet_Ioi]
33   exact hi.const_mul (t/Real.sqrt Real.pi)
34 
35 theorem kernel_mass (t : ℝ) (ht : 0 < t) : (∫ s in Ioi 0,kernel t s)=1 := by
36   rw [setIntegral_congr_fun measurableSet_Ioi (fun s hs => kernel_substitution t s hs.le)]
37   rw [integral_const_mul,integral_comp_rpow_Ioi (fun u : ℝ => Real.exp (-(t^2/4)*u^2)) (p := -1/2) (by norm_num),integral_gaussian_Ioi]
38   have hp : Real.sqrt Real.pi≠0 := (Real.sqrt_pos.mpr Real.pi_pos).ne'
39   rw [Real.sqrt_div Real.pi_pos.le,Real.sqrt_div (sq_nonneg t),Real.sqrt_sq_eq_abs,abs_of_pos ht]
40   norm_num
41   field_simp
42 
43 theorem kernel_nonnegative (t s : ℝ) (ht : 0 ≤ t) (hs : 0 ≤ s) : 0 ≤ kernel t s := by
44   unfold kernel
45   positivity
46 
47 theorem heat_integrand_bounds (t lam s : ℝ) (ht : 0 ≤ t) (hl : 0 ≤ lam) (hs : 0 ≤ s) :
48     0 ≤ heatIntegrand t lam s ∧ heatIntegrand t lam s ≤ kernel t s := by
49   have hk := kernel_nonnegative t s ht hs
50   constructor
51   · exact mul_nonneg hk (Real.exp_pos _).le
52   · exact mul_le_of_le_one_right hk (Real.exp_le_one_iff.mpr (by nlinarith))
53 
54 theorem heat_integrand_integrable (t lam : ℝ) (ht : 0 < t) (hl : 0 ≤ lam) :
55     IntegrableOn (heatIntegrand t lam) (Ioi 0) := by
56   have hc : ContinuousOn (heatIntegrand t lam) (Ioi 0) := by
57     intro s hs
58     unfold heatIntegrand kernel
59     apply ContinuousAt.continuousWithinAt
60     have hs0 : s≠0 := hs.ne'
61     fun_prop (disch := simp_all)
62   apply (kernel_integrable t ht).mono' (hc.aestronglyMeasurable measurableSet_Ioi)
63   filter_upwards [ae_restrict_mem measurableSet_Ioi] with s hs
64   rw [Real.norm_of_nonneg (heat_integrand_bounds t lam s ht.le hl hs.le).1]
65   exact (heat_integrand_bounds t lam s ht.le hl hs.le).2
66 
67 theorem zero_mode_subordination (t : ℝ) (ht : 0 < t) :
68     (∫ s in Ioi 0,heatIntegrand t 0 s)=Real.exp (-t*Real.sqrt 0) := by
69   simpa [heatIntegrand] using kernel_mass t ht
70 
71 variable {I E : Type*} [Fintype I] [NormedAddCommGroup E] [NormedSpace ℝ E]
72 theorem finite_spectral_integrable (P : I → E) (lam : I → ℝ) (hl : ∀ i,0 ≤ lam i)
73     (t : ℝ) (ht : 0 < t) :
74     IntegrableOn (fun s => ∑ i,heatIntegrand t (lam i) s • P i) (Ioi 0) :=
75   integrable_finsetSum _ (fun i _ => (heat_integrand_integrable t (lam i) ht (hl i)).smul_const (P i))
76 
77 end KomorebiPaperVI.PoissonKernel

Back to source controls