PoissonSubordination.lean

1 import KomorebiPaperVI.PoissonKernel
2 import KomorebiPaperVI.ReciprocalGaussian
3 
4 /-! Author: Komorebi P. The improper subordination integral for every nonnegative spectral mode. -/
5 namespace KomorebiPaperVI.PoissonSubordination
6 open Set MeasureTheory
7 open KomorebiPaperVI.PoissonKernel KomorebiPaperVI.ReciprocalGaussian
8 
9 theorem scaled_reciprocal_gaussian (t lam : ℝ) (ht : 0 < t) (hl : 0 ≤ lam) :
10     (∫ u in Ioi 0, Real.exp (-(t^2/4)*u^2-lam/u^2))=
11       Real.exp (-t*Real.sqrt lam)*Real.sqrt Real.pi/t := by
12   let a := t/2*Real.sqrt lam
13   have he : EqOn (fun u : ℝ => Real.exp (-(t^2/4)*u^2-lam/u^2))
14       (fun u => Real.exp (-(t/2*u)^2-a^2/(t/2*u)^2)) (Ioi 0) := by
15     intro u hu
16     dsimp only
17     congr 1
18     dsimp [a]
19     have hu0 : u ≠ 0 := ne_of_gt hu
20     field_simp [hu0,ht.ne']
21     nlinarith [Real.sq_sqrt hl]
22   rw [setIntegral_congr_fun measurableSet_Ioi he]
23   rw [integral_comp_mul_left_Ioi (fun u : ℝ => Real.exp (-u^2-a^2/u^2)) 0 (by positivity : 0 < t/2)]
24   simp only [mul_zero,smul_eq_mul]
25   rw [reciprocal_square_gaussian a (by dsimp [a]; positivity)]
26   have he : -2*a= -t*Real.sqrt lam := by dsimp [a]; ring
27   rw [he]
28   field_simp
29 
30 theorem heat_substitution (t lam s : ℝ) (hs : 0 < s) :
31     heatIntegrand t lam s=t/Real.sqrt Real.pi *
32       ((|(-1/2:ℝ)| *s^((-1/2:ℝ)-1)) •
33         Real.exp (-(t^2/4)*(s^(-1/2:ℝ))^2-lam/(s^(-1/2:ℝ))^2)) := by
34   unfold heatIntegrand
35   rw [kernel_substitution t s hs.le,inverse_half_square s hs.le]
36   simp only [smul_eq_mul]
37   rw [mul_assoc,mul_assoc,← Real.exp_add]
38   congr 3
39   field_simp
40   ring
41 
42 theorem scalar_subordination (t lam : ℝ) (ht : 0 < t) (hl : 0 ≤ lam) :
43     (∫ s in Ioi 0,heatIntegrand t lam s)=Real.exp (-t*Real.sqrt lam) := by
44   rw [setIntegral_congr_fun measurableSet_Ioi (fun s hs => heat_substitution t lam s hs)]
45   rw [integral_const_mul,integral_comp_rpow_Ioi
46     (fun u : ℝ => Real.exp (-(t^2/4)*u^2-lam/u^2)) (p := -1/2) (by norm_num)]
47   rw [scaled_reciprocal_gaussian t lam ht hl]
48   have hp : Real.sqrt Real.pi ≠ 0 := (Real.sqrt_pos.mpr Real.pi_pos).ne'
49   field_simp
50 
51 variable {I E : Type*} [Fintype I] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
52 theorem finite_spectral_subordination (P : I → E) (lam : I → ℝ) (hl : ∀ i,0 ≤ lam i)
53     (t : ℝ) (ht : 0 < t) :
54     (∫ s in Ioi 0,∑ i,heatIntegrand t (lam i) s • P i)=
55       ∑ i,Real.exp (-t*Real.sqrt (lam i)) • P i := by
56   rw [integral_finsetSum _ (fun i _ => (heat_integrand_integrable t (lam i) ht (hl i)).smul_const (P i))]
57   congr 1
58   funext i
59   rw [integral_smul_const,scalar_subordination t (lam i) ht (hl i)]
60 
61 open KomorebiPaperVI.SpectralPackets
62 variable {R : Type*} [DecidableEq I] [NormedRing R] [NormedAlgebra ℝ R] [CompleteSpace R]
63 
64 omit [CompleteSpace R] in
65 theorem operator_integrand (P : I → R) (hP : ∑ i,P i=1)
66     (h : ∀ i j,P i*P j=if i=j then P i else 0) (lam : I → ℝ) (t s : ℝ) :
67     kernel t s • NormedSpace.exp ((-s) • resolve P lam)=
68       ∑ i,heatIntegrand t (lam i) s • P i := by
69   have he : (-s) • resolve P lam=resolve P (fun i => -s*lam i) := by
70     simp [resolve,Finset.smul_sum,smul_smul]
71   rw [he,exp_resolution P hP h]
72   simp [resolve,Finset.smul_sum,smul_smul,heatIntegrand]
73 
74 theorem operator_subordination (P : I → R) (hP : ∑ i,P i=1)
75     (h : ∀ i j,P i*P j=if i=j then P i else 0) (lam : I → ℝ)
76     (hl : ∀ i,0 ≤ lam i) (t : ℝ) (ht : 0 < t) :
77     IntegrableOn (fun s => kernel t s • NormedSpace.exp ((-s) • resolve P lam)) (Ioi 0) ∧
78     NormedSpace.exp ((-t) • fractional P lam (1/2))=
79       ∫ s in Ioi 0,kernel t s • NormedSpace.exp ((-s) • resolve P lam) := by
80   simp only [operator_integrand P hP h lam]
81   refine ⟨finite_spectral_integrable P lam hl t ht,?_⟩
82   rw [finite_spectral_subordination P lam hl t ht,spectral_transfer_exponential P hP h]
83   simp only [spectralTransfer,resolve,Real.sqrt_eq_rpow]
84 
85 end KomorebiPaperVI.PoissonSubordination

Back to source controls