BetaNormalization.lean

1 import Mathlib.Analysis.SpecialFunctions.Gamma.Beta
2 import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
3 
4 /-! Author: Komorebi P. Exact sine normalization of the fractional integral. -/
5 namespace KomorebiPaperVI.BetaNormalization
6 open Set MeasureTheory
7 set_option backward.isDefEq.respectTransparency false
8 
9 noncomputable def betaKernel (a x : ℝ) : ℝ := x^(a-1)*(1-x)^(-a)
10 noncomputable def changeVariable (x : ℝ) : ℝ := x/(1+x)
11 
12 theorem beta_value (a : ℝ) (ha : a∈Ioo 0 1) :
13     (∫ x in Ioo 0 1,betaKernel a x)=Real.pi/Real.sin (Real.pi*a) := by
14   have h := Complex.Gamma_mul_Gamma_eq_betaIntegral (s := (a:ℂ)) (t := 1-(a:ℂ))
15     (by simpa using ha.1) (by simpa using sub_pos.mpr ha.2)
16   rw [add_sub_cancel,Complex.Gamma_one,one_mul,Complex.Gamma_mul_Gamma_one_sub] at h
17   have he : Complex.betaIntegral (a:ℂ) (1-(a:ℂ))=
18       ((∫ x in Ioo 0 1,betaKernel a x):ℝ) := by
19     rw [Complex.betaIntegral,intervalIntegral.integral_of_le (by norm_num : (0:ℝ) ≤ 1),
20       integral_Ioc_eq_integral_Ioo]
21     trans ∫ x in Ioo (0:ℝ) 1,(betaKernel a x:ℂ)
22     · apply setIntegral_congr_fun measurableSet_Ioo
23       intro x hx
24       dsimp [betaKernel]
25       rw [Complex.ofReal_mul,Complex.ofReal_cpow hx.1.le,Complex.ofReal_cpow (by linarith [hx.2] : 0 ≤ 1-x)]
26       push_cast
27       congr 2
28       ring
29     · exact integral_complex_ofReal
30   rw [he] at h
31   exact_mod_cast h.symm
32 
33 theorem change_derivative (x : ℝ) (hx : 0 < x) :
34     HasDerivAt changeVariable ((1+x)^(-2:ℤ)) x := by
35   convert! (hasDerivAt_id x).div ((hasDerivAt_const x 1).add (hasDerivAt_id x)) (by linarith : 1+x≠0) using 1
36   simp [zpow_neg,div_eq_mul_inv]
37 
38 theorem change_injective : InjOn changeVariable (Ioi 0) := by
39   intro x hx y hy h
40   change 0 < x at hx
41   change 0 < y at hy
42   dsimp [changeVariable] at h
43   have h := (div_eq_div_iff (by linarith : 1+x≠0) (by linarith : 1+y≠0)).mp h
44   nlinarith
45 
46 theorem change_image : changeVariable '' Ioi 0=Ioo 0 1 := by
47   ext y
48   constructor
49   · rintro ⟨x,hx,rfl⟩
50     change 0 < x at hx
51     dsimp [changeVariable]
52     exact ⟨div_pos hx (by linarith), (div_lt_one (by linarith : 0 < 1+x)).mpr (by linarith)⟩
53   · intro hy
54     refine ⟨y/(1-y),div_pos hy.1 (sub_pos.mpr hy.2),?_⟩
55     dsimp [changeVariable]
56     have hy0 : 1-y ≠ 0 := ne_of_gt (sub_pos.mpr hy.2)
57     field_simp [hy0]
58     ring
59 
60 theorem change_integrand (a x : ℝ) (hx : 0 < x) :
61     |(1+x)^(-2:ℤ)| • betaKernel a (changeVariable x)=x^(a-1)/(1+x) := by
62   have hd : 0 < 1+x := by linarith
63   have hs : 1-x/(1+x)=1/(1+x) := by field_simp; ring
64   dsimp [betaKernel,changeVariable]
65   rw [hs,Real.div_rpow hx.le hd.le,Real.rpow_neg (by positivity : 0 ≤ 1/(1+x)),Real.div_rpow zero_le_one hd.le]
66   simp only [Real.one_rpow,one_div,inv_inv,zpow_neg,zpow_ofNat,abs_inv,abs_of_nonneg (sq_nonneg (1+x))]
67   rw [Real.rpow_sub hd,Real.rpow_one]
68   field_simp
69 
70 theorem rational_integral (a : ℝ) (ha : a∈Ioo 0 1) :
71     (∫ x in Ioi 0,x^(a-1)/(1+x))=Real.pi/Real.sin (Real.pi*a) := by
72   have h := integral_image_eq_integral_abs_deriv_smul measurableSet_Ioi
73     (fun x hx => (change_derivative x hx).hasDerivWithinAt) change_injective (betaKernel a)
74   rw [change_image] at h
75   rw [← beta_value a ha,h]
76   apply setIntegral_congr_fun measurableSet_Ioi
77   intro x hx
78   exact (change_integrand a x hx).symm
79 
80 theorem normalizer_exact (a : ℝ) (ha : a∈Ioo 0 1) :
81     (∫ t in Ioi 0,Real.rpowIntegrand₀₁ a t 1)=Real.pi/Real.sin (Real.pi*a) := by
82   rw [← rational_integral a ha]
83   apply setIntegral_congr_fun measurableSet_Ioi
84   intro t ht
85   dsimp only
86   rw [Real.rpowIntegrand₀₁_eq_pow_div ha ht.le zero_le_one,mul_one,add_comm]
87 
88 theorem sine_factor_positive (a : ℝ) (ha : a∈Ioo 0 1) :
89     0 < Real.sin (Real.pi*a)/Real.pi := by
90   apply div_pos _ Real.pi_pos
91   apply Real.sin_pos_of_pos_of_lt_pi
92   · exact mul_pos Real.pi_pos ha.1
93   · nlinarith [Real.pi_pos,ha.2]
94 
95 theorem scalar_fractional_integral (a x : ℝ) (ha : a∈Ioo 0 1) (hx : 0 ≤ x) :
96     x^a=(Real.sin (Real.pi*a)/Real.pi)*(∫ t in Ioi 0,Real.rpowIntegrand₀₁ a t x) := by
97   rw [Real.rpow_eq_const_mul_integral ha hx,normalizer_exact a ha,inv_div]
98 
99 theorem beta_real_integral (a b : ℝ) (ha : 0 < a) (hb : 0 < b) :
100     (∫ x in Ioo 0 1,x^(a-1)*(1-x)^(b-1))=Real.Gamma a*Real.Gamma b/Real.Gamma (a+b) := by
101   have h := Complex.betaIntegral_eq_Gamma_mul_div (a:ℂ) (b:ℂ) (by simpa) (by simpa)
102   have he : Complex.betaIntegral (a:ℂ) (b:ℂ)=
103       ((∫ x in Ioo 0 1,x^(a-1)*(1-x)^(b-1)):ℝ) := by
104     rw [Complex.betaIntegral,intervalIntegral.integral_of_le (by norm_num : (0:ℝ) ≤ 1),integral_Ioc_eq_integral_Ioo]
105     trans ∫ x in Ioo (0:ℝ) 1,((x^(a-1)*(1-x)^(b-1):ℝ):ℂ)
106     · apply setIntegral_congr_fun measurableSet_Ioo
107       intro x hx
108       dsimp only
109       rw [Complex.ofReal_mul,Complex.ofReal_cpow hx.1.le,Complex.ofReal_cpow (by linarith [hx.2] : 0 ≤ 1-x)]
110       push_cast
111       rfl
112     · exact integral_complex_ofReal
113   rw [he,← Complex.ofReal_add,Complex.Gamma_ofReal,Complex.Gamma_ofReal,Complex.Gamma_ofReal] at h
114   exact_mod_cast h
115 
116 theorem weighted_beta_value (p : ℝ) (hp : p∈Ioo 0 1) :
117     (∫ x in Ioo 0 1,x^p*(1-x)^(-p))=p*Real.pi/Real.sin (Real.pi*p) := by
118   have h := beta_real_integral (p+1) (1-p) (by linarith [hp.1]) (sub_pos.mpr hp.2)
119   rw [add_sub_cancel_right,show 1-p-1= -p by ring,show p+1+(1-p)=2 by ring,
120     Real.Gamma_add_one hp.1.ne',Real.Gamma_two,div_one,mul_assoc,Real.Gamma_mul_Gamma_one_sub] at h
121   simpa only [mul_div_assoc] using h
122 
123 theorem gap_change_integrand (p x : ℝ) (hx : 0 < x) :
124     |(1+x)^(-2:ℤ)| • ((changeVariable x)^p*(1-changeVariable x)^(-p))=x^p/(1+x)^2 := by
125   have hd : 0 < 1+x := by linarith
126   have hs : 1-x/(1+x)=1/(1+x) := by field_simp; ring
127   dsimp [changeVariable]
128   rw [hs,Real.div_rpow hx.le hd.le,Real.rpow_neg (by positivity : 0 ≤ 1/(1+x)),Real.div_rpow zero_le_one hd.le]
129   simp only [Real.one_rpow,one_div,inv_inv,zpow_neg,zpow_ofNat,abs_inv,abs_of_nonneg (sq_nonneg (1+x))]
130   field_simp
131 
132 theorem unit_gap_integral (p : ℝ) (hp : p∈Ioo 0 1) :
133     (∫ x in Ioi 0,x^p/(1+x)^2)=p*Real.pi/Real.sin (Real.pi*p) := by
134   have h := integral_image_eq_integral_abs_deriv_smul measurableSet_Ioi
135     (fun x hx => (change_derivative x hx).hasDerivWithinAt) change_injective
136     (fun x : ℝ => x^p*(1-x)^(-p))
137   rw [change_image] at h
138   rw [← weighted_beta_value p hp,h]
139   apply setIntegral_congr_fun measurableSet_Ioi
140   intro x hx
141   exact (gap_change_integrand p x hx).symm
142 
143 theorem gap_integral (p m : ℝ) (hp : p∈Ioo 0 1) (hm : 0 < m) :
144     (∫ t in Ioi 0,t^p/(t+m)^2)=m^(p-1)*(p*Real.pi/Real.sin (Real.pi*p)) := by
145   have h := integral_comp_mul_left_Ioi' (fun t : ℝ => t^p/(t+m)^2) 0 hm
146   simp only [mul_zero,smul_eq_mul] at h
147   rw [← h]
148   have he : EqOn (fun x : ℝ => (m*x)^p/(m*x+m)^2)
149       (fun x => m^(p-2)*(x^p/(1+x)^2)) (Ioi 0) := by
150     intro x hx
151     dsimp only
152     rw [Real.mul_rpow hm.le (le_of_lt hx),Real.rpow_sub hm,Real.rpow_two]
153     have hd : 1+x ≠ 0 := by linarith [show 0 < x from hx]
154     rw [show m*x+m=m*(1+x) by ring,mul_pow]
155     field_simp [hm.ne',hd]
156   rw [setIntegral_congr_fun measurableSet_Ioi he,integral_const_mul,unit_gap_integral p hp]
157   have he : m*m^(p-2)=m^(p-1) := by
158     nth_rw 1 [← Real.rpow_one m]
159     rw [← Real.rpow_add hm]
160     congr 1
161     ring
162   rw [← mul_assoc,he]
163 
164 theorem normalized_gap_integral (p m : ℝ) (hp : p∈Ioo 0 1) (hm : 0 < m) :
165     (Real.sin (Real.pi*p)/Real.pi)*(∫ t in Ioi 0,t^p/(t+m)^2)=p*m^(p-1) := by
166   rw [gap_integral p m hp hm]
167   have hs : Real.sin (Real.pi*p) ≠ 0 := by
168     intro hs
169     have h := sine_factor_positive p hp
170     rw [hs,zero_div] at h
171     exact (lt_irrefl 0) h
172   field_simp
173 
174 end KomorebiPaperVI.BetaNormalization

Back to source controls