FractionalIntegral.lean

1 import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
2 import Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
3 
4 /-! Author: Komorebi P. A common-measure integral for the actual CFC fractional defect.
5 The explicit sine normalization and the manuscript norm constants remain to be identified. -/
6 namespace KomorebiPaperVI.FractionalIntegral
7 open Set MeasureTheory
8 open scoped NNReal
9 variable {R : Type*} [CStarAlgebra R] [PartialOrder R] [StarOrderedRing R]
10 
11 noncomputable def integrand (a : ℝ≥0) (t : ℝ) (A : R) : R :=
12   cfcₙ (Real.rpowIntegrand₀₁ a t) A
13 
14 theorem common_measure_defect (a : ℝ≥0) (ha : a∈Ioo 0 1) :
15     ∃ μ : Measure ℝ,∀ A B : R,0 ≤ A → 0 ≤ B → ∀ C : R,
16       IntegrableOn (fun t => C*integrand a t A-integrand a t B*C) (Ioi 0) μ ∧
17       C*CFC.nnrpow A a-CFC.nnrpow B a*C=
18         ∫ t in Ioi 0,C*integrand a t A-integrand a t B*C ∂μ := by
19   obtain ⟨μ,hμ⟩ := CFC.exists_measure_nnrpow_eq_integral_cfcₙ_rpowIntegrand₀₁ R ha
20   refine ⟨μ,?_⟩
21   intro A B hA hB C
22   have hiA : IntegrableOn (integrand a · A) (Ioi 0) μ := (hμ A hA).1
23   have hiB : IntegrableOn (integrand a · B) (Ioi 0) μ := (hμ B hB).1
24   have hl : IntegrableOn (fun t => C*integrand a t A) (Ioi 0) μ :=
25     (ContinuousLinearMap.mul ℝ R C).integrable_comp hiA
26   have hr : IntegrableOn (fun t => integrand a t B*C) (Ioi 0) μ :=
27     (ContinuousLinearMap.mul ℝ R).flip C |>.integrable_comp hiB
28   refine ⟨hl.sub hr,?_⟩
29   rw [integral_sub hl hr,integral_const_mul_of_integrable hiA,integral_mul_const_of_integrable hiB]
30   exact congrArg₂ (fun x y : R => C*x-y*C) (hμ A hA).2 (hμ B hB).2
31 
32 theorem scalar_normalizer_positive (a : ℝ) (ha : a∈Ioo 0 1) :
33     0 < ∫ t in Ioi 0,Real.rpowIntegrand₀₁ a t 1 :=
34   Real.integral_rpowIntegrand₀₁_one_pos ha
35 
36 theorem scalar_normalized_representation (a x : ℝ) (ha : a∈Ioo 0 1) (hx : 0 ≤ x) :
37     x^a=(∫ t in Ioi 0,Real.rpowIntegrand₀₁ a t 1)⁻¹*
38       ∫ t in Ioi 0,Real.rpowIntegrand₀₁ a t x :=
39   Real.rpow_eq_const_mul_integral ha hx
40 
41 end KomorebiPaperVI.FractionalIntegral

Back to source controls