NormalizedFractional.lean

1 import KomorebiPaperVI.BetaNormalization
2 import KomorebiPaperVI.FractionalIntegral
3 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
4 
5 /-!
6 Author: Komorebi P.
7 The CFC integration argument adapts Mathlib's Rpow/IntegralRepresentation.lean,
8 Copyright (c) 2025 Frédéric Dupuis, Apache 2.0. Its explicit measure is retained here.
9 -/
10 set_option backward.isDefEq.respectTransparency false
11 namespace KomorebiPaperVI.NormalizedFractional
12 open Set MeasureTheory Real
13 open scoped NNReal ENNReal
14 attribute [local instance] IsStarNormal.instContinuousFunctionalCalculus
15 variable {A : Type*} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
16 
17 noncomputable def coefficient (p : ℝ) : ℝ := Real.sin (Real.pi*p)/Real.pi
18 
19 theorem scalar_measure (p : ℝ≥0) (hp : (p:ℝ)∈Ioo 0 1) :
20     let c : ℝ≥0 := ⟨coefficient p,(by exact (BetaNormalization.sine_factor_positive p hp).le)⟩
21     ∀ x ∈ Ici (0:ℝ), IntegrableOn (fun t => rpowIntegrand₀₁ p t x) (Ioi 0) (c • volume) ∧
22       x^(p:ℝ)=∫ t in Ioi 0,rpowIntegrand₀₁ p t x ∂(c • volume) := by
23   dsimp only
24   intro x hx
25   constructor
26   · unfold IntegrableOn
27     rw [Measure.restrict_smul]
28     exact Integrable.smul_measure_nnreal (integrableOn_rpowIntegrand₀₁_Ioi hp hx)
29   · simp only [Measure.restrict_smul,integral_smul_nnreal_measure,NNReal.smul_def,smul_eq_mul]
30     exact BetaNormalization.scalar_fractional_integral p x hp hx
31 
32 theorem cfc_explicit_measure (p : ℝ≥0) (hp : (p:ℝ)∈Ioo 0 1) (a : A) (ha : 0 ≤ a) :
33     let c : ℝ≥0 := ⟨coefficient p,(by exact (BetaNormalization.sine_factor_positive p hp).le)⟩
34     IntegrableOn (fun t => cfcₙ (rpowIntegrand₀₁ p t) a) (Ioi 0) (c • volume) ∧
35       CFC.nnrpow a p=∫ t in Ioi 0,cfcₙ (rpowIntegrand₀₁ p t) a ∂(c • volume) := by
36   let c : ℝ≥0 := ⟨coefficient p,(by exact (BetaNormalization.sine_factor_positive p hp).le)⟩
37   let μ : Measure ℝ := c • volume
38   have hμ := scalar_measure p hp
39   change IntegrableOn _ _ μ ∧ _
40   nontriviality A
41   have p_pos : 0 < (p : ℝ) := by exact_mod_cast hp.1
42   let f t := rpowIntegrand₀₁ p t
43   let maxr := sSup (quasispectrum ℝ a)
44   have maxr_nonneg : 0 ≤ maxr :=
45     le_csSup_of_le (b := 0) (IsCompact.bddAbove (by grind)) (by simp) (by simp)
46   let bound (t : ℝ) := ‖f t maxr‖
47   have hf : ContinuousOn (Function.uncurry f) (Ioi (0 : ℝ) ×ˢ quasispectrum ℝ a) := by
48     refine continuousOn_rpowIntegrand₀₁_uncurry hp (quasispectrum ℝ a) ?_
49     grind
50   have hbound : ∀ᵐ t ∂μ.restrict (Ioi 0), ∀ z ∈ quasispectrum ℝ a, ‖f t z‖ ≤ bound t := by
51     filter_upwards [ae_restrict_mem measurableSet_Ioi] with t ht
52     intro z hz
53     have hz' : 0 ≤ z := by grind
54     unfold bound f
55     rw [Real.norm_of_nonneg (rpowIntegrand₀₁_nonneg p_pos (le_of_lt ht) hz'),
56         Real.norm_of_nonneg (rpowIntegrand₀₁_nonneg p_pos (le_of_lt ht) maxr_nonneg)]
57     refine rpowIntegrand₀₁_monotoneOn hp (le_of_lt ht) hz' maxr_nonneg ?_
58     exact le_csSup (IsCompact.bddAbove (quasispectrum.isCompact _)) hz
59   have hbound_finite_integral : HasFiniteIntegral bound (μ.restrict (Ioi 0)) := by
60     rw [hasFiniteIntegral_norm_iff]
61     exact (hμ maxr maxr_nonneg).1.2
62   have hmapzero : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), rpowIntegrand₀₁ p x 0 = 0 := by
63     filter_upwards [ae_restrict_mem measurableSet_Ioi]
64     simp
65   refine ⟨?integrable, ?integral⟩
66   case integrable =>
67     exact integrableOn_cfcₙ measurableSet_Ioi _ bound a hf hmapzero hbound hbound_finite_integral
68   case integral => calc
69     a ^ p = cfcₙ (fun r => ∫ t in Ioi 0, rpowIntegrand₀₁ p t r ∂μ) a := by
70       rw [CFC.nnrpow_eq_cfcₙ_real _ _]
71       exact cfcₙ_congr fun r _ ↦ (hμ r (by grind)).2
72     _ = _ := cfcₙ_setIntegral measurableSet_Ioi _ bound a hf hmapzero hbound
73                 hbound_finite_integral ha.isSelfAdjoint
74 
75 theorem cfc_lebesgue_integral (p : ℝ≥0) (hp : (p:ℝ)∈Ioo 0 1) (a : A) (ha : 0 ≤ a) :
76     IntegrableOn (fun t => cfcₙ (rpowIntegrand₀₁ p t) a) (Ioi 0) ∧
77       CFC.nnrpow a p=coefficient p • ∫ t in Ioi 0,cfcₙ (rpowIntegrand₀₁ p t) a := by
78   let c : ℝ≥0 := ⟨coefficient p,by exact (BetaNormalization.sine_factor_positive p hp).le⟩
79   have h := cfc_explicit_measure p hp a ha
80   change IntegrableOn _ _ (c • volume) ∧ _ at h
81   have hc0 : (c:ℝ≥0∞) ≠ 0 := by
82     have hc : c ≠ 0 := by
83       apply NNReal.coe_ne_zero.mp
84       exact (BetaNormalization.sine_factor_positive p hp).ne'
85     exact_mod_cast hc
86   constructor
87   · have hi := h.1
88     unfold IntegrableOn at hi ⊢
89     rw [Measure.restrict_smul] at hi
90     exact (integrable_smul_measure hc0 (by simp)).mp hi
91   · have he := h.2
92     simp only [Measure.restrict_smul,integral_smul_nnreal_measure,NNReal.smul_def] at he
93     convert! he using 1
94 
95 end KomorebiPaperVI.NormalizedFractional

Back to source controls