FractionalScalarBounds.lean

1 import KomorebiPaperVI.BetaNormalization
2 import Mathlib.Analysis.SpecialFunctions.Integrals.Basic
3 
4 /-! Author: Komorebi P. Exact scalar integrals for the split fractional-defect bound. -/
5 namespace KomorebiPaperVI.FractionalScalarBounds
6 open Set MeasureTheory Real
7 
8 theorem low_integral (p r : ℝ) (hp : 0 < p) (hr : 0 < r) :
9     (∫ t in Ioc 0 r,t^(p-1))=r^p/p := by
10   rw [← intervalIntegral.integral_of_le hr.le,
11     integral_rpow (Or.inl (by linarith : -1 < p-1))]
12   simp [hp.ne']
13 
14 theorem high_integral (p r : ℝ) (hp : p < 1) (hr : 0 < r) :
15     (∫ t in Ioi r,t^(p-2))=r^(p-1)/(1-p) := by
16   rw [integral_Ioi_rpow_of_lt (by linarith : p-2 < -1) hr]
17   have he : p-2+1=p-1 := by ring
18   rw [he,show p-1= -(1-p) by ring,div_neg,neg_div,neg_neg]
19 
20 theorem split_domain (r : ℝ) (hr : 0 ≤ r) : Ioi (0:ℝ)=Ioc 0 r∪Ioi r := by
21   ext t
22   simp only [mem_Ioi,mem_union,mem_Ioc]
23   constructor
24   · intro ht
25     by_cases h : t ≤ r
26     · exact Or.inl ⟨ht,h⟩
27     · exact Or.inr (lt_of_not_ge h)
28   · rintro (h|h)
29     · exact h.1
30     · exact hr.trans_lt h
31 
32 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
33 theorem split_norm_bound (f : ℝ → E) (p c d r : ℝ) (hp : p∈Ioo 0 1) (hr : 0 < r)
34     (hf : IntegrableOn f (Ioi 0))
35     (hlow : ∀ t,0 < t → ‖f t‖ ≤ c*t^(p-1))
36     (hhigh : ∀ t,0 < t → ‖f t‖ ≤ d*t^(p-2)) :
37     ‖∫ t in Ioi 0,f t‖ ≤ c*r^p/p+d*r^(p-1)/(1-p) := by
38   have hf1 := hf.mono_set (Ioc_subset_Ioi_self : Ioc (0:ℝ) r ⊆ Ioi 0)
39   have hf2 := hf.mono_set (Ioi_subset_Ioi hr.le)
40   have hg1 : IntegrableOn (fun t : ℝ => c*t^(p-1)) (Ioc 0 r) := by
41     exact (intervalIntegral.intervalIntegrable_rpow' (by linarith [hp.1] : -1 < p-1)).1.const_mul c
42   have hg2 := (integrableOn_Ioi_rpow_of_lt (by linarith [hp.2] : p-2 < -1) hr).const_mul d
43   have hdis : Disjoint (Ioc (0:ℝ) r) (Ioi r) := by
44     apply disjoint_left.mpr
45     intro t ht hu
46     exact (not_lt_of_ge ht.2) hu
47   rw [split_domain r hr.le,setIntegral_union hdis measurableSet_Ioi hf1 hf2]
48   calc
49     _ ≤ ‖∫ t in Ioc 0 r,f t‖+‖∫ t in Ioi r,f t‖ := norm_add_le _ _
50     _ ≤ (∫ t in Ioc 0 r,c*t^(p-1))+(∫ t in Ioi r,d*t^(p-2)) := by
51       apply add_le_add
52       · exact (norm_integral_le_integral_norm _).trans (setIntegral_mono_on hf1.norm hg1 measurableSet_Ioc (fun t ht => hlow t ht.1))
53       · exact (norm_integral_le_integral_norm _).trans (setIntegral_mono_on hf2.norm hg2 measurableSet_Ioi (fun t ht => hhigh t (hr.trans ht)))
54     _ = _ := by rw [integral_const_mul,integral_const_mul,low_integral p r hp.1 hr,high_integral p r hp.2 hr]; ring
55 
56 theorem optimize_split (p c d : ℝ) (hp : p∈Ioo 0 1) (hc : 0 < c) (hd : 0 < d) :
57     c*(d/c)^p/p+d*(d/c)^(p-1)/(1-p)=c^(1-p)*d^p/(p*(1-p)) := by
58   rw [Real.rpow_sub (div_pos hd hc),Real.rpow_one,Real.div_rpow hd.le hc.le,
59     Real.rpow_sub hc,Real.rpow_one]
60   have hcPow : c^p ≠ 0 := (Real.rpow_pos_of_pos hc p).ne'
61   field_simp [hc.ne',hd.ne',hp.1.ne',(sub_pos.mpr hp.2).ne',hcPow]
62   ring
63 
64 end KomorebiPaperVI.FractionalScalarBounds

Back to source controls