6.2 One-dimensional power-law operators
This chapter studies power-law integral operators and their spectral representations. It covers exact polynomial formulas and approximation results, with separate treatment of the compactness range and its critical boundary. Equilibrium minimization is outside its scope.
Supporting results: integrals of real powers
For \(\alpha {\gt}-1\) and \(a,b\ge 0\), \(t^\alpha \) is integrable on the open interval between \(a\) and \(b\), all its bases there are positive, and its oriented integral is \(\int _a^b t^\alpha \, dt=(b^{\alpha +1}-a^{\alpha +1})/(\alpha +1)\). Here orientation means multiplying the integral on \((\min (a,b),\max (a,b))\) by \(1\) when \(a\le b\) and by \(-1\) otherwise. For every integer \(n\ge 0\) the polynomial \(t^n\) is integrable on arbitrary real intervals, with \(\int _a^b t^n\, dt=(b^{n+1}-a^{n+1})/(n+1)\).
Lean Formalisation
theorem Real.integrable_rpow_openInterval (α : ↑(Set.Ioi (-1))) (a b : NNReal) :
MeasureTheory.Integrable (fun t => ↑t ^ ↑α) (MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume)Lean proof
/-- Real powers are integrated only at positive bases; endpoints may be zero. -/
theorem integrable_rpow_openInterval (α : Ioi (-1 : ℝ)) (a b : ℝ≥0) :
Integrable (fun t : Ioo (min (a : ℝ) (b : ℝ)) (max (a : ℝ) (b : ℝ)) ↦ t.val^α.val)
(Measure.comap Subtype.val volume) := by
apply (integrableOn_iff_comap_subtypeVal (f := fun t : ℝ ↦ t ^ α.val) measurableSet_Ioo).mp
by_cases h : 0 < max (a : ℝ) (b : ℝ)
· exact ((intervalIntegral.integrableOn_Ioo_rpow_iff h).2 α.property).mono_set
(Ioo_subset_Ioo (le_min a.property b.property) le_rfl)
· have he : Ioo (min (a : ℝ) (b : ℝ)) (max (a : ℝ) (b : ℝ)) = ∅ :=
Ioo_eq_empty_of_le ((le_of_not_gt h).trans (le_min a.property b.property))
rw [he]
exact integrableOn_emptyFor \(\alpha ,x\in \mathbb {R}\), let \(D_x=\{ y\in (-1,1):y\ne x\} \). An input at \((\alpha ,x)\) is a function \(f:D_x\to \mathbb {R}\) for which \(y\mapsto |x-y|^\alpha f(y)\) is integrable. Define
The parameter and input domain allow every existing weighted integral, without assigning a kernel value on the diagonal. Reference: [GCO22, Section 2].
Lean Formalisation
def Real.PowerLawDomain (x : ℝ) : TypeLean definition
/-- The integration points of the power-law kernel, excluding its possible singularity. -/
abbrev PowerLawDomain (x : ℝ) := {y : ℝ // y ∈ Ioo (-1 : ℝ) 1 ∧ y ≠ x}Reference details: Characterisation of the power-law integral and related results
For \(f\) in the power-law domain at exponent \(\alpha \) and point \(x\), \(|x-y|{\gt}0\) for \(y\in D_x=(-1,1)\setminus \{ x\} \), the function \(y\mapsto |x-y|^\alpha f(y)\) is integrable on \(D_x\), and
Lean Formalisation
theorem Real.powerLawDomain_base_pos {x : ℝ} (y : x.PowerLawDomain) : 0 < |x - ↑y|Lean proof
/-- Every kernel base is strictly positive. -/
theorem powerLawDomain_base_pos {x : ℝ} (y : PowerLawDomain x) : 0 < |x-y.val| :=
abs_pos.mpr (sub_ne_zero.mpr y.property.2.symm)For \(\alpha \in \mathbb {R}\) and \(x\ge -1\), an input is a real-valued function on \((-1,x)\) with integrable weighted product \((x-y)^\alpha f(y)\). Define
The collapsed interval at \(x=-1\) is empty.
Lean Formalisation
def Real.PowerLawLeftInput (α : ℝ) (x : ↑(Set.Ici (-1))) : TypeLean definition
/-- Integrable inputs for the left-oriented positive-base kernel. -/
abbrev PowerLawLeftInput (α : ℝ) (x : Ici (-1 : ℝ)) :=
{f : Ioo (-1 : ℝ) x.val → ℝ // Integrable (fun y ↦ (x.val-y.val)^α*f y)
(Measure.comap Subtype.val volume)}Every kernel base is positive, every input has an integrable weighted product, and \(L_\alpha f(x)\) equals the displayed integral.
Lean Formalisation
theorem Real.powerLawLeft_spec {α : ℝ} {x : ↑(Set.Ici (-1))} (f : α.PowerLawLeftInput x) :
(∀ (y : ↑(Set.Ioo (-1) ↑x)), 0 < ↑x - ↑y) ∧
MeasureTheory.Integrable (fun y => (↑x - ↑y) ^ α * ↑f y)
(MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume) ∧
Real.powerLawLeft f =
∫ (y : ↑(Set.Ioo (-1) ↑x)), (↑x - ↑y) ^ α * ↑f y ∂MeasureTheory.Measure.comap Subtype.val MeasureTheory.volumeLean proof
/-- Left input characterization and positive kernel base. -/
theorem powerLawLeft_spec {α : ℝ} {x : Ici (-1 : ℝ)} (f : PowerLawLeftInput α x) :
(∀ y : Ioo (-1 : ℝ) x.val, 0 < x.val-y.val) ∧
Integrable (fun y : Ioo (-1 : ℝ) x.val ↦ (x.val-y.val)^α*f.val y)
(Measure.comap Subtype.val volume) ∧
powerLawLeft f = ∫ y : Ioo (-1 : ℝ) x.val,
(x.val-y.val)^α*f.val y ∂Measure.comap Subtype.val volume :=
⟨fun y ↦ sub_pos.mpr y.property.2, f.property, rfl⟩For \(\alpha \in \mathbb {R}\) and \(x\le 1\), an input is a real-valued function on \((x,1)\) with integrable weighted product \((y-x)^\alpha f(y)\). Define
The collapsed interval at \(x=1\) is empty.
Lean Formalisation
def Real.PowerLawRightInput (α : ℝ) (x : ↑(Set.Iic 1)) : TypeLean definition
/-- Integrable inputs for the right-oriented positive-base kernel. -/
abbrev PowerLawRightInput (α : ℝ) (x : Iic (1 : ℝ)) :=
{f : Ioo x.val (1 : ℝ) → ℝ // Integrable (fun y ↦ (y.val-x.val)^α*f y)
(Measure.comap Subtype.val volume)}Every kernel base is positive, every input has an integrable weighted product, and \(R_\alpha f(x)\) equals the displayed integral.
Lean Formalisation
theorem Real.powerLawRight_spec {α : ℝ} {x : ↑(Set.Iic 1)} (f : α.PowerLawRightInput x) :
(∀ (y : ↑(Set.Ioo (↑x) 1)), 0 < ↑y - ↑x) ∧
MeasureTheory.Integrable (fun y => (↑y - ↑x) ^ α * ↑f y)
(MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume) ∧
Real.powerLawRight f =
∫ (y : ↑(Set.Ioo (↑x) 1)), (↑y - ↑x) ^ α * ↑f y ∂MeasureTheory.Measure.comap Subtype.val MeasureTheory.volumeLean proof
/-- Right input characterization and positive kernel base. -/
theorem powerLawRight_spec {α : ℝ} {x : Iic (1 : ℝ)} (f : PowerLawRightInput α x) :
(∀ y : Ioo x.val (1 : ℝ), 0 < y.val-x.val) ∧
Integrable (fun y : Ioo x.val (1 : ℝ) ↦ (y.val-x.val)^α*f.val y)
(Measure.comap Subtype.val volume) ∧
powerLawRight f = ∫ y : Ioo x.val (1 : ℝ),
(y.val-x.val)^α*f.val y ∂Measure.comap Subtype.val volume :=
⟨fun y ↦ sub_pos.mpr y.property.1, f.property, rfl⟩For \(x\in [-1,1]\), every input in Definition 6.2.2 has integrable left and right restrictions, and its integral equals
For \(\alpha {\gt}-1\) the kernel is integrable, including at \(x=\pm 1\); multiplying by an input continuous on \([-1,1]\) preserves integrability. In particular,
Reflection preserves the full weighted-integrability domain and obeys \(Q_\alpha (f\circ (-\mathrm{id}))(-x)=Q_\alpha f(x)\). This is the unweighted degree-zero base case, not the general weighted hypergeometric formula.
Reference: [GCO22, Section 2].
Lean Formalisation
theorem Real.PowerLawInput.ofContinuous_apply (α : ↑(Set.Ioi (-1))) (x : ↑(Set.Icc (-1) 1)) (f : C(↑(Set.Icc (-1) 1), ℝ))
(y : (↑x).PowerLawDomain) : ↑(Real.PowerLawInput.ofContinuous α x f) y = f ⟨↑y, ⋯⟩Lean proof
/-- The continuous constructor agrees pointwise on the kernel domain. -/
theorem PowerLawInput.ofContinuous_apply (α : Ioi (-1 : ℝ)) (x : Icc (-1 : ℝ) 1)
(f : C(Icc (-1 : ℝ) 1, ℝ)) (y : PowerLawDomain x.val) :
(PowerLawInput.ofContinuous α x f).val y = f ⟨y.val, Ioo_subset_Icc_self y.property.1⟩ := rflReference details: Gegenbauer-weighted functions for power-law integration and related results
Write \(w_\lambda (y)=(1-y^2)^{\lambda -1/2}\) on \((-1,1)\). For \(\alpha {\gt}-1\), \(\lambda {\gt}-1/2\), \(x\in (-1,1)\) and \(f\in C([-1,1],\mathbb {R})\), define \(g(y)=w_\lambda (y)f(y)\) on \(D_x\) as a function in the domain of \(u\mapsto Q_\alpha u(x)\). Taking \(f=1\) gives the weighted constant amplitude; taking \(f=C_n^{(\lambda )}\) for \(n\in \mathbb N\) gives the weighted polynomial modes. At \(x=1\), define \(g(y)=w_\lambda (y)\) on \(D_1\) under the endpoint conditions \(\lambda {\gt}-1/2\) and \(\alpha +\lambda {\gt}-1/2\); no separate lower bound on \(\alpha \) is imposed. Membership in these domains requires the product \(|x-y|^\alpha g(y)\) to be integrable on \(D_x\).
Lean Formalisation
def Real.PowerLawEndpointParameters : TypeLean definition
/-- Endpoint data use the combined singularity exponent, without an unnecessary alpha bound. -/
abbrev PowerLawEndpointParameters := {p : ℝ × ℝ // -(1/2) < p.2 ∧ -(1/2) < p.1+p.2}Let \(w_\lambda (y)=(1-y^2)^{\lambda -1/2}\) on \((-1,1)\). For \(\alpha {\gt}-1\), \(\lambda {\gt}-1/2\), \(x\in (-1,1)\) and \(f\in C([-1,1],\mathbb {R})\), the weighted function in Definition 6.2.9 has value \(w_\lambda (y)f(y)\) for every \(y\in D_x\). The constant-amplitude case is \(w_\lambda (y)\), and the degree-\(n\) case is \(w_\lambda (y)C_n^{(\lambda )}(y)\). At \(x=1\), the constant-amplitude case has the same values on \(D_1\) under \(\lambda {\gt}-1/2\) and \(\alpha +\lambda {\gt}-1/2\). Reflection gives \(w_\lambda (y)\) on \(D_{-1}\) with its weighted integrability preserved. At degree zero, \(w_\lambda C_0^{(\lambda )}=w_\lambda \).
Lean Formalisation
theorem Real.PowerLawInput.gegenbauerContinuous_apply (α : ↑(Set.Ioi (-1))) (lam : ↑(Set.Ioi (-(1 / 2))))
(x : ↑(Set.Ioo (-1) 1)) (f : C(↑(Set.Icc (-1) 1), ℝ)) (y : (↑x).PowerLawDomain) :
↑(Real.PowerLawInput.gegenbauerContinuous α lam x f) y = ↑((Polynomial.gegenbauerWeight ↑lam) ⟨↑y, ⋯⟩) * f ⟨↑y, ⋯⟩Lean proof
/-- Pointwise characterization of the weighted input. -/
theorem PowerLawInput.gegenbauerContinuous_apply (α : Ioi (-1 : ℝ))
(lam : Ioi (-(1/2) : ℝ)) (x : Ioo (-1 : ℝ) 1)
(f : C(Icc (-1 : ℝ) 1, ℝ)) (y : PowerLawDomain x.val) :
(PowerLawInput.gegenbauerContinuous α lam x f).val y =
(gegenbauerWeight lam.val ⟨y.val,y.property.1⟩ : ℝ) *
f ⟨y.val,Ioo_subset_Icc_self y.property.1⟩ := rflLet \(w_\lambda (y)=(1-y^2)^{\lambda -1/2}\). If \(\lambda {\gt}-1/2\) and \(\alpha +\lambda {\gt}-1/2\), the right-endpoint integrand is integrable and
References: the Jacobi Beta integral, [DLMF, 5.12.1], and the weighted operator convention of [GCO22, Section 2].
Lean Formalisation
theorem Real.powerLawIntegral_gegenbauerEndpoint (p : Real.PowerLawEndpointParameters) :
Real.powerLawIntegral (Real.PowerLawInput.gegenbauerEndpoint p) =
2 ^ ((↑p).1 + 2 * (↑p).2) * Real.GammaOn (Real.GammaPoint.ofPos ((↑p).1 + (↑p).2 + 1 / 2) ⋯) *
Real.GammaOn (Real.GammaPoint.ofPos ((↑p).2 + 1 / 2) ⋯) /
Real.GammaOn (Real.GammaPoint.ofPos ((↑p).1 + 2 * (↑p).2 + 1) ⋯)Lean proof
/-- The endpoint formula uses only positive-argument Gamma values. -/
theorem powerLawIntegral_gegenbauerEndpoint (p : PowerLawEndpointParameters) :
powerLawIntegral (.gegenbauerEndpoint p) =
(2 : ℝ)^(p.val.1+2*p.val.2) *
GammaOn (.ofPos (p.val.1+p.val.2+1/2) (by linarith [p.property.2])) *
GammaOn (.ofPos (p.val.2+1/2) (by linarith [p.property.1])) /
GammaOn (.ofPos (p.val.1+2*p.val.2+1) (by linarith [p.property.1,p.property.2])) := by
calc
_ = ∫ y : Ioo (-1 : ℝ) 1,
(jacobiWeight (p.val.1+(p.val.2-1/2)) (p.val.2-1/2) y : ℝ) := by
let W : ℝ → ℝ := fun y ↦ if h : y ∈ Ioo (-1 : ℝ) 1 then
(jacobiWeight (p.val.1+(p.val.2-1/2)) (p.val.2-1/2) ⟨y,h⟩ : ℝ) else 0
have hs : {y : ℝ | y ∈ Ioo (-1 : ℝ) 1 ∧ y ≠ 1} = Ioo (-1 : ℝ) 1 := by
ext y
exact ⟨fun h ↦ h.1, fun h ↦ ⟨h, ne_of_lt h.2⟩⟩
calc
_ = ∫ y : PowerLawDomain 1, W y ∂Measure.comap Subtype.val volume := by
apply integral_congr_ae
filter_upwards [] with y
simp only [PowerLawInput.gegenbauerEndpoint_apply, W, dite_eq_left y.property.1]
exact powerLaw_mul_gegenbauerWeight_one p.val.1 p.val.2 ⟨y.val,y.property.1⟩
_ = ∫ y in {y : ℝ | y ∈ Ioo (-1 : ℝ) 1 ∧ y ≠ 1}, W y :=
integral_subtype_comap (measurableSet_Ioo.inter (measurableSet_singleton (1 : ℝ)).compl) W
_ = _ := by
rw [hs, ← integral_subtype_comap measurableSet_Ioo W]
apply integral_congr_ae
filter_upwards [] with y
simp only [W, dite_eq_left y.property]
_ = _ := by
rw [integral_jacobiWeight (by linarith [p.property.2])
(by linarith [p.property.1])]
simp only [GammaOn, GammaPoint.ofPos]
rw [show p.val.1+(p.val.2-1/2)+(p.val.2-1/2)+1 = p.val.1+2*p.val.2 by ring,
show p.val.1+(p.val.2-1/2)+1 = p.val.1+p.val.2+1/2 by ring,
show p.val.2-1/2+1 = p.val.2+1/2 by ring,
show p.val.1+(p.val.2-1/2)+(p.val.2-1/2)+2 = p.val.1+2*p.val.2+1 by ring]The endpoint condition concerns the combined weight and kernel exponent. Interior integrability has different hypotheses; see Theorem 6.2.12.
If \(\alpha {\gt}-1\), \(\lambda {\gt}-1/2\), and \(-1{\lt}x{\lt}1\), then
is integrable on \(D_x\) whenever \(f\) is continuous on \([-1,1]\). In particular every Gegenbauer mode \(f=C_n^{(\lambda )}\) is admissible, including the degenerate parameter \(\lambda =0\). These are interior hypotheses; the endpoint values have the separate combined-exponent condition above. The left/right fractional-integral decomposition consequently holds for these weighted inputs without additional integrability assumptions.
Reference: [GCO22, Section 2].
Lean Formalisation
theorem Real.continuous_gegenbauerWeightOn (lam : ℝ) : Continuous fun y => ↑((Polynomial.gegenbauerWeight lam) y)Lean proof
/-- Continuity of the density on its actual open domain. -/
theorem continuous_gegenbauerWeightOn (lam : ℝ) :
Continuous (fun y : Ioo (-1 : ℝ) 1 ↦ (Polynomial.gegenbauerWeight lam y : ℝ)) :=
continuous_subtype_val.comp (Polynomial.gegenbauerWeight lam).continuousLet \(\alpha {\gt}-1\), \(\lambda {\gt}-1/2\), \(-1{\lt}x{\lt}1\), and \(w_\lambda (y)=(1-y^2)^{\lambda -1/2}\). Write \(L_\alpha \) and \(R_\alpha \) for the unnormalized left and right power-law integrals. Then
These reductions include \(\lambda =0\).
Reference: [GCO22, Lemma 2.3].
Lean Formalisation
theorem Real.powerLawLeft_gegenbauer_oneOn (α : ↑(Set.Ioi (-1))) (lam : ↑(Set.Ioi (-(1 / 2)))) (x : ↑(Set.Ioo (-1) 1)) :
have α' := ⟨↑α + 1, ⋯⟩;
let xc := ⟨↑x, ⋯⟩;
Real.powerLawLeft (Real.PowerLawInput.left xc (Real.PowerLawInput.gegenbauerMode α lam x 1)) =
2 * ↑lam *
(↑x * Real.powerLawLeft (Real.PowerLawInput.left xc (Real.PowerLawInput.gegenbauerWeight α lam x)) -
Real.powerLawLeft (Real.PowerLawInput.left xc (Real.PowerLawInput.gegenbauerWeight α' lam x)))Lean proof
/-- First mode for the classical left integral. -/
theorem powerLawLeft_gegenbauer_oneOn (α : Ioi (-1 : ℝ))
(lam : Ioi (-(1/2) : ℝ)) (x : Ioo (-1 : ℝ) 1) :
let α' : Ioi (-1 : ℝ) := ⟨α.val+1, by change -1 < α.val+1; linarith [show -1 < α.val from α.property]⟩
let xc : Icc (-1 : ℝ) 1 := ⟨x.val,Ioo_subset_Icc_self x.property⟩
powerLawLeft ((PowerLawInput.gegenbauerMode α lam x 1).left xc) =
2*lam.val*(x.val*powerLawLeft ((PowerLawInput.gegenbauerWeight α lam x).left xc) -
powerLawLeft ((PowerLawInput.gegenbauerWeight α' lam x).left xc)) := by
dsimp only
let ap : Ioi (-1 : ℝ) := ⟨α.val+1,(by linarith [show -1 < α.val from α.property] : (-1 : ℝ) < α.val+1)⟩
let xc : Icc (-1 : ℝ) 1 := ⟨x.val,Ioo_subset_Icc_self x.property⟩
let f0 := (PowerLawInput.gegenbauerWeight α lam x).left xc
let f1 := (PowerLawInput.gegenbauerWeight ap lam x).left xc
have h0 := f0.property
have h1 := f1.property
calc
_ = ∫ y : Ioo (-1 : ℝ) x.val, 2*lam.val*(x.val*((x.val-y.val)^α.val*f0.val y) -
(x.val-y.val)^ap.val*f1.val y) ∂Measure.comap Subtype.val volume := by
apply integral_congr_ae
filter_upwards [] with y
change (x.val-y.val)^α.val*((Polynomial.gegenbauerWeight lam.val _ : ℝ)*
(gegenbauer lam.val 1).eval y.val) =
2*lam.val*(x.val*((x.val-y.val)^α.val*((Polynomial.gegenbauerWeight lam.val _ : ℝ)*1)) -
(x.val-y.val)^(α.val+1)*((Polynomial.gegenbauerWeight lam.val _ : ℝ)*1))
simp only [mul_one,gegenbauer_one,eval_mul,eval_C,eval_X]
rw [rpow_add_one (sub_pos.mpr y.property.2).ne']
ring
_ = _ := by
erw [integral_const_mul,integral_sub (h0.const_mul x.val) h1,integral_const_mul]
rflThe degree-zero hypergeometric formula is Theorem 6.2.25.
For \(x\in \mathbb {R}\), the domain of \(\phi _x\) is \(\{ t\in \mathbb {R}:1-xt\ne 0\} \), and \(\phi _x(t)=(x-t)/(1-xt)\). The rational map also retains all admissible real arguments outside that interval.
Lean Formalisation
def Real.PowerLawMobiusDomain (x : ℝ) : TypeLean definition
/-- The full classical rational domain; the pole has no assigned value. -/
abbrev PowerLawMobiusDomain (x : ℝ) := {t : ℝ // 1-x*t ≠ 0}The map has the stated rational value throughout its domain. For \(x,t\in (-1,1)\), its denominator is positive, it maps \((-1,1)\) onto itself, and \(\phi _x(\phi _x(t))=t\). Its derivative there is \((x^2-1)/(1-xt)^2\). Moreover,
Lean Formalisation
theorem Real.powerLawMobius_apply (x : ℝ) (t : x.PowerLawMobiusDomain) : x.powerLawMobius t = (x - ↑t) / (1 - x * ↑t)Lean proof
theorem powerLawMobius_apply (x : ℝ) (t : PowerLawMobiusDomain x) :
powerLawMobius x t = (x-t.val)/(1-x*t.val) := rflFor \(x\in (-1,1)\) and an integrable real function \(f\) on \((-1,1)\), define its Jacobian-weighted pullback as the integrable input
Lean Formalisation
def Real.powerLawMobiusPullback (x : ↑(Set.Ioo (-1) 1))
(f : MeasureTheory.IntegrableInput (MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume)) :
MeasureTheory.IntegrableInput (MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume)Lean definition
def powerLawMobiusPullback (x : Ioo (-1 : ℝ) 1) (f : IntegrableInput μI) : IntegrableInput μI :=
⟨fun t ↦ ((1-x.val^2)/(1-x.val*t.val)^2)*
f.val ⟨powerLawMobius x.val (.ofInterval x t),powerLawMobius_memOn x t⟩,
integrable_powerLawMobius_pullback x f⟩For \(x\in (-1,1)\) and integrable \(f\) on \((-1,1)\), the pullback is \(t\mapsto (1-x^2)(1-xt)^{-2}f(\phi _x(t))\), and \(\int _{(-1,1)}f=\int _{(-1,1)}(1-x^2)(1-xt)^{-2}f\circ \phi _x\). This applies to every integrable function \(f\), including functions with an integrable interior singularity; no continuity is required.
Lean Formalisation
theorem Real.powerLawMobiusPullback_apply (x : ↑(Set.Ioo (-1) 1))
(f : MeasureTheory.IntegrableInput (MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume))
(t : ↑(Set.Ioo (-1) 1)) :
↑(Real.powerLawMobiusPullback x f) t =
(1 - ↑x ^ 2) / (1 - ↑x * ↑t) ^ 2 * ↑f ⟨(↑x).powerLawMobius (Real.PowerLawMobiusDomain.ofInterval x t), ⋯⟩Lean proof
theorem powerLawMobiusPullback_apply (x : Ioo (-1 : ℝ) 1) (f : IntegrableInput μI)
(t : Ioo (-1 : ℝ) 1) :
(powerLawMobiusPullback x f).val t = ((1-x.val^2)/(1-x.val*t.val)^2)*
f.val ⟨powerLawMobius x.val (.ofInterval x t),powerLawMobius_memOn x t⟩ := rflFor \(\alpha {\gt}-1\), \(\lambda {\gt}-1/2\) and \(x\in (-1,1)\), define on \(D_0=(-1,1)\setminus \{ 0\} \) the function
as an element of the domain of \(u\mapsto Q_\alpha u(0)\); its product with \(|t|^\alpha \) is integrable. All bases of real powers in this expression are positive on \(D_0\).
Lean Formalisation
def Real.PowerLawInput.mobiusWeight (α : ↑(Set.Ioi (-1))) (lam : ↑(Set.Ioi (-(1 / 2)))) (x : ↑(Set.Ioo (-1) 1)) :
(↑α).PowerLawInput 0Lean definition
def PowerLawInput.mobiusWeight (α : Ioi (-1 : ℝ)) (lam : Ioi (-(1/2) : ℝ))
(x : Ioo (-1 : ℝ) 1) : PowerLawInput α.val 0 := by
refine ⟨fun t ↦ (Polynomial.gegenbauerWeight lam.val ⟨t.val,t.property.1⟩ : ℝ)/
(1-x.val*t.val)^(α.val+2*lam.val+1), ?_⟩
let F : C(Icc (-1 : ℝ) 1,ℝ) := ⟨fun t ↦ 1/(1-x.val*t.val)^(α.val+2*lam.val+1),by
apply continuous_const.div
((continuous_const.sub (continuous_const.mul continuous_subtype_val)).rpow_const
(fun t ↦ Or.inl (powerLawMobius_den_pos_closed x t).ne'))
intro t
exact (rpow_pos_of_pos (powerLawMobius_den_pos_closed x t) _).ne'⟩
have hi := (PowerLawInput.gegenbauerContinuous α lam ⟨0,by constructor <;> norm_num⟩ F).property
convert hi using 1
funext t
change |0-t.val|^α.val*((Polynomial.gegenbauerWeight lam.val _ : ℝ)/_) =
|0-t.val|^α.val*((Polynomial.gegenbauerWeight lam.val _ : ℝ)*(1/_))
ringFor \(\alpha {\gt}-1\), \(\lambda {\gt}-1/2\) and \(x\in (-1,1)\), the function
is the weighted function of Definition 6.2.18. Its product \(|t|^\alpha g(t)\) is integrable on \(D_0\).
Lean Formalisation
theorem Real.PowerLawInput.mobiusWeight_apply (α : ↑(Set.Ioi (-1))) (lam : ↑(Set.Ioi (-(1 / 2)))) (x : ↑(Set.Ioo (-1) 1))
(t : Real.PowerLawDomain 0) :
↑(Real.PowerLawInput.mobiusWeight α lam x) t =
↑((Polynomial.gegenbauerWeight ↑lam) ⟨↑t, ⋯⟩) / (1 - ↑x * ↑t) ^ (↑α + 2 * ↑lam + 1)Lean proof
theorem PowerLawInput.mobiusWeight_apply (α : Ioi (-1 : ℝ)) (lam : Ioi (-(1/2) : ℝ))
(x : Ioo (-1 : ℝ) 1) (t : PowerLawDomain 0) :
(PowerLawInput.mobiusWeight α lam x).val t =
(Polynomial.gegenbauerWeight lam.val ⟨t.val,t.property.1⟩ : ℝ)/
(1-x.val*t.val)^(α.val+2*lam.val+1) := rflFor \(\alpha {\gt}-1\), \(\lambda {\gt}-1/2\) and \(-1{\lt}x{\lt}1\), the map \(\phi _x(t)=(x-t)/(1-xt)\) is an involution of \((-1,1)\) with absolute Jacobian \((1-x^2)/(1-xt)^2\). Consequently,
Both integrals are classical and integrable. The substitution holds for every integrable input by Theorem 6.2.17. The pointwise transformed-kernel identity holds for all real \(\alpha ,\lambda \) on \(D_0\); the integral identity uses the stated integrability range. No value of a singular kernel at \(t=0\) is asserted. Reference: the degree-zero operator in [GCO22, Section 2].
Lean Formalisation
theorem Real.powerLawMobius_gegenbauer_integrandOn (α lam : ℝ) (x : ↑(Set.Ioo (-1) 1)) (t : Real.PowerLawDomain 0) :
(1 - ↑x ^ 2) / (1 - ↑x * ↑t) ^ 2 *
(|↑x - (↑x).powerLawMobius (Real.PowerLawMobiusDomain.ofInterval x ⟨↑t, ⋯⟩)| ^ α *
↑((Polynomial.gegenbauerWeight lam)
⟨(↑x).powerLawMobius (Real.PowerLawMobiusDomain.ofInterval x ⟨↑t, ⋯⟩), ⋯⟩)) =
(1 - ↑x ^ 2) ^ (α + lam + 1 / 2) *
(|↑t| ^ α * ↑((Polynomial.gegenbauerWeight lam) ⟨↑t, ⋯⟩) / (1 - ↑x * ↑t) ^ (α + 2 * lam + 1))Lean proof
theorem powerLawMobius_gegenbauer_integrandOn (α lam : ℝ)
(x : Ioo (-1 : ℝ) 1) (t : PowerLawDomain 0) :
((1-x.val^2)/(1-x.val*t.val)^2)*
(|x.val-powerLawMobius x.val (.ofInterval x ⟨t.val,t.property.1⟩)|^α *
(Polynomial.gegenbauerWeight lam
⟨powerLawMobius x.val (.ofInterval x ⟨t.val,t.property.1⟩),
powerLawMobius_memOn x ⟨t.val,t.property.1⟩⟩ : ℝ)) =
(1-x.val^2)^(α+lam+1/2)*
(|t.val|^α*(Polynomial.gegenbauerWeight lam ⟨t.val,t.property.1⟩ : ℝ)/
(1-x.val*t.val)^(α+2*lam+1)) := by
simp only [Polynomial.gegenbauerWeight_apply,powerLawMobius,PowerLawMobiusDomain.ofInterval]
have hx := x.property
have ht := t.property.1
have hA : 0 < 1-x.val^2 := by nlinarith [hx.1,hx.2]
have hB : 0 < 1-t.val^2 := by nlinarith [ht.1,ht.2]
have hD := powerLawMobius_den_pos hx ht
rw [sub_powerLawMobius hx ht,one_sub_powerLawMobius_sq hx ht,
abs_div,abs_mul,abs_of_pos hA,abs_of_pos hD,
div_rpow (mul_nonneg (abs_nonneg t.val) hA.le) hD.le,
mul_rpow (abs_nonneg t.val) hA.le,
div_rpow (mul_nonneg hA.le hB.le) (sq_nonneg _),mul_rpow hA.le hB.le]
rw [show α+lam+1/2 = 1+α+(lam-1/2) by ring,
show α+2*lam+1 = 2+α+2*(lam-1/2) by ring,
rpow_add hA,rpow_add hA,rpow_one,
rpow_add hD,rpow_add hD,rpow_mul hD.le]
norm_cast
simp only [mul_inv_rev,div_eq_mul_inv]
ringLet \(\alpha {\gt}-1\), \(\lambda {\gt}-1/2\), \(-1{\lt}x{\lt}1\), and put
The left and right weighted fractional integrals are, respectively, \(A(1+x)^pH((1+x)/2)\) and \(A(1-x)^pH((1-x)/2)\). In particular,
Both Gauss arguments lie in \((0,1)\). This evaluates the full degree-zero operator throughout its natural interior range, using the classical real Gauss function. Theorem 6.2.25 gives the equivalent single Gauss value at \(x^2\). References: [GCO22, Section 2]; [DLMF, 15.6.1].
Lean Formalisation
theorem Real.powerLawLeft_gegenbauerWeight_hypergeometricOn (α : ↑(Set.Ioi (-1))) (lam : ↑(Set.Ioi (-(1 / 2))))
(x : ↑(Set.Ioo (-1) 1)) :
have c := Real.GammaPoint.ofPos (↑α + ↑lam + 3 / 2) ⋯;
have p := GaussParameters.ofNoPole (1 / 2 - ↑lam) (↑lam + 1 / 2) ↑c ⋯;
have z := ⟨(↑x + 1) / 2, ⋯⟩;
Real.powerLawLeft (Real.PowerLawInput.left ⟨↑x, ⋯⟩ (Real.PowerLawInput.gegenbauerWeight α lam x)) =
2 ^ (↑lam - 1 / 2) * (↑x + 1) ^ (↑α + ↑lam + 1 / 2) *
(Real.GammaOn (Real.GammaPoint.ofPos (↑lam + 1 / 2) ⋯) * Real.GammaOn (Real.GammaPoint.ofPos (↑α + 1) ⋯) /
Real.GammaOn c *
ordinaryHypergeometricOn p (GaussSeriesPoint.ofUnitDisk p z))Lean proof
/-- Classical left Gauss formula, with the weighted input restricted to its side. -/
theorem powerLawLeft_gegenbauerWeight_hypergeometricOn (α : Ioi (-1 : ℝ))
(lam : Ioi (-(1/2) : ℝ)) (x : Ioo (-1 : ℝ) 1) :
let c := GammaPoint.ofPos (α.val+lam.val+3/2)
(by linarith [show -1 < α.val from α.property, show -(1/2) < lam.val from lam.property])
let p := GaussParameters.ofNoPole (1/2-lam.val) (lam.val+1/2) c.val c.property
let z : Metric.ball (0 : ℝ) 1 := ⟨(x.val+1)/2, by
rw [Metric.mem_ball, dist_zero_right, Real.norm_eq_abs, abs_lt]
constructor <;> linarith [x.property.1,x.property.2]⟩
powerLawLeft ((PowerLawInput.gegenbauerWeight α lam x).left ⟨x.val,Ioo_subset_Icc_self x.property⟩) =
(2 : ℝ)^(lam.val-1/2)*(x.val+1)^(α.val+lam.val+1/2) *
((GammaOn (.ofPos (lam.val+1/2) (by linarith [show -(1/2) < lam.val from lam.property])) *
GammaOn (.ofPos (α.val+1) (by linarith [show -1 < α.val from α.property])) / GammaOn c) *
ordinaryHypergeometricOn p (.ofUnitDisk p z)) := by
dsimp only
let bp : Ioi (0 : ℝ) := ⟨lam.val+1/2, (by linarith [show -(1/2) < lam.val from lam.property] : (0 : ℝ) < lam.val+1/2)⟩
let dp : Ioi (0 : ℝ) := ⟨α.val+1, (by linarith [show -1 < α.val from α.property] : (0 : ℝ) < α.val+1)⟩
let z : Metric.ball (0 : ℝ) 1 := ⟨(x.val+1)/2, by
rw [Metric.mem_ball,dist_zero_right,Real.norm_eq_abs,abs_lt]
constructor <;> linarith [x.property.1,x.property.2]⟩
have hE := (integral_eulerHypergeometricOn (1/2-lam.val) bp dp z).2
have hv : powerLawLeft ((PowerLawInput.gegenbauerWeight α lam x).left ⟨x.val,Ioo_subset_Icc_self x.property⟩) =
(2 : ℝ)^(lam.val-1/2)*(x.val+1)^(α.val+lam.val+1/2) *
∫ t : Ioo (0 : ℝ) 1, t.val^(bp.val-1)*(1-t.val)^(dp.val-1)/
(1-z.val*t.val)^(1/2-lam.val) ∂Measure.comap Subtype.val volume := by
rw [left_affine_integral α.val x,← integral_const_mul,← integral_const_mul]
apply integral_congr_ae
filter_upwards [] with t
change (x.val+1) * ((x.val-((x.val+1)*t.val-1))^α.val *
(((Polynomial.gegenbauerWeight lam.val _) : ℝ) * 1)) = _
rw [mul_one,Polynomial.gegenbauerWeight_apply]
simpa only [bp,dp,z,add_sub_cancel_right,
show lam.val+1/2-1 = lam.val-1/2 by ring] using
gegenbauer_affine_algebra α.val lam.val x t
have hc : (lam.val+1/2)+(α.val+1) = α.val+lam.val+3/2 := by ring
let cp := GammaPoint.ofPos (α.val+lam.val+3/2)
(by linarith [show -1 < α.val from α.property,show -(1/2) < lam.val from lam.property])
let pg := GaussParameters.ofNoPole (1/2-lam.val) (lam.val+1/2) cp.val cp.property
have hp : eulerGaussParameters (1/2-lam.val) bp dp = pg := by
simp only [eulerGaussParameters,GaussParameters.ofNoPole,bp,dp,pg,cp,GammaPoint.ofPos,hc]
have hg := congrArg (fun p : GaussParameters ℝ ↦ ordinaryHypergeometricOn p (.ofUnitDisk p z)) hp
rw [hv,hE,hg]
simp only [bp,dp,z,pg,cp,GammaPoint.ofPos,hc]For real \(a\), \(p{\gt}-1\) and \(|x|{\lt}1\),
This includes all terminating cases. A reusable second-order linear ODE uniqueness theorem compares the transformed functions and their initial data; all Gauss arguments remain inside the series disk. Reference: quadratic transformations in [DLMF, 15.8] and the operator formula in [GCO22, Section 2].
Lean Formalisation
theorem eqOn_of_secondOrder_linear_ode {a b t₀ : ℝ} {A B f f₁ g g₁ : ℝ → ℝ} (hA : ContinuousOn A (Set.Icc a b))
(hB : ContinuousOn B (Set.Icc a b)) (ht : t₀ ∈ Set.Ioo a b) (hf : ContinuousOn f (Set.Icc a b))
(hf₁ : ContinuousOn f₁ (Set.Icc a b)) (hg : ContinuousOn g (Set.Icc a b)) (hg₁ : ContinuousOn g₁ (Set.Icc a b))
(hfd : ∀ t ∈ Set.Ioo a b, HasDerivAt f (f₁ t) t) (hfd₁ : ∀ t ∈ Set.Ioo a b, HasDerivAt f₁ (A t * f t + B t * f₁ t) t)
(hgd : ∀ t ∈ Set.Ioo a b, HasDerivAt g (g₁ t) t) (hgd₁ : ∀ t ∈ Set.Ioo a b, HasDerivAt g₁ (A t * g t + B t * g₁ t) t)
(he : f t₀ = g t₀) (he₁ : f₁ t₀ = g₁ t₀) : Set.EqOn f g (Set.Icc a b)Lean proof
/-- Two solutions of a scalar linear second-order equation with continuous
coefficients agree when their values and first derivatives agree initially. -/
theorem eqOn_of_secondOrder_linear_ode {a b t₀ : ℝ} {A B f f₁ g g₁ : ℝ → ℝ}
(hA : ContinuousOn A (Icc a b)) (hB : ContinuousOn B (Icc a b))
(ht : t₀ ∈ Ioo a b)
(hf : ContinuousOn f (Icc a b)) (hf₁ : ContinuousOn f₁ (Icc a b))
(hg : ContinuousOn g (Icc a b)) (hg₁ : ContinuousOn g₁ (Icc a b))
(hfd : ∀ t ∈ Ioo a b, HasDerivAt f (f₁ t) t)
(hfd₁ : ∀ t ∈ Ioo a b, HasDerivAt f₁ (A t*f t+B t*f₁ t) t)
(hgd : ∀ t ∈ Ioo a b, HasDerivAt g (g₁ t) t)
(hgd₁ : ∀ t ∈ Ioo a b, HasDerivAt g₁ (A t*g t+B t*g₁ t) t)
(he : f t₀ = g t₀) (he₁ : f₁ t₀ = g₁ t₀) : EqOn f g (Icc a b) := by
let v : ℝ → (ℝ × ℝ) →L[ℝ] (ℝ × ℝ) := fun t ↦
(ContinuousLinearMap.snd ℝ ℝ ℝ).prod
(A t • ContinuousLinearMap.fst ℝ ℝ ℝ + B t • ContinuousLinearMap.snd ℝ ℝ ℝ)
have hv : ContinuousOn v (Icc a b) := by
have he : v = fun t ↦
(ContinuousLinearMap.snd ℝ ℝ ℝ).prod (0 : (ℝ × ℝ) →L[ℝ] ℝ) +
A t • (0 : (ℝ × ℝ) →L[ℝ] ℝ).prod (ContinuousLinearMap.fst ℝ ℝ ℝ) +
B t • (0 : (ℝ × ℝ) →L[ℝ] ℝ).prod (ContinuousLinearMap.snd ℝ ℝ ℝ) := by
funext t
ext <;> simp [v]
rw [he]
fun_prop
obtain ⟨C, hC⟩ := isCompact_Icc.exists_bound_of_continuousOn hv
let K : ℝ≥0 := ⟨max C 0, le_max_right _ _⟩
have hLip (t : ℝ) (ht' : t ∈ Ioo a b) :
LipschitzOnWith K (v t) (Set.univ : Set (ℝ × ℝ)) := by
apply ((v t).lipschitzWith.weaken ?_).lipschitzOnWith
exact_mod_cast (hC t (Ioo_subset_Icc_self ht')).trans (le_max_left C 0)
have hu := ODE_solution_unique_of_mem_Icc hLip ht
(hf.prodMk hf₁) (fun t ht' ↦ (hfd t ht').prodMk (hfd₁ t ht'))
(fun _ _ ↦ Set.mem_univ _) (hg.prodMk hg₁)
(fun t ht' ↦ (hgd t ht').prodMk (hgd₁ t ht'))
(fun _ _ ↦ Set.mem_univ _) (Prod.ext he he₁)
intro t ht'
exact congrArg Prod.fst (hu ht')For \(k\in \mathbb N\) and admissible \((a,-k,c)\), define
Admissibility allows earlier termination by the other numerator and termination before a later denominator pole. Reference: [DLMF, 15.2.4–15.2.5].
Lean Formalisation
def TerminatingGaussParameters.{u_2} (K : Type u_2) [RCLike K] (k : ℕ) : Type u_2Lean definition
/-- Admissible terminating Gauss parameters, retaining possible earlier termination. -/
abbrev TerminatingGaussParameters (K : Type*) [RCLike K] (k : ℕ) :=
{p : GaussParameters K // p.b = -(k : K)}Every non-pole denominator parameter gives admissible terminating data. For all admissible \((a,-k,c)\), the classical Gauss function equals \(H_k(a,c;z)\) at every argument \(z\), and \(\deg H_k\le k\). The bound permits earlier termination. Reference: [DLMF, 15.2.4–15.2.5].
Lean Formalisation
theorem ordinaryHypergeometric_eq_eval_polynomial.{u_1} {K : Type u_1} [RCLike K] (k : ℕ) (p : TerminatingGaussParameters K k)
(z : K) :
ordinaryHypergeometricOn (↑p) (GaussSeriesPoint.ofTerminating (↑p) k ⋯ z) =
Polynomial.eval z (ordinaryHypergeometricPolynomial k p)Lean proof
/-- The classical terminating function equals its polynomial at every argument. -/
theorem ordinaryHypergeometric_eq_eval_polynomial (k : ℕ)
(p : TerminatingGaussParameters K k) (z : K) :
ordinaryHypergeometricOn p.val (.ofTerminating p.val k (Or.inr p.property) z) =
(ordinaryHypergeometricPolynomial k p).eval z := by
rw [ordinaryHypergeometricOn_terminating]
simp only [ordinaryHypergeometricPolynomial, Polynomial.eval_finsetSum,
Polynomial.eval_mul, Polynomial.eval_C, Polynomial.eval_pow, Polynomial.eval_X]For \(\alpha {\gt}-1\), \(\lambda {\gt}-1/2\), and \(-1{\lt}x{\lt}1\),
The full natural parameter range is retained, including terminating and nonterminating series. Reference: [GCO22, Section 2].
Lean Formalisation
theorem Real.powerLawIntegral_gegenbauerWeight_originOn (α : ↑(Set.Ioi (-1))) (lam : ↑(Set.Ioi (-(1 / 2)))) :
Real.powerLawIntegral
(Real.PowerLawInput.gegenbauerWeight α lam ⟨0, Real.powerLawIntegral_gegenbauerWeight_originOn._proof_1⟩) =
Real.GammaOn (Real.GammaPoint.ofPos ((↑α + 1) / 2) ⋯) * Real.GammaOn (Real.GammaPoint.ofPos (↑lam + 1 / 2) ⋯) /
Real.GammaOn (Real.GammaPoint.ofPos (↑lam + ↑α / 2 + 1) ⋯)Lean proof
/-- The origin value contains only positive Gamma arguments. -/
theorem powerLawIntegral_gegenbauerWeight_originOn (α : Ioi (-1 : ℝ))
(lam : Ioi (-(1/2) : ℝ)) :
powerLawIntegral (.gegenbauerWeight α lam ⟨0, by constructor <;> norm_num⟩) =
GammaOn (.ofPos ((α.val+1)/2) (by linarith [show -1 < α.val from α.property])) *
GammaOn (.ofPos (lam.val+1/2) (by linarith [show -(1/2) < lam.val from lam.property])) /
GammaOn (.ofPos (lam.val+α.val/2+1) (by linarith [show -1 < α.val from α.property,show -(1/2) < lam.val from lam.property])) := by
let bp : Ioi (0 : ℝ) := ⟨(α.val+1)/2, (by linarith [show -1 < α.val from α.property] : (0 : ℝ) < (α.val+1)/2)⟩
let dp : Ioi (0 : ℝ) := ⟨lam.val+1/2, (by linarith [show -(1/2) < lam.val from lam.property] : (0 : ℝ) < lam.val+1/2)⟩
have hE := integral_eulerHypergeometricOn (0 : ℝ) bp dp ⟨0,by simp⟩
simp only [zero_mul,sub_zero,rpow_zero,div_one,
gauss_zero,mul_one] at hE
let f : IntegrableInput (volume : Measure (Ioo (0 : ℝ) 1)) :=
⟨fun u ↦ u.val^(bp.val-1)*(1-u.val)^(dp.val-1),hE.1⟩
have hs := integral_unitInterval_sq f
let x0 : Ioo (-1 : ℝ) 1 := ⟨0,by constructor <;> norm_num⟩
let u := PowerLawInput.gegenbauerWeight α lam x0
have hchange : (∫ s : Ioo (0 : ℝ) 1, f.val s) =
2*powerLawRight (u.right ⟨0,by constructor <;> norm_num⟩) := by
rw [hs.2]
change _ = 2*(∫ r : Ioo (0 : ℝ) 1, _ ∂Measure.comap Subtype.val volume)
rw [← integral_const_mul]
apply integral_congr_ae
filter_upwards [] with r
change 2*r.val*((r.val^2)^(bp.val-1)*(1-r.val^2)^(dp.val-1)) =
2*((r.val-0)^α.val*(((Polynomial.gegenbauerWeight lam.val _) : ℝ)*1))
rw [mul_one,sub_zero,Polynomial.gegenbauerWeight_apply]
have he : (r.val^2)^(bp.val-1) = r.val^(α.val-1) := by
rw [show r.val^2 = r.val^(2 : ℝ) by norm_cast,← rpow_mul r.property.1.le]
congr 1
dsimp only [bp]
ring
rw [he,show dp.val-1 = lam.val-1/2 by dsimp only [dp]; ring,
show r.val^α.val = r.val^(α.val-1)*r.val by
rw [← rpow_add_one r.property.1.ne',sub_add_cancel]]
ring
have hsplit := powerLawIntegral_eq_left_add_right ⟨0,by constructor <;> norm_num⟩ u
have hlr : powerLawLeft (u.left ⟨0,by constructor <;> norm_num⟩) =
powerLawRight (u.right ⟨0,by constructor <;> norm_num⟩) := by
dsimp only [u]
erw [powerLawLeft_gegenbauerWeight_hypergeometricOn α lam x0,powerLawRight_gegenbauerWeight_hypergeometricOn α lam x0]
simp only [x0,zero_add,sub_zero]
rw [hlr,← two_mul] at hsplit
rw [hsplit,← hchange]
change (∫ s : Ioo (0 : ℝ) 1, s.val^(bp.val-1)*(1-s.val)^(dp.val-1)
∂Measure.comap Subtype.val volume) = _
rw [hE.2]
simp only [bp,dp,show (α.val+1)/2+(lam.val+1/2) = lam.val+α.val/2+1 by ring]Apply the even quadratic transformation to the two-value formula.
The Beta integral at \(x=0\) fixes the normalization.
Let \(\alpha {\gt}-1\), \(\lambda {\gt}-1/2\), and \(w_\lambda (y)=(1-y^2)^{\lambda -1/2}\). For continuous amplitudes \(f,g\) on \([-1,1]\) with \(|f-g|\le \varepsilon \) there,
The corresponding absolute bound holds for every function \(u\) in the domain of \(v\mapsto Q_\alpha v(x)\) satisfying \(|u(y)|\le \varepsilon w_\lambda (y)\) on \(D_x\), with \(\varepsilon \ge 0\). More generally, two functions \(u,v\) in this domain satisfying \(|u-v|\le \varepsilon w_\lambda \) obey the same difference bound. Thus bounded amplitudes are included whenever their weighted kernel is integrable; continuous amplitudes satisfy this automatically. The mass \(Q_\alpha w_\lambda \) is continuous on \((-1,1)\) and bounded above by a positive constant on every compact subset. No polynomial compatibility condition is required.
Lean Formalisation
theorem Real.abs_powerLawIntegral_le_weightedMass (α : ↑(Set.Ioi (-1))) (lam : ↑(Set.Ioi (-(1 / 2)))) (x : ↑(Set.Ioo (-1) 1))
(u : (↑α).PowerLawInput ↑x) (ε : NNReal)
(hu : ∀ (y : (↑x).PowerLawDomain), |↑u y| ≤ ↑ε * ↑((Polynomial.gegenbauerWeight ↑lam) ⟨↑y, ⋯⟩)) :
|Real.powerLawIntegral u| ≤ ↑ε * Real.powerLawIntegral (Real.PowerLawInput.gegenbauerWeight α lam x)Lean proof
theorem abs_powerLawIntegral_le_weightedMass (α : Ioi (-1 : ℝ))
(lam : Ioi (-(1/2) : ℝ)) (x : Ioo (-1 : ℝ) 1)
(u : PowerLawInput α.val x.val) (ε : ℝ≥0)
(hu : ∀ y, |u.val y| ≤ (ε : ℝ) * (gegenbauerWeight lam.val ⟨y.val,y.property.1⟩ : ℝ)) :
|powerLawIntegral u| ≤ (ε : ℝ) * powerLawIntegral (.gegenbauerWeight α lam x) := by
have hi := (PowerLawInput.gegenbauerWeight α lam x).property.const_mul (ε : ℝ)
unfold powerLawIntegral
rw [← integral_const_mul]
rw [← Real.norm_eq_abs]
apply norm_integral_le_of_norm_le hi
apply Filter.Eventually.of_forall
intro y
have hn : 0 ≤ |x.val-y.val|^α.val := rpow_nonneg (abs_nonneg _) _
simpa only [Real.norm_eq_abs, abs_mul, abs_of_nonneg hn,
PowerLawInput.gegenbauerWeight_apply, mul_left_comm] using
mul_le_mul_of_nonneg_left (hu y) hnUnder the preceding parameter hypotheses, if continuous amplitudes \(f_n\) converge uniformly to a continuous \(f\) on \([-1,1]\), then \(Q_\alpha (w_\lambda f_n)\) converges uniformly to \(Q_\alpha (w_\lambda f)\) on every compact subset of \((-1,1)\). For each such compact set and each positive output tolerance, a polynomial amplitude achieves that tolerance. For a second power \(\beta {\gt}-1\) and real \(a,b\), the same input error \(\varepsilon \) controls the output error for \(aQ_\alpha +bQ_\beta \) by
Both powers use the same weight and amplitudes; neither needs compatibility. These are interior approximation statements, not endpoint convergence or finite bandwidth claims.
Lean Formalisation
theorem Real.tendstoUniformlyOn_powerLaw_gegenbauerContinuous (α : ↑(Set.Ioi (-1))) (lam : ↑(Set.Ioi (-(1 / 2))))
(f : C(↑(Set.Icc (-1) 1), ℝ)) (u : ℕ → C(↑(Set.Icc (-1) 1), ℝ))
(hconv : TendstoUniformly (fun n y => (u n) y) (⇑f) Filter.atTop) {K : Set ↑(Set.Ioo (-1) 1)} (hK : IsCompact K) :
TendstoUniformlyOn (fun n x => Real.powerLawIntegral (Real.PowerLawInput.gegenbauerContinuous α lam x (u n)))
(fun x => Real.powerLawIntegral (Real.PowerLawInput.gegenbauerContinuous α lam x f)) Filter.atTop KLean proof
theorem tendstoUniformlyOn_powerLaw_gegenbauerContinuous (α : Ioi (-1 : ℝ))
(lam : Ioi (-(1/2) : ℝ)) (f : C(Icc (-1 : ℝ) 1, ℝ))
(u : ℕ → C(Icc (-1 : ℝ) 1, ℝ))
(hconv : TendstoUniformly (fun n y ↦ u n y) f atTop)
{K : Set (Ioo (-1 : ℝ) 1)} (hK : IsCompact K) :
TendstoUniformlyOn
(fun n x ↦ powerLawIntegral (.gegenbauerContinuous α lam x (u n)))
(fun x ↦ powerLawIntegral (.gegenbauerContinuous α lam x f)) atTop K := by
obtain ⟨M,hM,hb⟩ := exists_powerLawIntegral_weightedMass_bound α lam hK
apply Metric.tendstoUniformlyOn_iff.mpr
intro ε hε
filter_upwards [Metric.tendstoUniformly_iff.mp hconv (ε/(2*M)) (by positivity)] with n hn x hx
have he := abs_powerLawIntegral_gegenbauerContinuous_sub_le α lam x f (u n)
⟨ε/(2*M), by positivity⟩ (fun y ↦ (show |f y-u n y| < ε/(2*M) from by
simpa only [Real.dist_eq] using hn y).le)
rw [Real.dist_eq]
calc
_ ≤ (ε/(2*M))*powerLawIntegral (.gegenbauerWeight α lam x) := he
_ ≤ (ε/(2*M))*M := mul_le_mul_of_nonneg_left (hb x hx) (by positivity)
_ < ε := by field_simp; nlinarithTake \(\alpha {\gt}-1\), \(\lambda {\gt}-1/2\) and \(\alpha +\lambda {\gt}-1/2\). For \(x\in [-1,1]\) and \(f\in C([-1,1],\mathbb {R})\), define the functions \(y\mapsto w_\lambda (y)f(y)\) and \(y\mapsto w_\lambda (y)\) on \(D_x\) as elements of the domain of \(u\mapsto Q_\alpha u(x)\), which requires their products with \(|x-y|^\alpha \) to be integrable on \(D_x\). No value of a singular density is assigned on the excluded endpoints or diagonal.
Lean Formalisation
def Real.PowerLawClosedParameters : TypeLean definition
abbrev PowerLawClosedParameters := {p : ℝ × ℝ // -1 < p.1 ∧ -(1/2) < p.2 ∧ -(1/2) < p.1+p.2}Suppose \(\alpha {\gt}-1\), \(\lambda {\gt}-1/2\) and \(\alpha +\lambda {\gt}-1/2\). For every \(x\in [-1,1]\) and \(f\in C([-1,1],\mathbb {R})\), the weighted functions of Definition 6.2.28 are \(w_\lambda (y)f(y)\) and \(w_\lambda (y)\) on \(D_x\); their products with \(|x-y|^\alpha \) are integrable. This includes both endpoints. At a single endpoint, the more general combined-exponent domain of Definition 6.2.9 remains available; the three inequalities here give one domain valid for all \(x\in [-1,1]\).
Lean Formalisation
theorem Real.PowerLawInput.gegenbauerContinuousClosed_apply (p : Real.PowerLawClosedParameters) (x : ↑(Set.Icc (-1) 1))
(f : C(↑(Set.Icc (-1) 1), ℝ)) (y : (↑x).PowerLawDomain) :
↑(Real.PowerLawInput.gegenbauerContinuousClosed p x f) y = ↑((Polynomial.gegenbauerWeight (↑p).2) ⟨↑y, ⋯⟩) * f ⟨↑y, ⋯⟩Lean proof
theorem PowerLawInput.gegenbauerContinuousClosed_apply (p : PowerLawClosedParameters)
(x : Icc (-1 : ℝ) 1) (f : C(Icc (-1 : ℝ) 1, ℝ)) (y : PowerLawDomain x.val) :
(PowerLawInput.gegenbauerContinuousClosed p x f).val y =
(Polynomial.gegenbauerWeight p.val.2 ⟨y.val,y.property.1⟩ : ℝ)*
f ⟨y.val,Ioo_subset_Icc_self y.property.1⟩ := rflAssume \(\alpha {\gt}-1\), \(\lambda {\gt}-1/2\) and \(\alpha +\lambda {\gt}-1/2\). Then \(|x-y|^\alpha w_\lambda (y)\) is integrable on \(D_x=(-1,1)\setminus \{ x\} \) for every \(x\in [-1,1]\), including both endpoint choices of \(x\). Multiplication by a continuous amplitude preserves this integrability. If \(f,g\) are continuous on \([-1,1]\) and \(|f-g|\le \varepsilon \), then
The absolute bound also holds for every integrable input \(u\) on \(D_x\) with \(|u|\le \varepsilon w_\lambda \), where \(\varepsilon \ge 0\). Two integrable inputs with \(|u-v|\le \varepsilon w_\lambda \) satisfy the same difference bound.
Lean Formalisation
theorem Real.abs_powerLawIntegral_le_weightedMassClosed (p : Real.PowerLawClosedParameters) (x : ↑(Set.Icc (-1) 1))
(u : (↑p).1.PowerLawInput ↑x) (ε : NNReal)
(hu : ∀ (y : (↑x).PowerLawDomain), |↑u y| ≤ ↑ε * ↑((Polynomial.gegenbauerWeight (↑p).2) ⟨↑y, ⋯⟩)) :
|Real.powerLawIntegral u| ≤ ↑ε * Real.powerLawIntegral (Real.PowerLawInput.gegenbauerWeightClosed p x)Lean proof
theorem abs_powerLawIntegral_le_weightedMassClosed (p : PowerLawClosedParameters)
(x : Icc (-1 : ℝ) 1)
(u : PowerLawInput p.val.1 x.val) (ε : ℝ≥0)
(hu : ∀ y, |u.val y| ≤ (ε : ℝ) * (Polynomial.gegenbauerWeight p.val.2 ⟨y.val,y.property.1⟩ : ℝ)) :
|powerLawIntegral u| ≤ (ε : ℝ) * powerLawIntegral (.gegenbauerWeightClosed p x) := by
have hi := (PowerLawInput.gegenbauerWeightClosed p x).property.const_mul (ε : ℝ)
unfold powerLawIntegral
rw [← integral_const_mul]
rw [← Real.norm_eq_abs]
apply norm_integral_le_of_norm_le hi
apply Filter.Eventually.of_forall
intro y
have hn : 0 ≤ |x.val-y.val|^p.val.1 := rpow_nonneg (abs_nonneg _) _
simpa only [Real.norm_eq_abs, abs_mul, abs_of_nonneg hn,
PowerLawInput.gegenbauerWeightClosed_apply, mul_left_comm] using
mul_le_mul_of_nonneg_left (hu y) hnThese are sufficient endpoint hypotheses; no necessity or singular asymptotic statement is included here.
If \(\alpha \ge 0\) and \(\lambda {\gt}-1/2\), then, for every \(x\in [-1,1]\),
If \(\alpha {\gt}-1\) and \(\lambda \ge 1/2\), then
Consequently a positive uniform mass bound exists in either regime. More generally, under the preceding closed-interval hypotheses, any positive uniform mass bound upgrades uniform convergence of continuous input amplitudes to uniform convergence of their weighted integral outputs on all of \([-1,1]\).
Lean Formalisation
theorem Real.powerLawIntegral_weightedMassClosed_le_of_nonneg (p : Real.PowerLawClosedParameters) (hα : 0 ≤ (↑p).1)
(x : ↑(Set.Icc (-1) 1)) :
Real.powerLawIntegral (Real.PowerLawInput.gegenbauerWeightClosed p x) ≤
2 ^ (↑p).1 *
Real.powerLawIntegral
(Real.PowerLawInput.gegenbauerWeight ⟨0, Real.powerLawIntegral_weightedMassClosed_le_of_nonneg._proof_1⟩
⟨(↑p).2, ⋯⟩ ⟨0, Real.powerLawIntegral_weightedMassClosed_le_of_nonneg._proof_2⟩)Lean proof
theorem powerLawIntegral_weightedMassClosed_le_of_nonneg
(p : PowerLawClosedParameters) (hα : 0 ≤ p.val.1)
(x : Icc (-1 : ℝ) 1) :
powerLawIntegral (.gegenbauerWeightClosed p x) ≤
(2 : ℝ)^p.val.1*powerLawIntegral (.gegenbauerWeight
⟨0,by norm_num⟩ ⟨p.val.2,p.property.2.1⟩ ⟨0,by constructor <;> norm_num⟩) := by
let W : Ioo (-1 : ℝ) 1 → ℝ := fun y ↦ (Polynomial.gegenbauerWeight p.val.2 y : ℝ)
have hlam : -(1/2 : ℝ) < p.val.2 := p.property.2.1
have hW : Integrable W (Measure.comap Subtype.val volume) := by
have h := Polynomial.integrable_jacobiWeight (α := p.val.2-1/2) (β := p.val.2-1/2)
(by linarith) (by linarith)
convert h using 1
all_goals rfl
have hx := integrable_integral_powerLawDomain x.val ⟨W,hW⟩
have hz := integrable_integral_powerLawDomain 0 ⟨W,hW⟩
have hb : powerLawIntegral (.gegenbauerWeightClosed p x) ≤
(2 : ℝ)^p.val.1 * (∫ y : PowerLawDomain x.val,
W ⟨y.val,y.property.1⟩ ∂Measure.comap Subtype.val volume) := by
rw [← integral_const_mul]
apply integral_mono (PowerLawInput.gegenbauerWeightClosed p x).property
(hx.1.const_mul _)
intro y
change |x.val-y.val|^p.val.1 * W ⟨y.val,y.property.1⟩ ≤
(2 : ℝ)^p.val.1 * W ⟨y.val,y.property.1⟩
apply mul_le_mul_of_nonneg_right _ (NNReal.coe_nonneg _)
exact rpow_le_rpow (abs_nonneg _)
(abs_le.mpr ⟨by linarith [x.property.1,y.property.1.2],
by linarith [x.property.2,y.property.1.1]⟩) hα
rw [hx.2,← hz.2] at hb
convert hb using 1
congr 1
apply integral_congr_ae
filter_upwards [] with y
simp only [PowerLawInput.gegenbauerWeight_apply,rpow_zero,one_mul]
rflThe singular-kernel, singular-weight regime is treated in Theorem 6.2.46.
Let \(\kappa \) be a measure on \(X\times Y\), with marginals bounded by \(C\mu \) and \(D\nu \), where \(C,D\) are finite nonnegative constants. Pullback along the coordinate projections defines bounded maps \(J_X:L^2(\mu )\to L^2(\kappa )\) and \(J_Y:L^2(\nu )\to L^2(\kappa )\) with norms at most \(\sqrt C\) and \(\sqrt D\). Then \(T=J_X^*J_Y\) satisfies
The pairing is absolutely integrable for all \(u\in L^2(\nu )\) and \(v\in L^2(\mu )\). For measurable nonnegative densities \(d\kappa =k\, d(\mu \times \nu )\) and sigma-finite \(\mu ,\nu \), the marginal densities are \(\int k(x,y)\, d\nu (y)\) and \(\int k(x,y)\, d\mu (x)\).
Lean Formalisation
theorem MeasureTheory.dominatedL2Pullback_ae.{u_1, u_2} {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y]
(μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) (f : Y → X) (hf : Measurable f) {C : ENNReal} (hC : C ≠ ⊤)
(h : MeasureTheory.Measure.map f ν ≤ C • μ) (u : ↥(MeasureTheory.Lp ℝ 2 μ)) :
↑↑((MeasureTheory.dominatedL2Pullback μ ν f hf hC h) u) =ᵐ[ν] ↑↑u ∘ fLean proof
/-- The pullback acts by composition almost everywhere. -/
theorem dominatedL2Pullback_ae (μ : Measure X) (ν : Measure Y) (f : Y → X)
(hf : Measurable f) {C : ℝ≥0∞} (hC : C ≠ ∞) (h : ν.map f ≤ C • μ)
(u : Lp ℝ 2 μ) : dominatedL2Pullback μ ν f hf hC h u =ᵐ[ν] u ∘ f := by
apply (Lp.coeFn_compMeasurePreserving _ (show MeasurePreserving f ν (ν.map f) from ⟨hf,rfl⟩)).trans
exact ae_of_ae_map hf.aemeasurable (Lp.coeFn_LpToLpOfMeasureLeSMul hC h u)Let \(D=\{ (x,y)\in (-1,1)^2:x\ne y\} \). For arbitrary real \(\alpha ,\tau ,\lambda \), restrict \(\mu _\tau \otimes \mu _\lambda \) to \(D\), multiply by its positive density \(|x-y|^\alpha \), and push forward to \(\mathbb {R}^2\). This defines the joint two-weight kernel measure. The common-weight kernel measure is its specialization \(\tau =\lambda \). These measures need not be finite. No diagonal or exterior kernel value is assigned.
Lean Formalisation
def Real.PowerLawKernelDomain : TypeLean definition
abbrev PowerLawKernelDomain := {z : ℝ × ℝ //
z.1 ∈ Ioo (-1 : ℝ) 1 ∧ z.2 ∈ Ioo (-1 : ℝ) 1 ∧ z.1 ≠ z.2}The distance base is strictly positive on \(D\). For every nonnegative measurable \(\varphi \) on \(\mathbb {R}^2\), integration against the joint measure is exactly
The equality is in \([0,\infty ]\), with no finiteness requirement. Equal input and output weights give the common-weight kernel measure.
Lean Formalisation
theorem Real.powerLawKernelDomain_base_pos (z : Real.PowerLawKernelDomain) : 0 < |(↑z).1 - (↑z).2|Lean proof
theorem powerLawKernelDomain_base_pos (z : PowerLawKernelDomain) :
0 < |z.val.1-z.val.2| := abs_pos.mpr (sub_ne_zero.mpr z.property.2.2)Mass-bound data consist of \(\alpha {\gt}-1\), \(\lambda {\gt}-1/2\), a finite nonnegative real bound \(M\), and \(Q_\alpha w_\lambda (x)\le M\) for every \(x\in (-1,1)\). Here \(Q_\alpha w_\lambda (x)=\int _{D_x}|x-y|^\alpha w_\lambda (y)\, dy\), with an integrable integrand on \(D_x\).
Lean Formalisation
inductive Real.PowerLawL2Data (α lam : ℝ) : TypeLean definition
structure PowerLawL2Data (α lam : ℝ) where
exponent_mem : -1 < α
weight_mem : -(1/2) < lam
bound : ℝ≥0
mass_le : ∀ x : Ioo (-1 : ℝ) 1,
powerLawIntegral (.gegenbauerWeight ⟨α,exponent_mem⟩ ⟨lam,weight_mem⟩ x) ≤ boundFor \((\alpha ,\lambda ,M)\) in the mass-bound domain of Definition 6.2.35, every \(x\in (-1,1)\) satisfies
Lean Formalisation
theorem Real.PowerLawL2Data.mass_le {α lam : ℝ} (self : α.PowerLawL2Data lam) (x : ↑(Set.Ioo (-1) 1)) :
Real.powerLawIntegral (Real.PowerLawInput.gegenbauerWeight ⟨α, ⋯⟩ ⟨lam, ⋯⟩ x) ≤ ↑self.boundFor \((\alpha ,\lambda ,M)\) satisfying Definition 6.2.35, define the bounded operator on \(L^2(\mu _\lambda ;\mathbb {R})\) by the Schur construction for the classical joint power-law kernel measure \(K_{\alpha ,\lambda }\).
Lean Formalisation
def Real.powerLawL2Operator {α lam : ℝ} (p : α.PowerLawL2Data lam) :
↥(MeasureTheory.Lp ℝ 2 (Polynomial.gegenbauerMeasure lam)) →L[ℝ]
↥(MeasureTheory.Lp ℝ 2 (Polynomial.gegenbauerMeasure lam))Lean definition
/-- The power-law operator on the same weighted L² space for input and output. -/
def powerLawL2Operator {α lam : ℝ} (p : PowerLawL2Data α lam) :
Lp ℝ 2 (gegenbauerMeasure lam) →L[ℝ] Lp ℝ 2 (gegenbauerMeasure lam) :=
schurL2Operator _ _ (powerLawKernelMeasure α lam) (by simp) (by simp)
p.kernel_marginals.1
p.kernel_marginals.2For every \(f,g\in L^2(\mu _\lambda )\) the pairing \(g(x)f(y)\) is integrable against \(K_{\alpha ,\lambda }\) and \(\langle g,Tf\rangle =\int g(x)f(y)\, dK_{\alpha ,\lambda }\). The operator is independent of the chosen uniform mass bound.
Lean Formalisation
theorem Real.powerLawL2Operator_spec {α lam : ℝ} (p : α.PowerLawL2Data lam)
(f g : ↥(MeasureTheory.Lp ℝ 2 (Polynomial.gegenbauerMeasure lam))) :
MeasureTheory.Integrable (fun z => ↑↑g z.1 * ↑↑f z.2) (α.powerLawKernelMeasure lam) ∧
inner ℝ g ((Real.powerLawL2Operator p) f) = ∫ (z : ℝ × ℝ), ↑↑g z.1 * ↑↑f z.2 ∂α.powerLawKernelMeasure lamLean proof
theorem powerLawL2Operator_spec {α lam : ℝ} (p : PowerLawL2Data α lam)
(f g : Lp ℝ 2 (gegenbauerMeasure lam)) :
Integrable (fun z : ℝ × ℝ ↦ g z.1*f z.2) (powerLawKernelMeasure α lam) ∧
⟪g,powerLawL2Operator p f⟫_ℝ =
∫ z : ℝ × ℝ, g z.1*f z.2 ∂powerLawKernelMeasure α lam := by
constructor
· exact integrable_schurL2_pair _ _ (powerLawKernelMeasure α lam) (by simp) (by simp)
p.kernel_marginals.1
p.kernel_marginals.2 f g
· exact inner_schurL2Operator _ _ (powerLawKernelMeasure α lam) (by simp) (by simp)
p.kernel_marginals.1
p.kernel_marginals.2 f gLet \(\alpha {\gt}-1\), \(\lambda {\gt}-1/2\), \(d\mu =w_\lambda (x)\, dx\) on \((-1,1)\), and suppose \(Q_\alpha w_\lambda (x)\le M\) throughout \((-1,1)\), with \(M\ge 0\). There is a bounded operator \(T_\alpha :L^2(\mu )\to L^2(\mu )\) with \(\| T_\alpha \| \le M\), characterized by
The double-integral pairing is absolutely integrable for all \(f,g\in L^2(\mu )\). Here \(F\) is integrable and, for almost every \(x\), is the actual power-law integral of \(y\mapsto g(x)w_\lambda (y)f(y)\) on \(D_x\), whose product with \(|x-y|^\alpha \) is integrable. This is the classical weak Fubini identity; no value is asserted for a divergent slice on an exceptional set. The construction is independent of the chosen uniform mass bound. The preceding explicit estimates supply such a bound whenever \(\alpha \ge 0\) or \(\lambda \ge 1/2\), retaining \(\alpha {\gt}-1\) and \(\lambda {\gt}-1/2\). The operator itself allows \(\lambda =0\) and does not require polynomial compatibility. Its identification with the integral is stated in weak form.
Lean Formalisation
theorem Real.lintegral_powerLaw_gegenbauerMeasureOn (α : ↑(Set.Ioi (-1))) (lam : ↑(Set.Ioi (-(1 / 2))))
(x : ↑(Set.Ioo (-1) 1)) :
∫⁻ (y : (↑x).PowerLawDomain),
ENNReal.ofReal (|↑x - ↑y| ^ ↑α) ∂MeasureTheory.Measure.comap Subtype.val (Polynomial.gegenbauerMeasure ↑lam) =
ENNReal.ofReal (Real.powerLawIntegral (Real.PowerLawInput.gegenbauerWeight α lam x))Lean proof
theorem lintegral_powerLaw_gegenbauerMeasureOn (α : Ioi (-1 : ℝ))
(lam : Ioi (-(1/2) : ℝ)) (x : Ioo (-1 : ℝ) 1) :
(∫⁻ y : PowerLawDomain x.val, ENNReal.ofReal (|x.val-y.val|^α.val)
∂Measure.comap Subtype.val (gegenbauerMeasure lam.val)) =
ENNReal.ofReal (powerLawIntegral (.gegenbauerWeight α lam x)) := by
obtain ⟨w,hw,he,hz,hμ⟩ := exists_powerLawKernel_density α.val
let : NullSingletonClass (gegenbauerMeasure lam.val) := nullSingletonClass_gegenbauerMeasure _
have hm := measurableSet_powerLawDomain x.val
have hae : ∀ᵐ y ∂gegenbauerMeasure lam.val, y ∈ Ioo (-1 : ℝ) 1 ∧ y ≠ x.val :=
(ae_mem_Ioo_gegenbauerMeasure lam.val).and ((gegenbauerMeasure lam.val).ae_ne x.val)
have ht := lintegral_subtype_comap (μ := gegenbauerMeasure lam.val) hm
(fun y : ℝ ↦ (w (x.val,y) : ℝ≥0∞))
erw [Measure.restrict_eq_self_of_ae_mem hae] at ht
calc
_ = ∫⁻ y : PowerLawDomain x.val, (w (x.val,y.val) : ℝ≥0∞)
∂Measure.comap Subtype.val (gegenbauerMeasure lam.val) := by
apply lintegral_congr
intro y
have hh := he ⟨(x.val,y.val),x.property,y.property.1,y.property.2.symm⟩
rw [← hh,ENNReal.ofReal_coe_nnreal]
_ = ∫⁻ y, (w (x.val,y) : ℝ≥0∞) ∂gegenbauerMeasure lam.val := ht
_ = _ := lintegral_safePowerLawKernel_row α lam x w heFor \((\alpha ,\lambda ,M)\) in the mass-bound domain of Definition 6.2.35, if \(\lambda \ne 0\) and \(\lambda +\alpha /2=k\in \mathbb N\), then \(T_\alpha \) applied to the \(L^2\) class of a polynomial \(p\) equals the \(L^2\) class of the previously constructed exact polynomial operator applied to \(p\). Thus the analytic and algebraic operators agree.
Lean Formalisation
theorem Real.powerLawL2Operator_polynomial_compatibleOn {α lam : ℝ} (p : α.PowerLawL2Data lam) (hzero : lam ≠ 0) {k : ℕ}
(hk : lam + α / 2 = ↑k) (q : Polynomial ℝ) :
(Real.powerLawL2Operator p) ((Polynomial.polynomialToL2 ⋯) q) =
(Polynomial.polynomialToL2 ⋯)
((Real.powerLawGegenbauerOperator (Real.PowerLawOperatorData.ofIntegrable ⟨α, ⋯⟩ ⟨lam, ⋯⟩ hzero) k) q)Lean proof
theorem powerLawL2Operator_polynomial_compatibleOn {α lam : ℝ} (p : PowerLawL2Data α lam)
(hzero : lam ≠ 0) {k : ℕ} (hk : lam+α/2 = k) (q : ℝ[X]) :
powerLawL2Operator p (polynomialToL2 (hasFiniteMoments_gegenbauerMeasure p.weight_mem) q) =
polynomialToL2 (hasFiniteMoments_gegenbauerMeasure p.weight_mem)
(powerLawGegenbauerOperator (.ofIntegrable ⟨α,p.exponent_mem⟩ ⟨lam,p.weight_mem⟩ hzero) k q) := by
let : SFinite (gegenbauerMeasure lam) := sFinite_gegenbauerMeasure _
let f := polynomialToL2 (hasFiniteMoments_gegenbauerMeasure p.weight_mem) q
obtain ⟨w,hw,he,hz,hμ⟩ := exists_powerLawKernel_density α
have hprod : ∀ᵐ z ∂(gegenbauerMeasure lam).prod (gegenbauerMeasure lam), f z.2 = q.eval z.2 :=
(Measure.quasiMeasurePreserving_snd (μ := gegenbauerMeasure lam)
(ν := gegenbauerMeasure lam)).ae (coe_polynomialToL2 (hasFiniteMoments_gegenbauerMeasure p.weight_mem) q)
have hpair : ∀ᵐ z ∂powerLawKernelMeasure α lam, f z.2 = q.eval z.2 := by
change ∀ᵐ z ∂twoWeightPowerLawKernelMeasure α lam lam, f z.2 = q.eval z.2
rw [hμ lam lam]
exact Measure.AbsolutelyContinuous.ae_eq (withDensity_absolutelyContinuous _ _) hprod
apply ext_inner_left ℝ
intro g
have hi : Integrable (fun z : ℝ × ℝ ↦ g z.1*q.eval z.2) (powerLawKernelMeasure α lam) := by
apply (powerLawL2Operator_spec p f g).1.congr
filter_upwards [hpair] with z hz
rw [hz]
obtain ⟨F,hF,hI⟩ := powerLawWeakFubini (fun y ↦ q.eval y) g hi
rw [(powerLawL2Operator_spec p f g).2,L2.inner_def]
calc
_ = ∫ z : ℝ × ℝ, g z.1*q.eval z.2 ∂powerLawKernelMeasure α lam := by
apply integral_congr_ae
filter_upwards [hpair] with z hz
rw [hz]
_ = ∫ x, F.val x ∂gegenbauerMeasure lam := hI.symm
_ = _ := by
apply integral_congr_ae
filter_upwards [ae_mem_Ioo_gegenbauerMeasure lam,hF,
coe_polynomialToL2 (hasFiniteMoments_gegenbauerMeasure p.weight_mem)
(powerLawGegenbauerOperator (.ofIntegrable ⟨α,p.exponent_mem⟩ ⟨lam,p.weight_mem⟩ hzero) k q)] with x hx hF hq
obtain ⟨I,hval,hFI⟩ := hF
rw [hFI,Real.inner_apply,hq,
eval_powerLawGegenbauerOperator ⟨α,p.exponent_mem⟩ ⟨lam,p.weight_mem⟩ hzero hk ⟨x,hx⟩ q,
powerLawPolynomial_apply]
unfold powerLawIntegral
erw [← integral_const_mul]
apply integral_congr_ae
filter_upwards [] with y
rw [hval y,PowerLawInput.gegenbauerPolynomial_apply]
ringOver \(\mathbb R\) or \(\mathbb C\), let \(P_N\) retain the first \(N\) coordinates in \(\ell ^2(\mathbb N)\). Then \(\| P_N\| \le 1\) and \(P_Nc\to c\) for every \(c\in \ell ^2\). For any bounded linear operator \(A\) on this space,
The convergence is strong operator convergence.
Lean Formalisation
theorem lp.initialL2Projection_apply.{u_1} {𝕜 : Type u_1} [RCLike 𝕜] (N : ℕ) (c : ↥(lp (fun x => 𝕜) 2)) :
(lp.initialL2Projection N) c = ∑ i ∈ Finset.range N, lp.single 2 i (↑c i)Lean proof
/-- The initial projection is the finite sum of coordinate vectors. -/
theorem initialL2Projection_apply (N : ℕ) (c : lp (fun _ : ℕ ↦ 𝕜) 2) :
initialL2Projection N c = ∑ i ∈ Finset.range N, lp.single 2 i (c i) := by
simp only [initialL2Projection, sum_apply, ContinuousLinearMap.comp_apply,
lp.singleContinuousLinearMap_apply]
rflThis is strong convergence for each input, without an assertion of operator-norm convergence or convergence of inverse solves.
Let \((b_n)_{n\ge 0}\) be a real or complex Hilbert basis, with coordinate isometry \(U\), and let \(T\) be a bounded linear operator. The coordinate operator \(A=UTU^{-1}\) satisfies
Transport also commutes with subtraction, so \(\| A_S-A_T\| =\| S-T\| \).
Lean Formalisation
theorem HilbertBasis.coefficientOperator_repr.{u_1, u_2} {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E]
[InnerProductSpace 𝕜 E] (b : HilbertBasis ℕ 𝕜 E) (T : E →L[𝕜] E) (f : E) :
(b.coefficientOperator T) (b.repr f) = b.repr (T f)Lean proof
/-- The transported operator agrees exactly with Hilbert-basis coordinates. -/
theorem coefficientOperator_repr (b : HilbertBasis ℕ 𝕜 E) (T : E →L[𝕜] E) (f : E) :
b.coefficientOperator T (b.repr f) = b.repr (T f) := by
change b.repr (T (b.repr.symm (b.repr f))) = _
rw [LinearIsometryEquiv.symm_apply_apply]For \((\alpha ,\lambda ,M)\) satisfying Definition 6.2.35, with \(\lambda \ne 0\), define \(A=UTU^{-1}\), where \(U\) is the isometry furnished by the normalized Gegenbauer Hilbert basis.
Lean Formalisation
def Real.powerLawCoefficientOperator {α lam : ℝ} (p : α.PowerLawL2Data lam) (hzero : lam ≠ 0) :
↥(lp (fun x => ℝ) 2) →L[ℝ] ↥(lp (fun x => ℝ) 2)Lean definition
/-- The bounded power-law operator in normalized Gegenbauer Hilbert coordinates. -/
def powerLawCoefficientOperator {α lam : ℝ} (p : PowerLawL2Data α lam) (hzero : lam ≠ 0) :
lp (fun _ : ℕ ↦ ℝ) 2 →L[ℝ] lp (fun _ : ℕ ↦ ℝ) 2 :=
(hilbertBasisGegenbauer p.weight_mem hzero).coefficientOperator (powerLawL2Operator p)Let \(T\) be the mass-bounded power-law operator on \(L^2(\mu _\lambda ;\mathbb {R})\) and let \(U\) be its normalized Gegenbauer coordinate isometry. The coefficient operator \(A\) satisfies \(A(Uf)=U(Tf)\) for every \(f\in L^2(\mu _\lambda ;\mathbb {R})\), on the parameter domain of Definition 6.2.43.
Lean Formalisation
theorem Real.powerLawCoefficientOperator_reprOn {α lam : ℝ} (p : α.PowerLawL2Data lam) (hzero : lam ≠ 0)
(f : ↥(MeasureTheory.Lp ℝ 2 (Polynomial.gegenbauerMeasure lam))) :
(Real.powerLawCoefficientOperator p hzero) ((Polynomial.hilbertBasisGegenbauer ⋯ hzero).repr f) =
(Polynomial.hilbertBasisGegenbauer ⋯ hzero).repr ((Real.powerLawL2Operator p) f)Lean proof
theorem powerLawCoefficientOperator_reprOn {α lam : ℝ} (p : PowerLawL2Data α lam)
(hzero : lam ≠ 0) (f : Lp ℝ 2 (gegenbauerMeasure lam)) :
powerLawCoefficientOperator p hzero ((hilbertBasisGegenbauer p.weight_mem hzero).repr f) =
(hilbertBasisGegenbauer p.weight_mem hzero).repr (powerLawL2Operator p f) := by
exact (hilbertBasisGegenbauer p.weight_mem hzero).coefficientOperator_repr (powerLawL2Operator p) fAssume the bounded-operator hypotheses and \(\lambda \ne 0\). Let \(U\) be the isometry from \(L^2(\mu )\) to real \(\ell ^2\) furnished by the normalized Gegenbauer Hilbert basis. The coefficient operator \(A=UT_\alpha U^{-1}\) has \(\| A\| \le M\) and represents \(T_\alpha \) exactly. These are orthonormal Hilbert coordinates, not the unscaled classical Gegenbauer coefficients. Applying \(T_\alpha \) to the classical Gegenbauer partial sums of any \(L^2\) input converges in \(L^2\) to its image. Moreover, if \(P_N\) retains the first \(N\) normalized coefficients, then
The convergence is strong operator convergence.
Lean Formalisation
theorem Real.tendsto_powerLawL2Operator_gegenbauer_sumsOn {α lam : ℝ} (p : α.PowerLawL2Data lam) (hzero : lam ≠ 0)
(f : ↥(MeasureTheory.Lp ℝ 2 (Polynomial.gegenbauerMeasure lam))) :
Filter.Tendsto
(fun N =>
(Real.powerLawL2Operator p)
(∑ n ∈ Finset.range N,
Polynomial.gegenbauerCoefficient lam (Polynomial.IntegralCoefficientInput.ofGegenbauerL2 ⋯ hzero f n) •
(Polynomial.polynomialToL2 ⋯) (Polynomial.gegenbauer lam n)))
Filter.atTop (nhds ((Real.powerLawL2Operator p) f))Lean proof
theorem tendsto_powerLawL2Operator_gegenbauer_sumsOn {α lam : ℝ} (p : PowerLawL2Data α lam)
(hzero : lam ≠ 0) (f : Lp ℝ 2 (gegenbauerMeasure lam)) :
Tendsto (fun N : ℕ ↦ powerLawL2Operator p
(∑ n ∈ Finset.range N, (gegenbauerCoefficient lam
(IntegralCoefficientInput.ofGegenbauerL2 p.weight_mem hzero f n)) •
polynomialToL2 (hasFiniteMoments_gegenbauerMeasure p.weight_mem) (gegenbauer lam n)))
atTop (𝓝 (powerLawL2Operator p f)) :=
(powerLawL2Operator p).continuous.tendsto _ |>.comp
(tendsto_sum_gegenbauerCoefficient_polynomialToL2 p.weight_mem hzero f)This is strong convergence of operator actions; no operator-norm convergence, finite bandwidth for incompatible parameters or inverse-solver convergence is asserted.
For positive \(a,b\) and nonpositive \(p,q\), \(a^pb^q\le a^{p+q}+b^{p+q}\). For \(\alpha {\lt}0\), \(\lambda \le 1/2\), \(x\in \mathbb {R}\), \(y\in D_x=(-1,1)\setminus \{ x\} \) and \(s=\alpha +\lambda -1/2\),
If additionally \(\alpha {\gt}-1\), \(\lambda {\gt}-1/2\) and \(\alpha +\lambda {\gt}-1/2\), this gives
Together with the earlier nonsingular regimes, a positive uniform mass bound therefore exists for every \(\alpha {\gt}-1\), \(\lambda {\gt}-1/2\), \(\alpha +\lambda {\gt}-1/2\).
Lean Formalisation
theorem Real.rpow_mul_rpow_le_add_rpowOn (a b : ↑(Set.Ioi 0)) (p q : ↑(Set.Iic 0)) :
↑a ^ ↑p * ↑b ^ ↑q ≤ ↑a ^ (↑p + ↑q) + ↑b ^ (↑p + ↑q)Lean proof
theorem rpow_mul_rpow_le_add_rpowOn (a b : Ioi (0 : ℝ)) (p q : Iic (0 : ℝ)) :
a.val^p.val*b.val^q.val ≤ a.val^(p.val+q.val)+b.val^(p.val+q.val) := by
rcases le_total a.val b.val with hab | hba
· calc
_ ≤ a.val^p.val*a.val^q.val := mul_le_mul_of_nonneg_left
(rpow_le_rpow_of_nonpos a.property hab q.property) (rpow_nonneg a.property.le _)
_ = a.val^(p.val+q.val) := (rpow_add a.property p.val q.val).symm
_ ≤ _ := le_add_of_nonneg_right (rpow_nonneg b.property.le _)
· calc
_ ≤ b.val^p.val*b.val^q.val := mul_le_mul_of_nonneg_right
(rpow_le_rpow_of_nonpos b.property hba p.property) (rpow_nonneg b.property.le _)
_ = b.val^(p.val+q.val) := (rpow_add b.property p.val q.val).symm
_ ≤ _ := le_add_of_nonneg_left (rpow_nonneg a.property.le _)No claim about the critical or more singular ranges is made.
The constant is not claimed sharp.
Assume \(\alpha {\gt}-1\), \(\lambda {\gt}-1/2\) and \(\alpha +\lambda {\gt}-1/2\). Uniform convergence of continuous amplitudes on \([-1,1]\) gives uniform convergence of their weighted power-law integral outputs on the entire closed interval. There is a bounded power-law operator on the common space \(L^2(\mu _\lambda )\), with the weak integral characterization and a finite norm bound supplied above. If \(\lambda \ne 0\), the normalized Gegenbauer coefficient operator has the same norm bound and its leading finite sections satisfy \(P_NAP_Nc\to Ac\) in \(\ell ^2\) for every \(c\in \ell ^2\). No polynomial compatibility is needed. These remain statements about operator actions, not inverse solves or optimal boundedness thresholds.
Lean Formalisation
theorem Real.tendstoUniformly_powerLaw_gegenbauerContinuousClosed_of_endpoint (p : Real.PowerLawClosedParameters)
(f : C(↑(Set.Icc (-1) 1), ℝ)) (u : ℕ → C(↑(Set.Icc (-1) 1), ℝ))
(hconv : TendstoUniformly (fun n y => (u n) y) (⇑f) Filter.atTop) :
TendstoUniformly (fun n x => Real.powerLawIntegral (Real.PowerLawInput.gegenbauerContinuousClosed p x (u n)))
(fun x => Real.powerLawIntegral (Real.PowerLawInput.gegenbauerContinuousClosed p x f)) Filter.atTopLean proof
theorem tendstoUniformly_powerLaw_gegenbauerContinuousClosed_of_endpoint
(p : PowerLawClosedParameters) (f : C(Icc (-1 : ℝ) 1, ℝ))
(u : ℕ → C(Icc (-1 : ℝ) 1, ℝ))
(hconv : TendstoUniformly (fun n y ↦ u n y) f atTop) :
TendstoUniformly
(fun n x ↦ powerLawIntegral (.gegenbauerContinuousClosed p x (u n)))
(fun x ↦ powerLawIntegral (.gegenbauerContinuousClosed p x f)) atTop := by
obtain ⟨M,hM,hb⟩ := exists_powerLawIntegral_weightedMassClosed_bound_of_endpoint p
exact tendstoUniformly_powerLaw_gegenbauerContinuousClosed p ⟨M,hM⟩ hb f u hconvFor real \(a,c,z\), if \((c)_n\ne 0\) for every \(n\ge 0\) and \(|z|{\lt}1\), then \({}_2F_1(a,c;c;z)=(1-z)^{-a}\). In particular, the denominator condition holds for \(c{\gt}0\). Reference: [DLMF, 15.4.6].
Lean Formalisation
theorem Real.ordinaryHypergeometricOn_cancel (a : ℝ) (c : Real.GammaPoint) (z : ↑(Metric.ball 0 1)) :
ordinaryHypergeometricOn (GaussParameters.ofNoPole a ↑c ↑c ⋯)
(GaussSeriesPoint.ofUnitDisk (GaussParameters.ofNoPole a ↑c ↑c ⋯) z) =
(1 - ↑z) ^ (-a)Lean proof
/-- Cancellation of a non-pole denominator on the open unit disk. -/
theorem ordinaryHypergeometricOn_cancel (a : ℝ) (c : GammaPoint)
(z : Metric.ball (0 : ℝ) 1) :
ordinaryHypergeometricOn (.ofNoPole a c.val c.val c.property)
(.ofUnitDisk _ z) = (1-z.val)^(-a) := by
have hz : |z.val| < 1 := by
simpa only [Metric.mem_ball, dist_zero_right, Real.norm_eq_abs] using z.property
have hc (n : ℕ) : (ascPochhammer ℝ n).eval c.val ≠ 0 := by
intro hn
obtain ⟨k,_,hk⟩ := (ascPochhammer_eval_eq_zero_iff n c.val).mp hn
exact c.property k (by simpa using congrArg Neg.neg hk.symm)
have h := (one_div_one_sub_rpow_hasFPowerSeriesOnBall_zero a).hasSum
(y := z.val) (by
rw [Metric.mem_eball, edist_eq_enorm_sub, sub_zero, enorm_eq_nnnorm]
exact_mod_cast hz)
have hcoeff (n : ℕ) : Ring.choose (a+n-1) n =
(n.factorial : ℝ)⁻¹ * (ascPochhammer ℝ n).eval a := by
rw [← Ring.multichoose_eq]
have hn := Ring.factorial_nsmul_multichoose_eq_ascPochhammer a n
simp only [nsmul_eq_mul, ascPochhammer_smeval_eq_eval] at hn
have hne : (n.factorial : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr n.factorial_ne_zero
apply mul_left_cancel₀ hne
rw [hn, ← mul_assoc, mul_inv_cancel₀ hne, one_mul]
simp only [FormalMultilinearSeries.ofScalars_apply_eq, smul_eq_mul,
hcoeff, zero_add] at h
have he (n : ℕ) : ordinaryHypergeometricCoefficientOn
(.ofNoPole a c.val c.val c.property) n =
(n.factorial : ℝ)⁻¹ * (ascPochhammer ℝ n).eval a := by
rw [ordinaryHypergeometricCoefficientOn_eq_div _ n (hc n)]
dsimp only [GaussParameters.ofNoPole]
have hf : (n.factorial : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr n.factorial_ne_zero
field_simp [hc n, hf]
have hs := hasSum_ordinaryHypergeometricOn (.ofNoPole a c.val c.val c.property) z
simp only [he] at hs
have hv := hs.unique h
rw [rpow_neg (by linarith [le_abs_self z.val] : 0 ≤ 1-z.val)]
simpa only [one_div] using hvFor any real \(\lambda ,p\), multiplication of \(\mu _\lambda \) by \((1-x^2)^p\) gives \(\mu _{\lambda +p}\). These are identities of measures on \((-1,1)\), without a finiteness assumption. The multiplying factor is the Gegenbauer weight \(w_{p+1/2}(x)=(1-x^2)^p\).
Lean Formalisation
theorem Polynomial.gegenbauerMeasure_shift (lam p : ℝ) :
MeasureTheory.openIntervalWeightMeasure (-1) 1
(Polynomial.gegenbauerWeight lam * Polynomial.gegenbauerWeight (p + 1 / 2)) =
Polynomial.gegenbauerMeasure (lam + p)Lean proof
/-- Multiplication of classical open-domain weights shifts the parameter.
Here the second weight has exponent p. Reference: DLMF Table 18.3.1. -/
theorem gegenbauerMeasure_shift (lam p : ℝ) :
openIntervalWeightMeasure (-1) 1
(gegenbauerWeight lam * gegenbauerWeight (p + 1 / 2)) =
gegenbauerMeasure (lam+p) := by
change openIntervalWeightMeasure (-1) 1 _ = openIntervalWeightMeasure (-1) 1 _
congr 1
ext x
simp only [ContinuousMap.mul_apply, NNReal.coe_mul, gegenbauerWeight_apply]
have hp : 0 < 1 - (x : ℝ)^2 := by nlinarith [x.property.1,x.property.2]
rw [← Real.rpow_add hp]
congr 1
ringFor a measure \(\mu \), a positive measurable weight is a measurable real function \(h\) such that \(h{\gt}0\) \(\mu \)-almost everywhere. No pointwise positivity on a null set is imposed.
Lean Formalisation
def MeasureTheory.PositiveWeight.{u_1} {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) : Type u_1Lean definition
/-- A measurable real weight with positivity bundled almost everywhere. -/
abbrev PositiveWeight (μ : Measure X) :=
{h : X → ℝ // Measurable h ∧ ∀ᵐ x ∂μ, 0 < h x}A weight \(h\) in the positive-measurable-weight domain is measurable and satisfies \(h(x){\gt}0\) for \(\mu \)-almost every \(x\).
Lean Formalisation
theorem MeasureTheory.PositiveWeight.spec.{u_1} {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X)
(w : MeasureTheory.PositiveWeight μ) : Measurable ↑w ∧ ∀ᵐ (x : X) ∂μ, 0 < ↑w xLean proof
theorem PositiveWeight.spec (μ : Measure X) (w : PositiveWeight μ) :
Measurable w.val ∧ ∀ᵐ x ∂μ, 0 < w.val x := w.propertyFor a positive measurable weight \(h\), define \(D_h:L^2(\mu ;\mathbb {R})\to L^2(h^2\mu ;\mathbb {R})\) as the linear isometry characterized by \((D_hu)h=u\) \(h^2\mu \)-almost everywhere for every \(u\in L^2(\mu ;\mathbb {R})\). This defines an \(L^2\) equivalence class and assigns no pointwise quotient at a zero of \(h\).
Lean Formalisation
def MeasureTheory.divWeightL2.{u_1} {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X)
(w : MeasureTheory.PositiveWeight μ) :
↥(MeasureTheory.Lp ℝ 2 μ) →ₗᵢ[ℝ] ↥(MeasureTheory.Lp ℝ 2 (μ.withDensity fun x => ENNReal.ofReal (↑w x ^ 2)))Lean definition
/-- The unique classical isometry supplied by its multiplicative characterisation. -/
def divWeightL2 (μ : Measure X) (w : PositiveWeight μ) :
Lp ℝ 2 μ →ₗᵢ[ℝ] Lp ℝ 2 (μ.withDensity (fun x ↦ ENNReal.ofReal (w.val x^2))) :=
(exists_divWeightL2 μ w).chooseThe isometry satisfies \((D_hu)h=u\) \(h^2\mu \)-almost everywhere and is uniquely determined by this identity. Equivalently, it is division by \(h\) on the conull positive-weight domain. Neither \(h\in L^2(\mu )\) nor finiteness of \(h^2\mu \) is required.
Lean Formalisation
theorem MeasureTheory.divWeightL2_spec.{u_1} {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X)
(w : MeasureTheory.PositiveWeight μ) (u : ↥(MeasureTheory.Lp ℝ 2 μ)) :
∀ᵐ (x : X) ∂μ.withDensity fun x => ENNReal.ofReal (↑w x ^ 2), ↑↑((MeasureTheory.divWeightL2 μ w) u) x * ↑w x = ↑↑u xLean proof
theorem divWeightL2_spec (μ : Measure X) (w : PositiveWeight μ) (u : Lp ℝ 2 μ) :
∀ᵐ x ∂μ.withDensity (fun x ↦ ENNReal.ofReal (w.val x^2)),
divWeightL2 μ w u x*w.val x = u x :=
(exists_divWeightL2 μ w).choose_spec uFor a positive measurable weight \(h\) and a joint measure whose marginals are bounded by \(C h^2\mu \), with \(0\le C{\lt}\infty \), let \(S\) be the ordinary Schur operator on \(L^2(h^2\mu )\). Define \(T=D_h^* S D_h\) on \(L^2(\mu )\).
Lean Formalisation
def MeasureTheory.weightedSchurL2Operator.{u_1} {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X)
(κ : MeasureTheory.Measure (X × X)) (w : MeasureTheory.PositiveWeight μ) {C : ENNReal} (hC : C ≠ ⊤)
(hfst : MeasureTheory.Measure.map Prod.fst κ ≤ C • μ.withDensity fun x => ENNReal.ofReal (↑w x ^ 2))
(hsnd : MeasureTheory.Measure.map Prod.snd κ ≤ C • μ.withDensity fun x => ENNReal.ofReal (↑w x ^ 2)) :
↥(MeasureTheory.Lp ℝ 2 μ) →L[ℝ] ↥(MeasureTheory.Lp ℝ 2 μ)Lean definition
/-- The weighted Schur operator, obtained by conjugating the ordinary Schur construction. -/
def weightedSchurL2Operator (μ : Measure X) (κ : Measure (X × X))
(w : PositiveWeight μ)
{C : ℝ≥0∞} (hC : C ≠ ∞)
(hfst : κ.map Prod.fst ≤ C • μ.withDensity (fun x ↦ ENNReal.ofReal (w.val x^2)))
(hsnd : κ.map Prod.snd ≤ C • μ.withDensity (fun x ↦ ENNReal.ofReal (w.val x^2))) :
Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ :=
let D := (divWeightL2 μ w).toContinuousLinearMap
D.adjoint.comp ((schurL2Operator _ _ κ hC hC hfst hsnd).comp D)Let \(h\) be real measurable and positive \(\mu \)-almost everywhere. Division by \(h\) is an isometry \(D:L^2(\mu ;\mathbb R)\to L^2(h^2\mu ;\mathbb R)\). If a measure \(\kappa \) on \(X\times X\) has both marginals at most \(C h^2\mu \), with \(0\le C{\lt}\infty \), then there is a bounded operator \(T\) on \(L^2(\mu ;\mathbb R)\) with
This pairing is absolutely integrable for every pair of \(L^2\) functions. Neither \(h\in L^2(\mu )\) nor finiteness of \(h^2\mu \) is required.
Lean Formalisation
theorem MeasureTheory.norm_weightedSchurL2Operator_le.{u_1} {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X)
(κ : MeasureTheory.Measure (X × X)) (w : MeasureTheory.PositiveWeight μ) {C : ENNReal} (hC : C ≠ ⊤)
(hfst : MeasureTheory.Measure.map Prod.fst κ ≤ C • μ.withDensity fun x => ENNReal.ofReal (↑w x ^ 2))
(hsnd : MeasureTheory.Measure.map Prod.snd κ ≤ C • μ.withDensity fun x => ENNReal.ofReal (↑w x ^ 2)) :
‖MeasureTheory.weightedSchurL2Operator μ κ w hC hfst hsnd‖ ≤ C.toRealLean proof
/-- The weighted Schur construction retains the marginal norm bound. -/
theorem norm_weightedSchurL2Operator_le (μ : Measure X) (κ : Measure (X × X))
(w : PositiveWeight μ)
{C : ℝ≥0∞} (hC : C ≠ ∞)
(hfst : κ.map Prod.fst ≤ C • μ.withDensity (fun x ↦ ENNReal.ofReal (w.val x^2)))
(hsnd : κ.map Prod.snd ≤ C • μ.withDensity (fun x ↦ ENNReal.ofReal (w.val x^2))) :
‖weightedSchurL2Operator μ κ w hC hfst hsnd‖ ≤ C.toReal := by
let D := (divWeightL2 μ w).toContinuousLinearMap
let S := schurL2Operator _ _ κ hC hC hfst hsnd
have hd : ‖D‖ ≤ 1 := (divWeightL2 μ w).norm_toContinuousLinearMap_le
have hs : ‖S‖ ≤ C.toReal := by
simpa [S, Real.mul_self_sqrt ENNReal.toReal_nonneg] using
norm_schurL2Operator_le _ _ κ hC hC hfst hsnd
change ‖D.adjoint.comp (S.comp D)‖ ≤ _
apply (ContinuousLinearMap.opNorm_comp_le _ _).trans
rw [ContinuousLinearMap.adjoint.norm_map]
calc
_ ≤ 1 * (‖S‖ * ‖D‖) := mul_le_mul hd (ContinuousLinearMap.opNorm_comp_le _ _)
(norm_nonneg _) (by norm_num)
_ ≤ 1 * (C.toReal * 1) := by gcongr
_ = _ := by ringFor every real \(\alpha \), define the continuous positive weight \(h_\alpha (x)=(1-x^2)^{\alpha /2}\) on \(x\in (-1,1)\).
Lean Formalisation
def Real.powerLawSchurWeight (α : ℝ) : C(↑(Set.Ioo (-1) 1), NNReal)Lean definition
def powerLawSchurWeight (α : ℝ) : C(Ioo (-1 : ℝ) 1, ℝ≥0) :=
Polynomial.gegenbauerWeight ((α+1)/2)For every real \(\alpha \) and \(x\in (-1,1)\),
The domain of \(h_\alpha \) excludes the endpoints and exterior of the interval.
Lean Formalisation
theorem Real.powerLawSchurWeight_apply (α : ℝ) (x : ↑(Set.Ioo (-1) 1)) : ↑(α.powerLawSchurWeight x) = (1 - ↑x ^ 2) ^ (α / 2)Lean proof
theorem powerLawSchurWeight_apply (α : ℝ) (x : Ioo (-1 : ℝ) 1) :
(powerLawSchurWeight α x : ℝ) = (1-x.val^2)^(α/2) := by
rw [powerLawSchurWeight, Polynomial.gegenbauerWeight_apply]
congr 1
ringFor real \(\alpha \) such that neither \((\alpha +1)/2\) nor \(-\alpha /2\) is a nonpositive integer, define \(C_\alpha =\Gamma ((\alpha +1)/2)\Gamma (-\alpha /2)/\Gamma (1/2)\).
Lean Formalisation
def Real.PowerLawSchurParameter : TypeLean definition
abbrev PowerLawSchurParameter := {α : ℝ //
(∀ n : ℕ, (α+1)/2 ≠ -(n : ℝ)) ∧ (∀ n : ℕ, -α/2 ≠ -(n : ℝ))}Whenever neither \((\alpha +1)/2\) nor \(-\alpha /2\) is a nonpositive integer,
Every \(-1{\lt}\alpha {\lt}0\) satisfies these conditions and gives \(C_\alpha {\gt}0\).
Lean Formalisation
theorem Real.powerLawSchurConstant_apply (α : Real.PowerLawSchurParameter) :
Real.powerLawSchurConstant α =
Real.GammaOn ⟨(↑α + 1) / 2, ⋯⟩ * Real.GammaOn ⟨-↑α / 2, ⋯⟩ /
Real.GammaOn (Real.GammaPoint.ofPos (1 / 2) Real.powerLawSchurConstant._proof_1)Lean proof
theorem powerLawSchurConstant_apply (α : PowerLawSchurParameter) :
powerLawSchurConstant α =
GammaOn ⟨(α.val+1)/2,α.property.1⟩*GammaOn ⟨-α.val/2,α.property.2⟩/
GammaOn (.ofPos (1/2) (by norm_num)) := rflFor \(-1{\lt}\alpha {\lt}0\) and \(x\in (-1,1)\), set
Then \(Q_\alpha w_{-\alpha /2-1/2}(x)=C_\alpha h_\alpha (x)\). Consequently, if \(\lambda {\gt}-1/2\) and \(\alpha +\lambda =-1/2\),
The nonnegative integral is taken on \(D_x=(-1,1)\setminus \{ x\} \), where all factors have their classical values. The auxiliary weight is positive throughout the support domain of every Gegenbauer measure.
Lean Formalisation
theorem Real.powerLawIntegral_gegenbauerWeight_criticalOn (α : ↑(Set.Ioo (-1) 0)) (x : ↑(Set.Ioo (-1) 1)) :
Real.powerLawIntegral (Real.PowerLawInput.gegenbauerWeight ⟨↑α, ⋯⟩ ⟨-↑α / 2 - 1 / 2, ⋯⟩ x) =
Real.powerLawSchurConstant (Real.PowerLawSchurParameter.ofCritical α) * ↑((↑α).powerLawSchurWeight x)Lean proof
theorem powerLawIntegral_gegenbauerWeight_criticalOn (α : Ioo (-1 : ℝ) 0)
(x : Ioo (-1 : ℝ) 1) :
powerLawIntegral (.gegenbauerWeight ⟨α.val,α.property.1⟩
⟨-α.val/2-1/2,by change -(1/2) < -α.val/2-1/2; linarith [α.property.2]⟩ x) =
powerLawSchurConstant (.ofCritical α)*(powerLawSchurWeight α.val x : ℝ) := by
rw [powerLawIntegral_gegenbauerWeight_hypergeometricSqOn,powerLawSchurWeight_apply]
simp only [GaussParameters.ofNoPole,
GammaOn,GammaPoint.ofPos,powerLawSchurConstant,PowerLawSchurParameter.ofCritical]
simp only [show -α.val/2-1/2+1/2 = -α.val/2 by ring,
show -α.val/2-1/2+α.val/2+1 = (1/2 : ℝ) by ring]
have hz : |x.val^2| < 1 := by
rw [abs_of_nonneg (sq_nonneg x.val)]
nlinarith [x.property.1,x.property.2,sq_nonneg (x.val+1),sq_nonneg (x.val-1)]
have hc := ordinaryHypergeometricOn_cancel_of_pos (-α.val/2)
⟨(1/2 : ℝ),by norm_num⟩ ⟨x.val^2,by
simpa only [Metric.mem_ball,dist_zero_right,Real.norm_eq_abs] using hz⟩
simp only [GaussParameters.ofNoPole] at hc
erw [show -(-α.val/2-1/2)-α.val/2 = (1/2 : ℝ) by ring, hc]
congr 2
ringFor real \(\alpha ,\lambda \), define the joint kernel measure with exponent \(\alpha \) and Gegenbauer parameter \(\lambda +\alpha /2\) in both variables. It is the classical measure obtained by tilting the original kernel by \(h_\alpha (x)h_\alpha (y)\) on its off-diagonal open-square domain.
Lean Formalisation
def Real.powerLawSchurMeasure (α lam : ℝ) : MeasureTheory.Measure (ℝ × ℝ)Lean definition
def powerLawSchurMeasure (α lam : ℝ) : Measure (ℝ × ℝ) :=
powerLawKernelMeasure α (lam+α/2)The measure is exactly the kernel measure with parameter \(\lambda +\alpha /2\). For \(-1{\lt}\alpha {\lt}0\) and \(\lambda =-\alpha -1/2\), both marginals are \(C_\alpha \mu _{-1/2}=C_\alpha h_\alpha ^2\mu _\lambda \).
Lean Formalisation
theorem Real.powerLawSchurMeasure_apply (α lam : ℝ) : α.powerLawSchurMeasure lam = α.powerLawKernelMeasure (lam + α / 2)Lean proof
theorem powerLawSchurMeasure_apply (α lam : ℝ) :
powerLawSchurMeasure α lam = powerLawKernelMeasure α (lam+α/2) := rflFor \(\alpha {\gt}-1\), \(\lambda {\gt}-1/2\), and \(\alpha +\lambda =-1/2\), define the bounded operator on \(L^2(\mu _\lambda ;\mathbb {R})\) by its integrable weak pairing \(\langle g,Tf\rangle =\int g(x)f(y)\, dK_{\alpha ,\lambda }(x,y)\), where \(K_{\alpha ,\lambda }\) is the classical joint power-law kernel measure.
Lean Formalisation
def Real.criticalPowerLawL2Operator {α lam : ℝ} (hα : -1 < α) (hlam : -(1 / 2) < lam) (hcrit : α + lam = -(1 / 2)) :
↥(MeasureTheory.Lp ℝ 2 (Polynomial.gegenbauerMeasure lam)) →L[ℝ]
↥(MeasureTheory.Lp ℝ 2 (Polynomial.gegenbauerMeasure lam))Lean definition
def criticalPowerLawL2Operator {α lam : ℝ}
(hα : -1 < α) (hlam : -(1/2) < lam) (hcrit : α+lam = -(1/2)) :
Lp ℝ 2 (gegenbauerMeasure lam) →L[ℝ] Lp ℝ 2 (gegenbauerMeasure lam) :=
(exists_criticalPowerLawL2Operator_classical hα hlam hcrit).chooseAssume \(\alpha {\gt}-1\), \(\lambda {\gt}-1/2\) and \(\alpha +\lambda =-1/2\). For every \(f,g\in L^2(\mu _\lambda ;\mathbb {R})\), the function \((x,y)\mapsto g(x)f(y)\) is integrable against the classical joint kernel measure \(K_{\alpha ,\lambda }\), and
This identity for all \(f,g\) uniquely determines the bounded operator \(T\).
Lean Formalisation
theorem Real.criticalPowerLawL2Operator_spec {α lam : ℝ} (hα : -1 < α) (hlam : -(1 / 2) < lam) (hcrit : α + lam = -(1 / 2))
(f g : ↥(MeasureTheory.Lp ℝ 2 (Polynomial.gegenbauerMeasure lam))) :
MeasureTheory.Integrable (fun z => ↑↑g z.1 * ↑↑f z.2) (α.powerLawKernelMeasure lam) ∧
inner ℝ g ((Real.criticalPowerLawL2Operator hα hlam hcrit) f) =
∫ (z : ℝ × ℝ), ↑↑g z.1 * ↑↑f z.2 ∂α.powerLawKernelMeasure lamLean proof
theorem criticalPowerLawL2Operator_spec {α lam : ℝ}
(hα : -1 < α) (hlam : -(1/2) < lam) (hcrit : α+lam = -(1/2))
(f g : Lp ℝ 2 (gegenbauerMeasure lam)) :
Integrable (fun z : ℝ × ℝ ↦ g z.1*f z.2) (powerLawKernelMeasure α lam) ∧
⟪g,criticalPowerLawL2Operator hα hlam hcrit f⟫_ℝ =
∫ z : ℝ × ℝ, g z.1*f z.2 ∂powerLawKernelMeasure α lam :=
(exists_criticalPowerLawL2Operator_classical hα hlam hcrit).choose_spec.2 f gAssume \(\alpha {\gt}-1\), \(\lambda {\gt}-1/2\) and \(\alpha +\lambda =-1/2\). The measure with density \(|x-y|^\alpha h_\alpha (x)h_\alpha (y)\) on \(\{ (x,y)\in (-1,1)^2:x\ne y\} \) against \(\mu _\lambda \otimes \mu _\lambda \) has both marginals exactly \(C_\alpha h_\alpha ^2\mu _\lambda \). It defines a bounded operator \(T\) on \(L^2(\mu _\lambda ;\mathbb R)\) with \(\| T\| \le C_\alpha \) and
The double pairing is absolutely integrable for every \(f,g\in L^2\); there is a \(\mu _\lambda \)-integrable function \(F\) such that, for almost every \(x\), the function \(y\mapsto |x-y|^\alpha g(x)w_\lambda (y)f(y)\) is integrable on \(D_x\), \(F(x)\) is its integral, and \(\langle g,Tf\rangle =\int F\, d\mu _\lambda \). Together with the strict case, a bounded weak kernel realization exists whenever \(\alpha +\lambda \ge -1/2\).
Lean Formalisation
theorem Real.norm_criticalPowerLawL2Operator_leOn {α lam : ℝ} (hα : -1 < α) (hlam : -(1 / 2) < lam)
(hcrit : α + lam = -(1 / 2)) :
‖Real.criticalPowerLawL2Operator hα hlam hcrit‖ ≤
Real.powerLawSchurConstant (Real.PowerLawSchurParameter.ofCritical ⟨α, ⋯⟩)Lean proof
theorem norm_criticalPowerLawL2Operator_leOn {α lam : ℝ}
(hα : -1 < α) (hlam : -(1/2) < lam) (hcrit : α+lam = -(1/2)) :
‖criticalPowerLawL2Operator hα hlam hcrit‖ ≤
powerLawSchurConstant (.ofCritical ⟨α,hα,by linarith⟩) :=
(exists_criticalPowerLawL2Operator_classical hα hlam hcrit).choose_spec.1No sharp operator norm or uniform endpoint convergence is asserted here.
Assume \(\alpha {\gt}-1\), \(\lambda {\gt}-1/2\), \(\lambda \ne 0\) and \(\alpha +\lambda =-1/2\). Let \(T\) be the critical weighted Schur operator, and let \(U\) be the normalized Gegenbauer Hilbert-coordinate isometry. Then \(A=UTU^{-1}\) satisfies
Writing \(b_i\) for the normalized \(L^2\) basis vectors, its entries are
Applying \(T\) to the classical Gegenbauer partial sums of any \(L^2\) input also converges in \(L^2\) to its image. Together with the strict-range result, normalized coefficient actions and finite-section convergence therefore cover \(\alpha +\lambda \ge -1/2\) whenever \(\lambda \ne 0\). The coefficient restriction comes from the classical Gegenbauer basis; the underlying \(L^2\) boundedness theorem includes \(\lambda =0\).
Lean Formalisation
theorem Real.norm_criticalPowerLawCoefficientOperator {α lam : ℝ} (hα : -1 < α) (hlam : -(1 / 2) < lam) (hzero : lam ≠ 0)
(hcrit : α + lam = -(1 / 2)) :
‖Real.criticalPowerLawCoefficientOperator hα hlam hzero hcrit‖ = ‖Real.criticalPowerLawL2Operator hα hlam hcrit‖Lean proof
/-- The critical coefficient operator has the same norm as its L² realization. -/
theorem norm_criticalPowerLawCoefficientOperator {α lam : ℝ}
(hα : -1 < α) (hlam : -(1/2) < lam) (hzero : lam ≠ 0) (hcrit : α+lam = -(1/2)) :
‖criticalPowerLawCoefficientOperator hα hlam hzero hcrit‖ =
‖criticalPowerLawL2Operator hα hlam hcrit‖ :=
(hilbertBasisGegenbauer hlam hzero).norm_coefficientOperator _For a measure \(\mu \), weak kernel data include almost-everywhere measurability of \(x\mapsto (y\mapsto (x,y))_*\mu \) as a measure-valued map, certifying the product \(\mu \times \mu \). They consist further of a real kernel \(k(x,y)\), a bounded operator \(T\) on \(L^2(\mu ;\mathbb {R})\), and, for every \(L^2\) pair \(f,g\), absolute integrability of \(k(x,y)g(x)f(y)\) and the identity \(\langle g,Tf\rangle =\int k(x,y)g(x)f(y)\, d(\mu \times \mu )\).
Lean Formalisation
inductive MeasureTheory.L2WeakKernel.{u_1} {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) : Type u_1Lean definition
structure L2WeakKernel {X : Type*} [MeasurableSpace X] (μ : Measure X) where
product_measurable : AEMeasurable (fun x : X => Measure.map (Prod.mk x) μ) μ
kernel : X × X → ℝ
operator : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ
pair_integrable : ∀ f g : Lp ℝ 2 μ,
Integrable (fun z : X × X ↦ kernel z*(g z.1*f z.2)) (μ.prod μ)
pairing : ∀ f g : Lp ℝ 2 μ,
⟪g,operator f⟫_ℝ = ∫ z : X × X, kernel z*(g z.1*f z.2) ∂μ.prod μLet \((\mu ,k,T)\) satisfy the weak-kernel conditions of Definition 6.2.67. For every \(f,g\in L^2(\mu ;\mathbb {R})\), \(k(x,y)g(x)f(y)\) is integrable and
The integral does not depend on the pointwise representatives of \(f,g\). For s-finite \(\mu \), the measure-valued product kernel is automatically almost-everywhere measurable; in particular the product-measurability condition adds no restriction for finite measures.
Lean Formalisation
theorem MeasureTheory.L2WeakKernel.spec.{u_1} {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X}
(K : MeasureTheory.L2WeakKernel μ) (f g : ↥(MeasureTheory.Lp ℝ 2 μ)) :
MeasureTheory.Integrable (fun z => K.kernel z * (↑↑g z.1 * ↑↑f z.2)) (μ.prod μ) ∧
inner ℝ g (K.operator f) = ∫ (z : X × X), K.kernel z * (↑↑g z.1 * ↑↑f z.2) ∂μ.prod μLean proof
theorem L2WeakKernel.spec {X : Type*} [MeasurableSpace X] {μ : Measure X}
(K : L2WeakKernel μ) (f g : Lp ℝ 2 μ) :
Integrable (fun z : X × X ↦ K.kernel z*(g z.1*f z.2)) (μ.prod μ) ∧
⟪g,K.operator f⟫_ℝ = ∫ z : X × X, K.kernel z*(g z.1*f z.2) ∂μ.prod μ :=
⟨K.pair_integrable f g,K.pairing f g⟩Let \(\mu \) be finite and let a bounded real \(L^2(\mu )\) operator \(T\) have weak kernel \(k(x,y)\) as in Definition 6.2.67. For measurable \(A,B\), the rectangle integral exists and
Lean Formalisation
theorem MeasureTheory.L2WeakKernel.integrableOn_rectangle.{u_1} {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X}
[MeasureTheory.IsFiniteMeasure μ] (K : MeasureTheory.L2WeakKernel μ) {A B : Set X} (hA : MeasurableSet A)
(hB : MeasurableSet B) : MeasureTheory.IntegrableOn K.kernel (A ×ˢ B) (μ.prod μ)Lean proof
theorem L2WeakKernel.integrableOn_rectangle {X : Type*} [MeasurableSpace X]
{μ : Measure X} [IsFiniteMeasure μ] (K : L2WeakKernel μ)
{A B : Set X} (hA : MeasurableSet A) (hB : MeasurableSet B) :
IntegrableOn K.kernel (A ×ˢ B) (μ.prod μ) := by
let u := indicatorConstLp 2 hB (measure_ne_top μ B) (1 : ℝ)
let v := indicatorConstLp 2 hA (measure_ne_top μ A) (1 : ℝ)
have he : (fun z : X × X ↦ K.kernel z*(v z.1*u z.2)) =ᵐ[μ.prod μ]
(A ×ˢ B).indicator K.kernel := by
filter_upwards [Measure.quasiMeasurePreserving_fst.ae_eq_comp
(indicatorConstLp_coeFn (p := 2) (hs := hA) (hμs := measure_ne_top μ A) (c := (1 : ℝ))),
Measure.quasiMeasurePreserving_snd.ae_eq_comp
(indicatorConstLp_coeFn (p := 2) (hs := hB) (hμs := measure_ne_top μ B) (c := (1 : ℝ)))] with z hz hz'
change v z.1 = A.indicator (fun _ ↦ (1 : ℝ)) z.1 at hz
change u z.2 = B.indicator (fun _ ↦ (1 : ℝ)) z.2 at hz'
rw [hz,hz']
by_cases ha : z.1 ∈ A <;> by_cases hb : z.2 ∈ B <;> simp [ha,hb]
exact (integrable_indicator_iff (hA.prod hB)).mp ((K.pair_integrable u v).congr he)For real \(\alpha ,\lambda \), a weak realization is a bounded operator \(T\) on \(L^2(\mu _\lambda ;\mathbb {R})\) such that the function \(g(x)f(y)\) is integrable against the classical joint kernel measure for every \(L^2\) pair \(f,g\), and \(\langle g,Tf\rangle =\int g(x)f(y)\, dK_{\alpha ,\lambda }\). This domain may be empty.
Lean Formalisation
def Real.PowerLawWeakRealization (α lam : ℝ) : TypeLean definition
abbrev PowerLawWeakRealization (α lam : ℝ) :=
{T : Lp ℝ 2 (gegenbauerMeasure lam) →L[ℝ] Lp ℝ 2 (gegenbauerMeasure lam) //
∀ f g : Lp ℝ 2 (gegenbauerMeasure lam),
Integrable (fun z : ℝ × ℝ ↦ g z.1*f z.2) (powerLawKernelMeasure α lam) ∧
⟪g,T f⟫_ℝ = ∫ z : ℝ × ℝ, g z.1*f z.2 ∂powerLawKernelMeasure α lam}For real \(\alpha ,\lambda \) and a weak realization \(T\) in the sense of Definition 6.2.70, every \(f,g\in L^2(\mu _\lambda ;\mathbb {R})\) satisfies
with an integrable integrand. This assertion is conditional on the existence of \(T\) in that domain.
Lean Formalisation
theorem Real.PowerLawWeakRealization.spec {α lam : ℝ} (T : α.PowerLawWeakRealization lam)
(f g : ↥(MeasureTheory.Lp ℝ 2 (Polynomial.gegenbauerMeasure lam))) :
MeasureTheory.Integrable (fun z => ↑↑g z.1 * ↑↑f z.2) (α.powerLawKernelMeasure lam) ∧
inner ℝ g (↑T f) = ∫ (z : ℝ × ℝ), ↑↑g z.1 * ↑↑f z.2 ∂α.powerLawKernelMeasure lamLean proof
theorem PowerLawWeakRealization.spec {α lam : ℝ} (T : PowerLawWeakRealization α lam)
(f g : Lp ℝ 2 (gegenbauerMeasure lam)) :
Integrable (fun z : ℝ × ℝ ↦ g z.1*f z.2) (powerLawKernelMeasure α lam) ∧
⟪g,T.val f⟫_ℝ = ∫ z : ℝ × ℝ, g z.1*f z.2 ∂powerLawKernelMeasure α lam := T.property f gIf \(-1/2{\lt}\lambda \le 1/2\), \(0{\lt}\delta \le 1\), and \(1-\delta \le a{\lt}b\le 1\), then
For \(\alpha \le 0\), any bounded weak kernel realization \(T\) on \(L^2(\mu _\lambda ;\mathbb R)\) satisfies
More generally, separated measurable sets with \(\delta /4\le |x-y|\le \delta \) give the lower bound \(\delta ^\alpha \sqrt{\mu _\lambda (A)\mu _\lambda (B)}\le \| T\| \) when both masses are positive. Both bounds also hold for a weak kernel that agrees with the power kernel on the tested rectangle, or on the endpoint strip squared away from the diagonal, respectively. No diagonal value of a singular kernel is prescribed. Thus, for \(\alpha {\gt}-1\), \(\lambda {\gt}-1/2\) and \(\alpha +\lambda {\lt}-1/2\), no bounded same-space \(L^2\) operator has the stated weak power-law kernel.
Lean Formalisation
theorem Real.gegenbauerMeasure_endpoint_interval_lowerOn (lam : ↑(Set.Ioc (-(1 / 2)) (1 / 2))) (δ : ↑(Set.Ioc 0 1))
(a b : ↑(Set.Icc (1 - ↑δ) 1)) (hab : ↑a < ↑b) :
(2 * ↑δ) ^ (↑lam - 1 / 2) * (↑b - ↑a) ≤ (Polynomial.gegenbauerMeasure ↑lam).real (Set.Ioo ↑a ↑b)Lean proof
theorem gegenbauerMeasure_endpoint_interval_lowerOn (lam : Ioc (-(1/2) : ℝ) (1/2))
(δ : Ioc (0 : ℝ) 1) (a b : Icc (1-δ.val) (1 : ℝ)) (hab : a.val < b.val) :
(2*δ.val)^(lam.val-1/2)*(b.val-a.val) ≤ (gegenbauerMeasure lam.val).real (Ioo a.val b.val) :=
gegenbauerMeasure_endpoint_interval_lower lam.property.1 lam.property.2 δ.property.1 δ.property.2
a.property.1 hab b.property.2Assume \(\alpha {\gt}-1\) and \(\lambda {\gt}-1/2\). There exists a bounded operator \(T\) on \(L^2(\mu _\lambda ;\mathbb R)\) satisfying
with absolute integrability for every \(f,g\in L^2(\mu _\lambda ;\mathbb R)\) if and only if \(\alpha +\lambda \ge -1/2\). This includes \(\lambda =0\). It classifies this common-space realization; it is not a two-weight mapping criterion or an inverse-solver theorem.
Lean Formalisation
theorem Real.exists_powerLawL2Operator_iffOn (α : ↑(Set.Ioi (-1))) (lam : ↑(Set.Ioi (-(1 / 2)))) :
(∃ T,
(∀ (f g : ↥(MeasureTheory.Lp ℝ 2 (Polynomial.gegenbauerMeasure ↑lam))),
MeasureTheory.Integrable (fun z => ↑↑g z.1 * ↑↑f z.2) ((↑α).powerLawKernelMeasure ↑lam)) ∧
∀ (f g : ↥(MeasureTheory.Lp ℝ 2 (Polynomial.gegenbauerMeasure ↑lam))),
inner ℝ g (T f) = ∫ (z : ℝ × ℝ), ↑↑g z.1 * ↑↑f z.2 ∂(↑α).powerLawKernelMeasure ↑lam) ↔
-(1 / 2) ≤ ↑α + ↑lamLean proof
theorem exists_powerLawL2Operator_iffOn (α : Ioi (-1 : ℝ)) (lam : Ioi (-(1/2) : ℝ)) :
(∃ T : Lp ℝ 2 (gegenbauerMeasure lam.val) →L[ℝ] Lp ℝ 2 (gegenbauerMeasure lam.val),
(∀ f g : Lp ℝ 2 (gegenbauerMeasure lam.val),
Integrable (fun z : ℝ × ℝ ↦ g z.1*f z.2) (powerLawKernelMeasure α.val lam.val)) ∧
∀ f g, ⟪g,T f⟫_ℝ = ∫ z : ℝ × ℝ, g z.1*f z.2 ∂powerLawKernelMeasure α.val lam.val) ↔
-(1/2) ≤ α.val+lam.val := by
constructor
· rintro ⟨T,hi,he⟩
by_contra hnot
exact not_exists_powerLawL2Operator_below_endpointOn α lam (lt_of_not_ge hnot)
⟨⟨T,fun f g ↦ ⟨hi f g,he f g⟩⟩⟩
· intro hs
obtain ⟨M,T,_,_,hT⟩ := exists_powerLawL2Operator_of_le_endpointOn α lam hs
exact ⟨T,fun f g ↦ (hT f g).1,fun f g ↦ (hT f g).2⟩Reference details: Normalized coordinates including the Chebyshev limit and related results
The measures satisfy \(\mu _0=\mu _T\). For \(\lambda {\gt}-1/2\), choose the normalized Gegenbauer Hilbert basis when \(\lambda \ne 0\), and the normalized Chebyshev \(T\) Hilbert basis when \(\lambda =0\), transported along this equality of measures. Denote this basis by \((b_n)\) and its coordinate isometry by \(U\).
Lean Formalisation
theorem Polynomial.gegenbauerMeasure_zero : Polynomial.gegenbauerMeasure 0 = Polynomial.Chebyshev.classicalMeasureTLean proof
/-- The zero-parameter Gegenbauer measure is precisely the Chebyshev T measure. -/
theorem gegenbauerMeasure_zero : gegenbauerMeasure 0 = Chebyshev.classicalMeasureT := by
rw [gegenbauerMeasure_eq_jacobiMeasure, measureT_eq_jacobiMeasure]
norm_numThis is a case distinction in the choice of coordinates, not an assertion of continuity in \(\lambda \).
For \(\alpha {\gt}-1\), \(\lambda {\gt}-1/2\), and \(\alpha +\lambda \ge -1/2\), select the bounded operator on \(L^2(\mu _\lambda ;\mathbb {R})\) characterized by integrable pairings \(\langle g,Tf\rangle =\int g(x)f(y)\, dK_{\alpha ,\lambda }\) against the classical joint kernel measure.
Lean Formalisation
def Real.boundedPowerLawL2Operator {α lam : ℝ} (hα : -1 < α) (hlam : -(1 / 2) < lam) (hs : -(1 / 2) ≤ α + lam) :
↥(MeasureTheory.Lp ℝ 2 (Polynomial.gegenbauerMeasure lam)) →L[ℝ]
↥(MeasureTheory.Lp ℝ 2 (Polynomial.gegenbauerMeasure lam))Lean definition
/-- The unique weak kernel realization throughout the exact same-space boundedness range. -/
def boundedPowerLawL2Operator {α lam : ℝ} (hα : -1 < α) (hlam : -(1/2) < lam)
(hs : -(1/2) ≤ α+lam) :
Lp ℝ 2 (gegenbauerMeasure lam) →L[ℝ] Lp ℝ 2 (gegenbauerMeasure lam) :=
Classical.choose ((exists_powerLawL2Operator_iffOn ⟨α,hα⟩ ⟨lam,hlam⟩).mpr hs)Assume \(\alpha {\gt}-1\), \(\lambda {\gt}-1/2\) and \(\alpha +\lambda \ge -1/2\). For every \(f,g\in L^2(\mu _\lambda ;\mathbb {R})\), the function \((x,y)\mapsto g(x)f(y)\) is integrable against the classical joint kernel measure \(K_{\alpha ,\lambda }\), and
This identity for all \(f,g\) uniquely determines the bounded operator \(T\).
Lean Formalisation
theorem Real.boundedPowerLawL2Operator_spec {α lam : ℝ} (hα : -1 < α) (hlam : -(1 / 2) < lam) (hs : -(1 / 2) ≤ α + lam)
(f g : ↥(MeasureTheory.Lp ℝ 2 (Polynomial.gegenbauerMeasure lam))) :
MeasureTheory.Integrable (fun z => ↑↑g z.1 * ↑↑f z.2) (α.powerLawKernelMeasure lam) ∧
inner ℝ g ((Real.boundedPowerLawL2Operator hα hlam hs) f) =
∫ (z : ℝ × ℝ), ↑↑g z.1 * ↑↑f z.2 ∂α.powerLawKernelMeasure lamLean proof
theorem boundedPowerLawL2Operator_spec {α lam : ℝ} (hα : -1 < α)
(hlam : -(1/2) < lam) (hs : -(1/2) ≤ α+lam) (f g : Lp ℝ 2 (gegenbauerMeasure lam)) :
Integrable (fun z : ℝ × ℝ ↦ g z.1*f z.2) (powerLawKernelMeasure α lam) ∧
⟪g,boundedPowerLawL2Operator hα hlam hs f⟫_ℝ =
∫ z : ℝ × ℝ, g z.1*f z.2 ∂powerLawKernelMeasure α lam := by
have h := Classical.choose_spec ((exists_powerLawL2Operator_iffOn ⟨α,hα⟩ ⟨lam,hlam⟩).mpr hs)
exact ⟨h.1 f g,h.2 f g⟩Assume \(\alpha {\gt}-1\), \(\lambda {\gt}-1/2\) and \(\alpha +\lambda \ge -1/2\). There is a unique bounded operator \(T\) on \(L^2(\mu _\lambda ;\mathbb R)\) with
Every such pairing is absolutely integrable. This realization agrees with any earlier mass-bound construction and, on the critical line, with the weighted Schur construction.
Lean Formalisation
theorem Real.boundedPowerLawL2Operator_eq_massOn {α lam : ℝ} (p : α.PowerLawL2Data lam) (hs : -(1 / 2) ≤ α + lam) :
Real.boundedPowerLawL2Operator ⋯ ⋯ hs = Real.powerLawL2Operator pLean proof
theorem boundedPowerLawL2Operator_eq_massOn {α lam : ℝ} (p : PowerLawL2Data α lam)
(hs : -(1/2) ≤ α+lam) :
boundedPowerLawL2Operator p.exponent_mem p.weight_mem hs = powerLawL2Operator p :=
boundedPowerLawL2Operator_eqOn p.exponent_mem p.weight_mem hs _
(fun f g ↦ (powerLawL2Operator_spec p f g).2)For every \(\alpha {\gt}-1\), \(\lambda {\gt}-1/2\) and \(\alpha +\lambda \ge -1/2\), use the preceding basis and weak realization. Then \(A=UTU^{-1}\) satisfies
and its entries are the absolutely integrable kernel pairings
A uniform nonnegative mass bound \(M\) gives \(\| A\| \le M\); on the critical line \(\| A\| \le C_\alpha \). For \(\lambda \ne 0\), this operator equals the previous Gegenbauer coefficient constructions. At \(\lambda =0\) it uses normalized Chebyshev \(T\) coordinates and covers \(\alpha \ge -1/2\), including \(\alpha =-1/2\). There is no exclusion of zero from this full-range theorem. Convergence is strong for each input; no operator-norm convergence, new bandwidth assertion or inverse-solver convergence is claimed.
Lean Formalisation
theorem Real.norm_boundedPowerLawCoefficientOperator {α lam : ℝ} (hα : -1 < α) (hlam : -(1 / 2) < lam)
(hs : -(1 / 2) ≤ α + lam) :
‖Real.boundedPowerLawCoefficientOperator hα hlam hs‖ = ‖Real.boundedPowerLawL2Operator hα hlam hs‖Lean proof
/-- Coordinate transport preserves the full-range operator norm exactly. -/
theorem norm_boundedPowerLawCoefficientOperator {α lam : ℝ}
(hα : -1 < α) (hlam : -(1/2) < lam) (hs : -(1/2) ≤ α+lam) :
‖boundedPowerLawCoefficientOperator hα hlam hs‖ = ‖boundedPowerLawL2Operator hα hlam hs‖ :=
(powerLawHilbertBasis hlam).norm_coefficientOperator _Reference details: Classical two-weight Schur operator and related results
For positive measurable weights \(h\) for \(\mu \) and \(g\) for \(\nu \), and a joint measure with marginals bounded by \(C h^2\mu \) and \(D g^2\nu \), where \(C,D\) are finite and nonnegative, define \(T=D_h^* S D_g\). Here \(S\) is the ordinary Schur operator between the two tilted \(L^2\) spaces.
Lean Formalisation
def MeasureTheory.twoWeightSchurL2Operator.{u_1, u_2} {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y]
(μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) (κ : MeasureTheory.Measure (X × Y))
(h : MeasureTheory.PositiveWeight μ) (g : MeasureTheory.PositiveWeight ν) {C D : ENNReal} (hC : C ≠ ⊤) (hD : D ≠ ⊤)
(hfst : MeasureTheory.Measure.map Prod.fst κ ≤ C • μ.withDensity fun x => ENNReal.ofReal (↑h x ^ 2))
(hsnd : MeasureTheory.Measure.map Prod.snd κ ≤ D • ν.withDensity fun y => ENNReal.ofReal (↑g y ^ 2)) :
↥(MeasureTheory.Lp ℝ 2 ν) →L[ℝ] ↥(MeasureTheory.Lp ℝ 2 μ)Lean definition
/-- The weighted Schur operator, obtained by conjugating the ordinary Schur construction. -/
def twoWeightSchurL2Operator (μ : Measure X) (ν : Measure Y) (κ : Measure (X × Y))
(h : PositiveWeight μ) (g : PositiveWeight ν)
{C D : ℝ≥0∞} (hC : C ≠ ∞) (hD : D ≠ ∞)
(hfst : κ.map Prod.fst ≤ C • μ.withDensity (fun x ↦ ENNReal.ofReal (h.val x^2)))
(hsnd : κ.map Prod.snd ≤ D • ν.withDensity (fun y ↦ ENNReal.ofReal (g.val y^2))) :
Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 μ :=
(divWeightL2 μ h).toContinuousLinearMap.adjoint.comp
((schurL2Operator _ _ κ hC hD hfst hsnd).comp
(divWeightL2 ν g).toContinuousLinearMap)Let \(\mu \) on \(X\) and \(\nu \) on \(Y\) have measurable positive almost-everywhere auxiliary weights \(h,g\). If a joint measure \(\kappa \) satisfies
for finite nonnegative \(C,D\), then there is a bounded \(T:L^2(\nu ;\mathbb R)\to L^2(\mu ;\mathbb R)\) with
The pairing is absolutely integrable for all \(u,v\). No finiteness of the original or tilted measures, or square-integrability of \(h,g\), is required.
Lean Formalisation
theorem MeasureTheory.norm_twoWeightSchurL2Operator_le.{u_1, u_2} {X : Type u_1} {Y : Type u_2} [MeasurableSpace X]
[MeasurableSpace Y] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) (κ : MeasureTheory.Measure (X × Y))
(h : MeasureTheory.PositiveWeight μ) (g : MeasureTheory.PositiveWeight ν) {C D : ENNReal} (hC : C ≠ ⊤) (hD : D ≠ ⊤)
(hfst : MeasureTheory.Measure.map Prod.fst κ ≤ C • μ.withDensity fun x => ENNReal.ofReal (↑h x ^ 2))
(hsnd : MeasureTheory.Measure.map Prod.snd κ ≤ D • ν.withDensity fun y => ENNReal.ofReal (↑g y ^ 2)) :
‖MeasureTheory.twoWeightSchurL2Operator μ ν κ h g hC hD hfst hsnd‖ ≤ √C.toReal * √D.toRealLean proof
/-- The weighted Schur construction retains the marginal norm bound. -/
theorem norm_twoWeightSchurL2Operator_le (μ : Measure X) (ν : Measure Y) (κ : Measure (X × Y))
(h : PositiveWeight μ) (g : PositiveWeight ν)
{C D : ℝ≥0∞} (hC : C ≠ ∞) (hD : D ≠ ∞)
(hfst : κ.map Prod.fst ≤ C • μ.withDensity (fun x ↦ ENNReal.ofReal (h.val x^2)))
(hsnd : κ.map Prod.snd ≤ D • ν.withDensity (fun y ↦ ENNReal.ofReal (g.val y^2))) :
‖twoWeightSchurL2Operator μ ν κ h g hC hD hfst hsnd‖ ≤
Real.sqrt C.toReal * Real.sqrt D.toReal := by
let A := (divWeightL2 μ h).toContinuousLinearMap
let B := (divWeightL2 ν g).toContinuousLinearMap
let S := schurL2Operator _ _ κ hC hD hfst hsnd
have ha : ‖A‖ ≤ 1 := (divWeightL2 μ h).norm_toContinuousLinearMap_le
have hb : ‖B‖ ≤ 1 := (divWeightL2 ν g).norm_toContinuousLinearMap_le
have hs := norm_schurL2Operator_le _ _ κ hC hD hfst hsnd
change ‖A.adjoint.comp (S.comp B)‖ ≤ _
apply (ContinuousLinearMap.opNorm_comp_le _ _).trans
rw [ContinuousLinearMap.adjoint.norm_map]
calc
_ ≤ 1 * (‖S‖ * ‖B‖) := mul_le_mul ha (ContinuousLinearMap.opNorm_comp_le _ _)
(norm_nonneg _) (by norm_num)
_ ≤ 1 * ((Real.sqrt C.toReal * Real.sqrt D.toReal) * 1) := by gcongr
_ = _ := by ringFor real or complex Hilbert bases \((a_j)\) of \(E\) and \((b_i)\) of \(F\) and bounded \(T:E\to F\), the coefficient map \(A=U_F T U_E^{-1}\) satisfies
The source and target spaces and bases may differ.
Lean Formalisation
theorem HilbertBasis.coefficientMap_repr.{u_1, u_2, u_3} {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} {F : Type u_3}
[NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (a : HilbertBasis ℕ 𝕜 E)
(b : HilbertBasis ℕ 𝕜 F) (T : E →L[𝕜] F) (f : E) : (a.coefficientMap b T) (a.repr f) = b.repr (T f)Lean proof
/-- The transported operator agrees exactly with Hilbert-basis coordinates. -/
theorem coefficientMap_repr (a : HilbertBasis ℕ 𝕜 E) (b : HilbertBasis ℕ 𝕜 F) (T : E →L[𝕜] F) (f : E) :
a.coefficientMap b T (a.repr f) = b.repr (T f) := by
change b.repr (T (a.repr.symm (a.repr f))) = _
rw [LinearIsometryEquiv.symm_apply_apply]For a common exponent \(\alpha {\gt}-1\), assume the uniform mass bounds of Definition 6.2.35 for input weight \(\lambda {\gt}-1/2\) and output weight \(\tau {\gt}-1/2\), with respective bounds \(M,N\ge 0\). Define \(T:L^2(\mu _\lambda )\to L^2(\mu _\tau )\) by the Schur construction for the classical two-weight joint kernel measure.
Lean Formalisation
def Real.twoWeightPowerLawL2Operator {α lam tau : ℝ} (p : α.PowerLawL2Data lam) (q : α.PowerLawL2Data tau) :
↥(MeasureTheory.Lp ℝ 2 (Polynomial.gegenbauerMeasure lam)) →L[ℝ]
↥(MeasureTheory.Lp ℝ 2 (Polynomial.gegenbauerMeasure tau))Lean definition
def twoWeightPowerLawL2Operator (p : PowerLawL2Data α lam) (q : PowerLawL2Data α tau) :
Lp ℝ 2 (gegenbauerMeasure lam) →L[ℝ] Lp ℝ 2 (gegenbauerMeasure tau) :=
schurL2Operator _ _ (twoWeightPowerLawKernelMeasure α tau lam) (by simp) (by simp)
(p.twoWeight_kernel_fst tau)
(q.twoWeight_kernel_snd lam (sFinite_gegenbauerMeasure lam))For \(T:L^2(\mu _\lambda ;\mathbb {R})\to L^2(\mu _\tau ;\mathbb {R})\) in the two-weight realization domain, every \(f\in L^2(\mu _\lambda ;\mathbb {R})\) and \(g\in L^2(\mu _\tau ;\mathbb {R})\) satisfy: \(g(x)f(y)\) is integrable against the joint kernel measure and its integral equals \(\langle g,Tf\rangle \).
Lean Formalisation
theorem Real.twoWeightPowerLawL2Operator_spec {α lam tau : ℝ} (p : α.PowerLawL2Data lam) (q : α.PowerLawL2Data tau)
(f : ↥(MeasureTheory.Lp ℝ 2 (Polynomial.gegenbauerMeasure lam)))
(g : ↥(MeasureTheory.Lp ℝ 2 (Polynomial.gegenbauerMeasure tau))) :
MeasureTheory.Integrable (fun z => ↑↑g z.1 * ↑↑f z.2) (α.twoWeightPowerLawKernelMeasure tau lam) ∧
inner ℝ g ((Real.twoWeightPowerLawL2Operator p q) f) =
∫ (z : ℝ × ℝ), ↑↑g z.1 * ↑↑f z.2 ∂α.twoWeightPowerLawKernelMeasure tau lamLean proof
theorem twoWeightPowerLawL2Operator_spec (p : PowerLawL2Data α lam) (q : PowerLawL2Data α tau)
(f : Lp ℝ 2 (gegenbauerMeasure lam)) (g : Lp ℝ 2 (gegenbauerMeasure tau)) :
Integrable (fun z : ℝ × ℝ ↦ g z.1*f z.2) (twoWeightPowerLawKernelMeasure α tau lam) ∧
⟪g,twoWeightPowerLawL2Operator p q f⟫_ℝ =
∫ z : ℝ × ℝ, g z.1*f z.2 ∂twoWeightPowerLawKernelMeasure α tau lam := by
constructor
· exact integrable_schurL2_pair _ _ (twoWeightPowerLawKernelMeasure α tau lam) (by simp) (by simp)
(p.twoWeight_kernel_fst tau)
(q.twoWeight_kernel_snd lam (sFinite_gegenbauerMeasure lam)) f g
· exact inner_schurL2Operator _ _ (twoWeightPowerLawKernelMeasure α tau lam) (by simp) (by simp)
(p.twoWeight_kernel_fst tau)
(q.twoWeight_kernel_snd lam (sFinite_gegenbauerMeasure lam)) f gLet \(\alpha {\gt}-1\), \(\lambda ,\tau {\gt}-1/2\). Suppose the input-weight row masses are bounded by \(M\ge 0\) and the output-weight row masses by \(N\ge 0\) throughout \((-1,1)\). Then the kernel measure with density \(|x-y|^\alpha \) on \(\{ (x,y)\in (-1,1)^2:x\ne y\} \) against \(\mu _\tau \otimes \mu _\lambda \) defines \(T:L^2(\mu _\lambda )\to L^2(\mu _\tau )\), with
Every weak pairing is absolutely integrable. Fubini provides an integrable function \(F\) on the output space and, for \(\mu _\tau \)-almost every \(x\), an integrable function \(y\mapsto |x-y|^\alpha g(x)w_\lambda (y)f(y)\) on \(D_x\) whose integral is \(F(x)\), with \(\langle g,Tf\rangle =\int F\, d\mu _\tau \). Such positive mass bounds exist whenever \(\alpha +\lambda {\gt}-1/2\) and \(\alpha +\tau {\gt}-1/2\).
Lean Formalisation
theorem Real.twoWeightPowerLawKernelMeasure_fst_leOn {α lam : ℝ} (p : α.PowerLawL2Data lam) (tau : ℝ) :
MeasureTheory.Measure.map Prod.fst (α.twoWeightPowerLawKernelMeasure tau lam) ≤
ENNReal.ofReal ↑p.bound • Polynomial.gegenbauerMeasure tauLean proof
theorem twoWeightPowerLawKernelMeasure_fst_leOn (p : PowerLawL2Data α lam) (tau : ℝ) :
(twoWeightPowerLawKernelMeasure α tau lam).map Prod.fst ≤
ENNReal.ofReal p.bound • gegenbauerMeasure tau :=
p.twoWeight_kernel_fst tauThese are sufficient conditions, not a sharp two-weight classification.
Reference details: Two-weight coefficient map and related results
Define \(A=U_\tau T U_\lambda ^{-1}\) using the normalized source and target Hilbert bases, including the Chebyshev \(T\) choice at a zero parameter.
Lean Formalisation
def Real.twoWeightPowerLawCoefficientOperator {α lam tau : ℝ} (p : α.PowerLawL2Data lam) (q : α.PowerLawL2Data tau) :
↥(lp (fun x => ℝ) 2) →L[ℝ] ↥(lp (fun x => ℝ) 2)Lean definition
def twoWeightPowerLawCoefficientOperator (p : PowerLawL2Data α lam) (q : PowerLawL2Data α tau) :
lp (fun _ : ℕ ↦ ℝ) 2 →L[ℝ] lp (fun _ : ℕ ↦ ℝ) 2 :=
(powerLawHilbertBasis p.weight_mem).coefficientMap (powerLawHilbertBasis q.weight_mem)
(twoWeightPowerLawL2Operator p q)For the two-weight operator \(T:L^2(\mu _\lambda ;\mathbb {R})\to L^2(\mu _\tau ;\mathbb {R})\) and coordinate isometries \(U_\lambda ,U_\tau \), its coefficient map \(A\) satisfies
Lean Formalisation
theorem Real.twoWeightPowerLawCoefficientOperator_reprOn {α lam tau : ℝ} (p : α.PowerLawL2Data lam) (q : α.PowerLawL2Data tau)
(f : ↥(MeasureTheory.Lp ℝ 2 (Polynomial.gegenbauerMeasure lam))) :
(Real.twoWeightPowerLawCoefficientOperator p q) ((Polynomial.powerLawHilbertBasis ⋯).repr f) =
(Polynomial.powerLawHilbertBasis ⋯).repr ((Real.twoWeightPowerLawL2Operator p q) f)Lean proof
theorem twoWeightPowerLawCoefficientOperator_reprOn (p : PowerLawL2Data α lam)
(q : PowerLawL2Data α tau) (f : Lp ℝ 2 (gegenbauerMeasure lam)) :
twoWeightPowerLawCoefficientOperator p q ((powerLawHilbertBasis p.weight_mem).repr f) =
(powerLawHilbertBasis q.weight_mem).repr (twoWeightPowerLawL2Operator p q f) :=
(powerLawHilbertBasis p.weight_mem).coefficientMap_repr (powerLawHilbertBasis q.weight_mem) _ fUnder the preceding mass-bound hypotheses, use normalized Gegenbauer coordinates at each nonzero parameter and normalized Chebyshev \(T\) coordinates at zero. The coefficient map \(A=U_\tau T U_\lambda ^{-1}\) preserves the operator norm, intertwines the action, and has entries
For every \(c\in \ell ^2\), \(P_NAP_Nc\to Ac\) strongly. Either or both weight parameters may be zero.
Lean Formalisation
theorem Real.norm_twoWeightPowerLawCoefficientOperatorOn {α lam tau : ℝ} (p : α.PowerLawL2Data lam) (q : α.PowerLawL2Data tau) :
‖Real.twoWeightPowerLawCoefficientOperator p q‖ = ‖Real.twoWeightPowerLawL2Operator p q‖Lean proof
theorem norm_twoWeightPowerLawCoefficientOperatorOn (p : PowerLawL2Data α lam)
(q : PowerLawL2Data α tau) :
‖twoWeightPowerLawCoefficientOperator p q‖ = ‖twoWeightPowerLawL2Operator p q‖ :=
(powerLawHilbertBasis p.weight_mem).norm_coefficientMap (powerLawHilbertBasis q.weight_mem) _No additional bandwidth or inverse-solver convergence is asserted.
Assume \(\alpha {\gt}-1\), \(\lambda {\gt}-1/2\) and \(\alpha +\lambda \ge -1/2\). Let \(A\) be the weak realization of
Then \(\langle g,Af\rangle =\langle f,Ag\rangle \) for all real \(L^2(\mu _\lambda )\) vectors. Both \(A\) and its normalized coefficient operator are self-adjoint, including on the critical boundary and at \(\lambda =0\), where the normalized basis is Chebyshev \(T\).
Lean Formalisation
theorem Real.inner_boundedPowerLawL2Operator_symm {α lam : ℝ} (hα : -1 < α) (hlam : -(1 / 2) < lam) (hs : -(1 / 2) ≤ α + lam)
(f g : ↥(MeasureTheory.Lp ℝ 2 (Polynomial.gegenbauerMeasure lam))) :
inner ℝ g ((Real.boundedPowerLawL2Operator hα hlam hs) f) = inner ℝ f ((Real.boundedPowerLawL2Operator hα hlam hs) g)Lean proof
/-- Symmetry of the weak kernel holds for every pair of weighted L² vectors. -/
theorem inner_boundedPowerLawL2Operator_symm
(f g : Lp ℝ 2 (gegenbauerMeasure lam)) :
⟪g, boundedPowerLawL2Operator hα hlam hs f⟫_ℝ =
⟪f, boundedPowerLawL2Operator hα hlam hs g⟫_ℝ := by
let := isFiniteMeasure_gegenbauerMeasure hlam
obtain ⟨K,hK,he,hz,hμ⟩ := exists_powerLawKernel_density α
have hsym (z : ℝ × ℝ) : K z.swap = K z := by
by_cases h : z.1 ∈ Ioo (-1 : ℝ) 1 ∧ z.2 ∈ Ioo (-1 : ℝ) 1 ∧ z.1 ≠ z.2
· apply NNReal.eq
rw [he ⟨z,h⟩,he ⟨z.swap,h.2.1,h.1,h.2.2.symm⟩]
change |z.2-z.1|^α = |z.1-z.2|^α
rw [abs_sub_comm]
· rw [hz z h,hz z.swap (fun hs ↦ h ⟨hs.2.1,hs.1,hs.2.2.symm⟩)]
have hm : powerLawKernelMeasure α lam =
((gegenbauerMeasure lam).prod (gegenbauerMeasure lam)).withDensity
(fun z ↦ (K z : ℝ≥0∞)) := hμ lam lam
rw [(boundedPowerLawL2Operator_spec hα hlam hs f g).2,(boundedPowerLawL2Operator_spec hα hlam hs g f).2,hm,
integral_withDensity_eq_integral_toReal_smul hK.coe_nnreal_ennreal (by simp),
integral_withDensity_eq_integral_toReal_smul hK.coe_nnreal_ennreal (by simp)]
rw [← integral_prod_swap]
apply integral_congr_ae
filter_upwards [] with z
simp only [ENNReal.coe_toReal,smul_eq_mul,Prod.swap,mul_comm]
rw [show K (z.2,z.1) = K z from hsym z]Reference details: Domination of weak kernels controls operator norms and related results
Let \(\mu \) be an s-finite measure. Let bounded real \(L^2(\mu )\) operators \(T,S\) have weak kernels \(k,q\), respectively, with all their weak pairings absolutely integrable. If \(c\ge 0\) and \(|k(x,y)|\le c q(x,y)\) almost everywhere for \(\mu \otimes \mu \), then \(\| T\| \le c\| S\| \).
Lean Formalisation
theorem MeasureTheory.norm_le_of_dominated_weak_kernel.{u_1} {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X)
[MeasureTheory.SFinite μ] (T S : ↥(MeasureTheory.Lp ℝ 2 μ) →L[ℝ] ↥(MeasureTheory.Lp ℝ 2 μ)) (k q : X × X → ℝ)
(ik : ∀ (f g : ↥(MeasureTheory.Lp ℝ 2 μ)), MeasureTheory.Integrable (fun z => k z * (↑↑g z.1 * ↑↑f z.2)) (μ.prod μ))
(iq : ∀ (f g : ↥(MeasureTheory.Lp ℝ 2 μ)), MeasureTheory.Integrable (fun z => q z * (↑↑g z.1 * ↑↑f z.2)) (μ.prod μ))
(hT : ∀ (f g : ↥(MeasureTheory.Lp ℝ 2 μ)), inner ℝ g (T f) = ∫ (z : X × X), k z * (↑↑g z.1 * ↑↑f z.2) ∂μ.prod μ)
(hS : ∀ (f g : ↥(MeasureTheory.Lp ℝ 2 μ)), inner ℝ g (S f) = ∫ (z : X × X), q z * (↑↑g z.1 * ↑↑f z.2) ∂μ.prod μ)
{c : ℝ} (hc : 0 ≤ c) (hb : ∀ᵐ (z : X × X) ∂μ.prod μ, ‖k z‖ ≤ c * q z) : ‖T‖ ≤ c * ‖S‖Lean proof
/-- Domination of weak kernels controls operator norms. Both weak pairings are
assumed absolutely integrable, so no pointwise representative is required. -/
theorem norm_le_of_dominated_weak_kernel
(T S : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ) (k q : X × X → ℝ)
(ik : ∀ f g : Lp ℝ 2 μ, Integrable (fun z ↦ k z*(g z.1*f z.2)) (μ.prod μ))
(iq : ∀ f g : Lp ℝ 2 μ, Integrable (fun z ↦ q z*(g z.1*f z.2)) (μ.prod μ))
(hT : ∀ f g, ⟪g, T f⟫_ℝ = ∫ z, k z*(g z.1*f z.2) ∂μ.prod μ)
(hS : ∀ f g, ⟪g, S f⟫_ℝ = ∫ z, q z*(g z.1*f z.2) ∂μ.prod μ)
{c : ℝ} (hc : 0 ≤ c) (hb : ∀ᵐ z ∂μ.prod μ, ‖k z‖ ≤ c*q z) :
‖T‖ ≤ c*‖S‖ := by
apply ContinuousLinearMap.opNorm_le_of_re_inner_le (mul_nonneg hc (norm_nonneg S))
intro f g hf hg
let f0 := (Lp.memLp f).norm.toLp (fun x ↦ ‖f x‖)
let g0 := (Lp.memLp g).norm.toLp (fun x ↦ ‖g x‖)
have hef := (Measure.quasiMeasurePreserving_snd (μ := μ) (ν := μ)).ae_eq_comp
(Lp.memLp f).norm.coeFn_toLp
have heg := (Measure.quasiMeasurePreserving_fst (μ := μ) (ν := μ)).ae_eq_comp
(Lp.memLp g).norm.coeFn_toLp
have hbound : ‖⟪g, T f⟫_ℝ‖ ≤ c*⟪g0, S f0⟫_ℝ := by
rw [hT, hS, ← integral_const_mul]
refine (norm_integral_le_integral_norm _).trans (integral_mono_ae (ik f g).norm
((iq f0 g0).const_mul c) ?_)
filter_upwards [hb, hef, heg] with z hz hfz hgz
change f0 z.2 = ‖f z.2‖ at hfz
change g0 z.1 = ‖g z.1‖ at hgz
rw [hfz, hgz, norm_mul, norm_mul]
nlinarith [mul_le_mul_of_nonneg_right hz (mul_nonneg (norm_nonneg (g z.1))
(norm_nonneg (f z.2)))]
have hn : ⟪g0, S f0⟫_ℝ ≤ ‖S‖ := by
apply (real_inner_le_norm _ _).trans
calc
‖g0‖*‖S f0‖ ≤ ‖g0‖*(‖S‖*‖f0‖) :=
mul_le_mul_of_nonneg_left (S.le_opNorm f0) (norm_nonneg _)
_ = ‖S‖ := by rw [norm_norm_toLp, norm_norm_toLp, hf, hg]; ring
change ⟪T f, g⟫_ℝ ≤ _
rw [real_inner_comm]
exact (le_abs_self _).trans (hbound.trans (mul_le_mul_of_nonneg_left hn hc))Let \(\mu \) be a finite Borel measure on \(\mathbb R\) and \(k\) a continuous real kernel on \(\mathbb R^2\) with \(|k|\le M\), \(M\ge 0\). Each row \(r_x=k(x,\cdot )\) defines an \(L^2(\mu )\) vector, continuously in \(x\), and \(\| r_x\| \le \sqrt{\mu (\mathbb R)}M\). For \(f\in L^2(\mu )\), its row pairing belongs to \(L^2(\mu )\) and represents the bounded-kernel operator almost everywhere:
If \(\mu \) is concentrated on a compact set and a countable Hilbert basis of \(L^2(\mu )\) is given, then \(T_k\) is compact.
Lean Formalisation
theorem MeasureTheory.memLp_continuousKernel_row (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] {k : ℝ × ℝ → ℝ}
(hk : Continuous k) {M : ℝ} (hb : ∀ (z : ℝ × ℝ), ‖k z‖ ≤ M) (x : ℝ) : MeasureTheory.MemLp (fun y => k (x, y)) 2 μLean proof
/-- A bounded continuous kernel row belongs to L². -/
theorem memLp_continuousKernel_row (x : ℝ) : MemLp (fun y ↦ k (x,y)) 2 μ :=
MemLp.of_bound (hk.comp (continuous_const.prodMk continuous_id)).aestronglyMeasurable M
(Eventually.of_forall (fun y ↦ hb (x,y)))For a real exponent \(\alpha \), admissible cutoffs satisfy \(\delta {\gt}0\) or \(\alpha \ge 0\). On \(\mathbb {R}^2\) define
A zero base is allowed only for a nonnegative exponent, with \(0^0=1\). For comparison with the unregularized kernel, the physical off-diagonal domain consists of pairs \(x,y\in [-1,1]\) with \(x\ne y\).
Lean Formalisation
def Real.PowerLawCutoff (α : ℝ) : TypeLean definition
/-- A bounded continuous regularization of the distance power on [-1,1]². -/
abbrev PowerLawCutoff (α : ℝ) := {δ : ℝ // 0 < δ ∨ 0 ≤ α}For real \(\alpha \) and an admissible cutoff \(\delta \) (that is, \(\delta {\gt}0\) or \(\alpha \ge 0\)), the regularized kernel is
Its base is positive if \(\delta {\gt}0\); otherwise it is nonnegative and \(\alpha \ge 0\). For every admissible cutoff, \(k_{\alpha ,\delta }\) is continuous on \(\mathbb {R}^2\).
Lean Formalisation
theorem Real.regularizedPowerLawKernel_apply (α : ℝ) (δ : α.PowerLawCutoff) (z : ℝ × ℝ) :
α.regularizedPowerLawKernel δ z = max (↑δ) (min |z.1 - z.2| 2) ^ αLean proof
theorem regularizedPowerLawKernel_apply (α : ℝ) (δ : PowerLawCutoff α) (z : ℝ × ℝ) :
regularizedPowerLawKernel α δ z = (max δ.val (min |z.1-z.2| 2)) ^ α := rflDefine \(k_{\alpha ,\delta }(x,y)=(\max \{ \delta ,\min \{ |x-y|,2\} \} )^\alpha \). For \(\delta {\gt}0\) this is continuous; if \(\delta \le 2\), then \(|k_{\alpha ,\delta }|\le \delta ^\alpha +2^\alpha \) globally. For \(\beta {\lt}\alpha \), \(\beta \le 0\), and distinct \(x,y\in [-1,1]\),
Whenever \(\alpha {\gt}-1\), \(\lambda {\gt}-1/2\), and \(\alpha +\lambda {\gt}-1/2\), there exists \(\beta {\lt}\min \{ \alpha ,0\} \) with \(\beta {\gt}-1\) and \(\beta +\lambda {\gt}-1/2\).
Lean Formalisation
theorem Real.norm_regularizedPowerLawKernel_le_on (α : ℝ) (δ : ↑(Set.Ioc 0 2)) (z : ℝ × ℝ) :
‖α.regularizedPowerLawKernel ⟨↑δ, ⋯⟩ z‖ ≤ ↑δ ^ α + 2 ^ αLean proof
theorem norm_regularizedPowerLawKernel_le_on (α : ℝ) (δ : Ioc (0 : ℝ) 2)
(z : ℝ × ℝ) :
‖regularizedPowerLawKernel α ⟨δ.val,Or.inl δ.property.1⟩ z‖ ≤ δ.val^α+(2 : ℝ)^α :=
norm_regularizedPowerLawKernel_le α δ.property.1 δ.property.2 zLet \(R_{\alpha ,\delta }\) be the bounded realization of \(k_{\alpha ,\delta }\) on \(L^2(\mu _\lambda )\), \(\lambda {\gt}-1/2\), \(0{\lt}\delta \le 2\). It is compact. If both exponents \(\alpha ,\beta \) belong to the boundedness range, \(\beta {\lt}\alpha \), and \(\beta \le 0\), then
Consequently, for \(\alpha {\gt}-1\) and \(\alpha +\lambda {\gt}-1/2\), \(R_{\alpha ,1/(n+1)}\to A_\alpha \) in operator norm and \(A_\alpha \) is compact. Its normalized coefficient realization \(\widehat A_\alpha \) is compact too, and
Lean Formalisation
theorem Real.isCompactOperator_regularizedPowerLawL2Operator {lam : ℝ} (hlam : -(1 / 2) < lam) (α : ℝ) {δ : ℝ} (hδ : 0 < δ)
(hδ2 : δ ≤ 2) : IsCompactOperator ⇑(Real.regularizedPowerLawL2Operator hlam α hδ hδ2)Lean proof
/-- Every positive-cutoff regularization is compact. -/
theorem isCompactOperator_regularizedPowerLawL2Operator (α : ℝ)
{δ : ℝ} (hδ : 0 < δ) (hδ2 : δ ≤ 2) :
IsCompactOperator (regularizedPowerLawL2Operator hlam α hδ hδ2) := by
let := isFiniteMeasure_gegenbauerMeasure hlam
apply isCompactOperator_boundedKernelL2Operator_of_continuous _
(continuous_regularizedPowerLawKernel α hδ) _
(norm_regularizedPowerLawKernel_le α hδ hδ2) (powerLawHilbertBasis hlam) isCompact_Icc
exact (ae_mem_Ioo_gegenbauerMeasure lam).mono (fun _ hx ↦ Ioo_subset_Icc_self hx)No assertion of compactness on the critical boundary is made here.
Throughout the boundedness range, \(I-cA\) is invertible precisely when \(I-c\widehat A\) is invertible. The condition \(|c|\| A\| {\lt}1\) is sufficient. Assuming invertibility, \(u-cAu=f\) has a unique physical \(L^2\) solution for every right-hand side. In the strict range \(\alpha +\lambda {\gt}-1/2\), let \(B_N=I-cP_N\widehat A\) and assume \(I-c\widehat A\) invertible. For all sufficiently large \(N\), \(B_N\) is invertible with
For every coefficient right-hand side \(f\), the projected equations
have exactly one solution, as does the corresponding actual \(N\times N\) matrix equation. On the cofinal set of invertible cutoffs, the solutions \(u_N=B_N^{-1}P_Nf\) converge to \(u=(I-c\widehat A)^{-1}f\) and eventually satisfy
These results concern linear integral equations, not equilibrium or optimisation problems.
Lean Formalisation
theorem Real.isUnit_one_sub_smul_powerLawCoefficientOperator_iff {α lam c : ℝ} (hα : -1 < α) (hlam : -(1 / 2) < lam)
(hs : -(1 / 2) ≤ α + lam) :
IsUnit (1 - c • Real.boundedPowerLawCoefficientOperator hα hlam hs) ↔
IsUnit (1 - c • Real.boundedPowerLawL2Operator hα hlam hs)Lean proof
/-- The physical and normalized coefficient second-kind equations have exactly
the same invertibility condition. -/
theorem isUnit_one_sub_smul_powerLawCoefficientOperator_iff
{α lam c : ℝ} (hα : -1 < α) (hlam : -(1/2) < lam) (hs : -(1/2) ≤ α+lam) :
IsUnit (1 - c • boundedPowerLawCoefficientOperator hα hlam hs) ↔
IsUnit (1 - c • boundedPowerLawL2Operator hα hlam hs) := by
let e := (powerLawHilbertBasis hlam).repr.toContinuousLinearEquiv.conjContinuousAlgEquiv
have h := MulEquiv.isUnit_map (f := e.toAlgEquiv.toMulEquiv)
(x := 1 - c • boundedPowerLawL2Operator hα hlam hs)
change IsUnit (e (1 - c • boundedPowerLawL2Operator hα hlam hs)) ↔ _ at h
rw [map_sub, map_one, map_smul] at h
exact hInvertibility is an explicit hypothesis: no claim is made for every coupling \(c\).
Reference details: Vanishing multipliers and compact operators
On real \(L^2(\mu )\), let \(Q_n\) multiply by measurable \(q_n\) with \(|q_n|\le M\) almost everywhere, uniformly in \(n\). If \(q_n\to 0\) almost everywhere, then \(Q_nf\to 0\) for every \(f\in L^2(\mu )\). If \(T\) is compact, \(\| Q_nT\| \to 0\). A real bounded multiplier is self-adjoint. For finite \(\mu \), if \(T\) has weak kernel \(k(x,y)\) whose pairings \(k(x,y)g(x)f(y)\) are integrable for every \(f,g\in L^2(\mu ;\mathbb R)\), multiplication of its output by \(q(x)\) gives integrable weak pairings with kernel \(q(x)k(x,y)\).
Lean Formalisation
theorem MeasureTheory.inner_boundedMulL2.{u_1} {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) (q : X → ℝ)
(hq : MeasureTheory.AEStronglyMeasurable q μ) {M : ℝ} (hM : 0 ≤ M) (hb : ∀ᵐ (x : X) ∂μ, ‖q x‖ ≤ M)
(f g : ↥(MeasureTheory.Lp ℝ 2 μ)) :
inner ℝ g ((MeasureTheory.boundedMulL2 μ q hq hM hb) f) = inner ℝ ((MeasureTheory.boundedMulL2 μ q hq hM hb) g) fLean proof
/-- Move a real bounded multiplier across the L² pairing. -/
theorem inner_boundedMulL2 (q : X → ℝ) (hq : AEStronglyMeasurable q μ)
{M : ℝ} (hM : 0 ≤ M) (hb : ∀ᵐ x ∂μ, ‖q x‖ ≤ M) (f g : Lp ℝ 2 μ) :
⟪g, boundedMulL2 μ q hq hM hb f⟫_ℝ = ⟪boundedMulL2 μ q hq hM hb g, f⟫_ℝ := by
simp only [L2.inner_def]
apply integral_congr_ae
filter_upwards [boundedMulL2_ae μ q hq hM hb f,
boundedMulL2_ae μ q hq hM hb g] with x hf hg
simp only [Real.inner_apply, hf, hg]
ringLet \(\alpha {\gt}-1\), \(\lambda {\gt}-1/2\) and \(\alpha +\lambda \ge -1/2\). The bounded power-law operator \(A\) on \(L^2(\mu _\lambda )\) and its normalized coefficient operator \(\widehat A\) satisfy
More generally, every bounded weak realization of the kernel on the critical line \(\alpha +\lambda =-1/2\) is noncompact.
Lean Formalisation
theorem Real.not_isCompactOperator_powerLaw_criticalOn (α : ↑(Set.Ioi (-1))) (lam : ↑(Set.Ioi (-(1 / 2))))
(hc : ↑α + ↑lam = -(1 / 2)) (T : (↑α).PowerLawWeakRealization ↑lam) : ¬IsCompactOperator ⇑↑TLean proof
theorem not_isCompactOperator_powerLaw_criticalOn
(α : Ioi (-1 : ℝ)) (lam : Ioi (-(1/2) : ℝ))
(hc : α.val+lam.val = -(1/2)) (T : PowerLawWeakRealization α.val lam.val) :
¬ IsCompactOperator T.val := by
exact not_isCompactOperator_powerLaw_critical_of_pairing α.property lam.property hc T.val T.propertyReference details: Small-norm finite sections without compactness and related results
Let \(E\) be a real or complex Banach space and \(T:E\to E\) bounded with \(\| T\| \le q{\lt}1\). Then \(I-T\) is invertible and \(\| (I-T)^{-1}\| \le (1-q)^{-1}\). For any bounded \(P\) with \(\| P\| \le 1\), the lifted section \(B_P=I-PT\) is invertible with the same inverse bound, and
If \(P_n\) are contractions converging strongly to \(I\), then for every \(f\), \(B_{P_n}^{-1}P_nf\to (I-T)^{-1}f\). These estimates need neither compactness nor idempotence; for projections, the earlier range and projected-equation lemmas identify the actual finite solve.
Lean Formalisation
theorem ContinuousLinearMap.norm_inverse_one_sub_le.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E]
[NormedSpace 𝕜 E] [CompleteSpace E] (T : E →L[𝕜] E) {q : ℝ} (hT : ‖T‖ ≤ q) (hq : q < 1) :
‖Ring.inverse (1 - T)‖ ≤ 1 / (1 - q)Lean proof
/-- Quantitative inverse bound for a perturbation of norm at most `q < 1`. -/
theorem norm_inverse_one_sub_le (T : E →L[𝕜] E) {q : ℝ}
(hT : ‖T‖ ≤ q) (hq : q < 1) : ‖Ring.inverse (1-T)‖ ≤ 1/(1-q) := by
have hu : IsUnit (1-T) := isUnit_one_sub_of_norm_lt_one (hT.trans_lt hq)
have hd : 0 < 1-q := sub_pos.mpr hq
apply opNorm_le_bound _ (by positivity)
intro f
let u := Ring.inverse (1-T) f
have he : u-T u = f := by
have h := congrArg (fun A : E →L[𝕜] E ↦ A f) (Ring.mul_inverse_cancel _ hu)
simpa only [mul_apply_eq_comp, sub_apply, one_apply_eq_self] using h
have hn : ‖T u‖ ≤ q*‖u‖ :=
(T.le_opNorm u).trans (mul_le_mul_of_nonneg_right hT (norm_nonneg _))
have hl : (1-q)*‖u‖ ≤ ‖f‖ := by
have hh := norm_sub_le (u-T u) (-T u)
rw [sub_neg_eq_add, sub_add_cancel, norm_neg, he] at hh
nlinarith
change ‖u‖ ≤ _
rw [one_div_mul_eq_div, le_div_iff₀ hd]
simpa only [mul_comm] using hlFor an invertible bounded operator \(B\) on a real or complex normed space, any right-hand side \(f\) and any candidate \(v\) satisfy
In a Banach space, if \(B=I-T\) and \(\| T\| \le q{\lt}1\), the multiplier \(\| B^{-1}\| \) can be replaced by \((1-q)^{-1}\). The residual here is the full-space residual, not merely its finite projection.
Lean Formalisation
theorem ContinuousLinearMap.norm_sub_inverse_apply_le_residual.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜]
[NormedAddCommGroup E] [NormedSpace 𝕜 E] (B : E →L[𝕜] E) (hB : IsUnit B) (f v : E) :
‖v - (Ring.inverse B) f‖ ≤ ‖Ring.inverse B‖ * ‖B v - f‖Lean proof
/-- An inverse-norm bound turns the full residual into an error certificate. -/
theorem norm_sub_inverse_apply_le_residual (B : E →L[𝕜] E) (hB : IsUnit B) (f v : E) :
‖v-Ring.inverse B f‖ ≤ ‖Ring.inverse B‖*‖B v-f‖ := by
have he : Ring.inverse B (B v) = v := by
have h := congrArg (fun A : E →L[𝕜] E ↦ A v) (Ring.inverse_mul_cancel B hB)
simpa only [mul_apply_eq_comp, one_apply_eq_self] using h
calc
_ = ‖Ring.inverse B (B v-f)‖ := by rw [map_sub, he]
_ ≤ _ := (Ring.inverse B).le_opNorm _Let \(\alpha {\gt}-1\), \(\lambda {\gt}-1/2\), \(\alpha +\lambda \ge -1/2\) and \(q=|c|\| A\| {\lt}1\). Write \(B_N=I-cP_N\widehat A\). For every \(N\), \(B_N\) is invertible with \(\| B_N^{-1}\| \le (1-q)^{-1}\). For every \(f\in \ell ^2\), there is a unique solution
and a unique solution of the corresponding actual \(N\times N\) matrix equation. The solutions \(u_N=B_N^{-1}P_Nf\) converge to \(u=(I-c\widehat A)^{-1}f\), with
at every resolution. This includes the noncompact critical line.
Lean Formalisation
theorem Real.isUnit_powerLaw_section_of_small_coupling {α lam c : ℝ} (hα : -1 < α) (hlam : -(1 / 2) < lam)
(hs : -(1 / 2) ≤ α + lam) (hc : |c| * ‖Real.boundedPowerLawL2Operator hα hlam hs‖ < 1) (N : ℕ) :
IsUnit (1 - lp.initialL2Projection N ∘SL (c • Real.boundedPowerLawCoefficientOperator hα hlam hs))Lean proof
/-- At small coupling every normalized section is invertible, including on the critical line. -/
theorem isUnit_powerLaw_section_of_small_coupling (N : ℕ) :
IsUnit (1-(lp.initialL2Projection (𝕜 := ℝ) N).comp (c • boundedPowerLawCoefficientOperator hα hlam hs)) := by
simpa only [liftedFiniteSection, comp_neg, ← sub_eq_add_neg] using
isUnit_liftedFiniteSection_of_norm_lt_one (lp.initialL2Projection (𝕜 := ℝ) N)
(c • boundedPowerLawCoefficientOperator hα hlam hs) (lp.norm_initialL2Projection_le (𝕜 := ℝ) N)
(by rwa [norm_smul_powerLawCoefficientOperator])Throughout \(\alpha {\gt}-1\), \(\lambda {\gt}-1/2\), \(\alpha +\lambda \ge -1/2\), if \(I-cA\) is invertible, then every physical candidate \(v\) satisfies
The same statement holds in normalized coefficient coordinates with \(\widehat A\). If \(q=|c|\| A\| {\lt}1\), the inverse-norm factor in either version can be replaced by \((1-q)^{-1}\). The residual is the full residual, including unresolved coordinates.
Lean Formalisation
theorem Real.norm_powerLawL2_error_le_residualOn {α lam c : ℝ} (hα : -1 < α) (hlam : -(1 / 2) < lam) (hs : -(1 / 2) ≤ α + lam)
(hT : IsUnit (1 - c • Real.boundedPowerLawL2Operator hα hlam hs))
(f v : ↥(MeasureTheory.Lp ℝ 2 (Polynomial.gegenbauerMeasure lam))) :
‖v - ↑hT.unit⁻¹ f‖ ≤ ‖↑hT.unit⁻¹‖ * ‖v - c • (Real.boundedPowerLawL2Operator hα hlam hs) v - f‖Lean proof
theorem norm_powerLawL2_error_le_residualOn (hT : IsUnit (1-c • boundedPowerLawL2Operator hα hlam hs)) (f v : Lp ℝ 2 (gegenbauerMeasure lam)) : ‖v-(↑((hT).unit⁻¹) : Lp ℝ 2 (gegenbauerMeasure lam) →L[ℝ] Lp ℝ 2 (gegenbauerMeasure lam)) f‖ ≤ ‖(↑((hT).unit⁻¹) : Lp ℝ 2 (gegenbauerMeasure lam) →L[ℝ] Lp ℝ 2 (gegenbauerMeasure lam))‖ * ‖v-c • boundedPowerLawL2Operator hα hlam hs v-f‖:= by
simpa only [inverse_eq_certified (hT)] using norm_powerLawL2_error_le_residual hα hlam hs hT f vUnresolved residual coordinates are included; these theorems do not assert a computable numerical bound without a certified bound for the full residual and the inverse norm.
Reference details: Gegenbauer lowering and weighted derivative and related results
For \(\lambda {\gt}-1/2\), the cleared lowering identity is \((1-x^2)(C_{n+1}^{(\lambda )})'+(n+1)xC_{n+1}^{(\lambda )} =(n+2\lambda )C_n^{(\lambda )}\). On \((-1,1)\),
The latter interior derivative identity itself needs no parameter restriction. Reference: [DLMF, 18.9.19–18.9.20].
Lean Formalisation
theorem Polynomial.gegenbauer_euler_derivative {lam : ℝ} (hlam : -(1 / 2) < lam) (n : ℕ) :
Polynomial.X * Polynomial.derivative (Polynomial.gegenbauer lam (n + 1)) -
Polynomial.C (↑n + 1) * Polynomial.gegenbauer lam (n + 1) =
Polynomial.derivative (Polynomial.gegenbauer lam n)Lean proof
/-- A derivative identity lowering the degree by one. -/
theorem gegenbauer_euler_derivative {lam : ℝ} (hlam : -(1/2) < lam) (n : ℕ) :
X*derivative (gegenbauer lam (n+1)) - C (n+1 : ℝ)*gegenbauer lam (n+1) =
derivative (gegenbauer lam n) := by
cases n with
| zero => simp [gegenbauer_one]; ring
| succ n =>
have hn : (n : ℝ)+lam+2 ≠ 0 := by have := Nat.cast_nonneg (α := ℝ) n; linarith
apply mul_left_cancel₀ (C_ne_zero.mpr hn)
have hr := gegenbauer_recurrence (lam+1) n
have hc := gegenbauer_conversion lam n
rw [derivative_gegenbauer_succ, derivative_gegenbauer_succ]
simp only [Nat.cast_add, Nat.cast_one, map_add, map_mul, map_ofNat, map_natCast,
map_one] at hr hc ⊢
simp only [Nat.add_assoc, Nat.reduceAdd]
linear_combination -C lam*hr-(n+2 : ℝ[X])*hcFor \(\alpha {\gt}-1\), \(\lambda {\gt}-1/2\), \(x\in (-1,1)\) and \(P\in \mathbb {R}[X]\), let \(f_P(y)=w_\lambda (y)P(y)\) on \((-1,x)\). Define the linear functional
Lean Formalisation
def Real.PowerLawLeftInput.gegenbauerPolynomial (α : ↑(Set.Ioi (-1))) (lam : ↑(Set.Ioi (-(1 / 2)))) (x : ↑(Set.Ioo (-1) 1))
(p : Polynomial ℝ) : (↑α).PowerLawLeftInput ⟨↑x, ⋯⟩Lean definition
/-- Polynomial inputs for the classical left kernel. -/
def PowerLawLeftInput.gegenbauerPolynomial (α : Ioi (-1 : ℝ))
(lam : Ioi (-(1/2) : ℝ)) (x : Ioo (-1 : ℝ) 1) (p : ℝ[X]) :
PowerLawLeftInput α.val ⟨x.val,x.property.1.le⟩ :=
PowerLawInput.left ⟨x.val,Ioo_subset_Icc_self x.property⟩
(.gegenbauerContinuous α lam x ⟨fun y ↦ p.eval y.val,p.continuous.comp continuous_subtype_val⟩)Let \(\alpha {\gt}-1\), \(\lambda {\gt}-1/2\), \(x\in (-1,1)\) and \(P\in \mathbb {R}[X]\). The weighted polynomial restricted to \((-1,x)\) has values \(f_P(y)=w_\lambda (y)P(y)\), and
Lean Formalisation
theorem Real.PowerLawLeftInput.gegenbauerPolynomial_apply (α : ↑(Set.Ioi (-1))) (lam : ↑(Set.Ioi (-(1 / 2))))
(x : ↑(Set.Ioo (-1) 1)) (p : Polynomial ℝ) (y : ↑(Set.Ioo (-1) ↑x)) :
↑(Real.PowerLawLeftInput.gegenbauerPolynomial α lam x p) y =
↑((Polynomial.gegenbauerWeight ↑lam) ⟨↑y, ⋯⟩) * Polynomial.eval (↑y) pLean proof
theorem PowerLawLeftInput.gegenbauerPolynomial_apply (α : Ioi (-1 : ℝ))
(lam : Ioi (-(1/2) : ℝ)) (x : Ioo (-1 : ℝ) 1) (p : ℝ[X])
(y : Ioo (-1 : ℝ) x.val) :
(PowerLawLeftInput.gegenbauerPolynomial α lam x p).val y =
(Polynomial.gegenbauerWeight lam.val ⟨y.val,y.property.1,y.property.2.trans x.property.2⟩ : ℝ)*
p.eval y.val := rflLet \(U_n(x)=Q_\alpha (w_\lambda C_n^{(\lambda )})(x)\), with \(\alpha {\gt}-1\), \(\lambda {\gt}-1/2\) and \(|x|{\lt}1\). For \(n\ge 1\),
The same cleared recurrence holds separately for the left and right integrals. It includes \(\lambda =0\) and does not divide by a polynomial norm. Reference: [GCO22, Lemma 2.2 and Theorem 2.4].
Lean Formalisation
theorem Real.powerLawLeftPolynomial_gegenbauer_recurrenceOn (α : ↑(Set.Ioi (-1))) (lam : ↑(Set.Ioi (-(1 / 2))))
(x : ↑(Set.Ioo (-1) 1)) (m : ℕ) :
have U := fun n => (Real.powerLawLeftPolynomial α lam x) (Polynomial.gegenbauer (↑lam) n);
2 * (↑m + ↑lam + 1) * (↑m + 1) * (↑m + 1 + 2 * ↑lam) * ↑x * U (m + 1) =
(↑m + 1) * (↑m + 2) * (↑m + 2 * ↑lam + ↑α + 2) * U (m + 2) + (↑m + 1 + 2 * ↑lam) * (↑m - ↑α) * (↑m + 2 * ↑lam) * U mLean proof
theorem powerLawLeftPolynomial_gegenbauer_recurrenceOn
(α : Ioi (-1 : ℝ)) (lam : Ioi (-(1/2) : ℝ)) (x : Ioo (-1 : ℝ) 1) (m : ℕ) :
let U := fun n ↦ powerLawLeftPolynomial α lam x (gegenbauer lam.val n)
2*((m : ℝ)+lam.val+1)*((m : ℝ)+1)*((m : ℝ)+1+2*lam.val)*x.val*U (m+1) =
((m : ℝ)+1)*((m : ℝ)+2)*((m : ℝ)+2*lam.val+α.val+2)*U (m+2)+
((m : ℝ)+1+2*lam.val)*((m : ℝ)-α.val)*((m : ℝ)+2*lam.val)*U m := by
dsimp only
let L := powerLawLeftPolynomial α lam x
have hr := congrArg L (gegenbauer_recurrence lam.val m)
have hl := congrArg L (gegenbauer_lowering lam.property m)
have hL (c : ℝ) (p : ℝ[X]) : L (C c*p) = c*L p := by
rw [← smul_eq_C_mul,map_smul,smul_eq_mul]
rw [mul_assoc] at hr hl
simp only [L.map_add,L.map_sub,L.map_zero,hL] at hr hl
have hi := powerLawLeftPolynomial_gegenbauer_integrationByParts α lam x (m+1)
rw [← powerLawLeftPolynomial_shift_weight] at hi
have he := powerLawLeftPolynomial_mul_X α lam x (gegenbauer lam.val (m+1))
change L (X*gegenbauer lam.val (m+1)) = x.val*L (gegenbauer lam.val (m+1)) - _ at he
change _ = -(α.val+1)*L ((1-X^2)*(gegenbauer lam.val (m+1)).derivative) at hi
change _*L (gegenbauer lam.val (m+1)) = _*L (gegenbauer lam.val (m+2)) + _*L (gegenbauer lam.val m)
push_cast at hi hl hr
linear_combination -2*((m : ℝ)+lam.val+1)*((m : ℝ)+1)*((m : ℝ)+1+2*lam.val)*he +
2*((m : ℝ)+lam.val+1)*hi - 2*((m : ℝ)+lam.val+1)*(α.val+1)*hl -
((m : ℝ)+1)*((m : ℝ)+2*lam.val+α.val+2)*hrA continuously differentiable convolution kernel consists of continuous real functions \(g\) and \(s\) on \(\mathbb {R}\), with \(g'(t)=s(t)\) at every \(t\in \mathbb {R}\).
Lean Formalisation
inductive Real.C1ConvolutionKernel : TypeLean definition
structure C1ConvolutionKernel where
value : C(ℝ,ℝ)
slope : C(ℝ,ℝ)
hasDeriv : ∀ x, HasDerivAt value (slope x) xFor a continuously differentiable convolution kernel \((g,s)\) as in Definition 6.2.106, \(g\) is differentiable at every \(t\in \mathbb {R}\) and \(g'(t)=s(t)\).
Lean Formalisation
theorem Real.C1ConvolutionKernel.hasDeriv (self : Real.C1ConvolutionKernel) (x : ℝ) : HasDerivAt (⇑self.value) (self.slope x) xFor \(g\in C(\mathbb {R};\mathbb {R})\), an integrable real function \(f\) on \((-1,1)\), and \(x\in \mathbb {R}\), consider the integrable function \(y\mapsto g(x-y)f(y)\). Define \(V_gf(x)=\int _{-1}^1 g(x-y)f(y)\, dy\) with this integrable product as integrand.
Lean Formalisation
def Real.convolutionInput (g : C(ℝ, ℝ)) (x : ℝ)
(f : MeasureTheory.IntegrableInput (MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume)) :
MeasureTheory.IntegrableInput (MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume)Lean definition
def convolutionInput (g : C(ℝ,ℝ)) (x : ℝ) (f : IntegrableInput μI) : IntegrableInput μI := by
refine ⟨fun y ↦ g (x-y.val)*f.val y, ?_⟩
obtain ⟨M,hM⟩ := (isCompact_Icc (a := x-1) (b := x+1)).exists_bound_of_continuousOn
g.continuous.continuousOn
apply f.property.bdd_mul
(g.continuous.comp (continuous_const.sub continuous_subtype_val)).aestronglyMeasurable
exact Eventually.of_forall (fun y ↦ hM (x-y.val) ⟨by linarith [y.property.2],by linarith [y.property.1]⟩)For \(g\in C(\mathbb {R};\mathbb {R})\), \(f\in L^1((-1,1);\mathbb {R})\) with a pointwise representative, and \(x\in \mathbb {R}\), the convolution integrand is \(g(x-y)f(y)\) and
If \((g,s)\) is a continuously differentiable convolution kernel, then \((V_gf)'(x)=V_sf(x)\) for \(-1{\lt}x{\lt}1\). Integrable endpoint singularities of \(f\) are allowed.
Lean Formalisation
theorem Real.convolutionInput_apply (g : C(ℝ, ℝ)) (x : ℝ)
(f : MeasureTheory.IntegrableInput (MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume))
(y : ↑(Set.Ioo (-1) 1)) : ↑(Real.convolutionInput g x f) y = g (x - ↑y) * ↑f yLean proof
theorem convolutionInput_apply (g : C(ℝ,ℝ)) (x : ℝ) (f : IntegrableInput μI)
(y : Ioo (-1 : ℝ) 1) : (convolutionInput g x f).val y = g (x-y.val)*f.val y := rflFor \(\beta \ge 0\), let \(k_\beta (t)=|t|^\beta \) on \(\mathbb {R}\), a continuous real function, with \(0^0=1\).
Lean Formalisation
def Real.absPowerKernel (β : NNReal) : C(ℝ, ℝ)Lean definition
def absPowerKernel (β : ℝ≥0) : C(ℝ,ℝ) :=
⟨fun t ↦ |t|^(β : ℝ), continuous_abs.rpow_const (fun _ ↦ Or.inr β.property)⟩For \(\beta \ge 0\), \(k_\beta (t)=|t|^\beta \) on \(\mathbb {R}\), with \(0^0=1\). For \(\beta {\gt}1\) its derivative exists at every real \(t\) and is \(\beta |t|^{\beta -1}\operatorname {sign}(t)\), including value zero at \(t=0\).
Lean Formalisation
theorem Real.absPowerKernel_apply (β : NNReal) (t : ℝ) : (Real.absPowerKernel β) t = |t| ^ ↑βLean proof
theorem absPowerKernel_apply (β : ℝ≥0) (t : ℝ) : absPowerKernel β t = |t|^(β : ℝ) := rflFor \(\beta {\gt}1\), equip \(k_\beta \) with its continuous slope \(s_\beta (t)=\beta |t|^{\beta -1}\operatorname {sign}(t)\).
Lean Formalisation
def Real.C1ConvolutionKernel.power (β : ↑(Set.Ioi 1)) : Real.C1ConvolutionKernelLean definition
def C1ConvolutionKernel.power (β : Ioi (1 : ℝ)) : C1ConvolutionKernel where
value := absPowerKernel ⟨β.val,by have hb : 1 < β.val := β.property; linarith⟩
slope := ⟨fun t ↦ β.val*|t|^(β.val-1)*sign t, by
have hb : 1 < β.val := β.property
have hg : ContDiff ℝ 1 (fun t : ℝ ↦ |t|^β.val) := by
simpa only [Real.norm_eq_abs] using (contDiff_norm_rpow (E := ℝ) hb)
have he : deriv (fun t : ℝ ↦ |t|^β.val) = fun t ↦ β.val*|t|^(β.val-1)*sign t :=
funext (fun t ↦ (hasDerivAt_absPowerKernel β t).deriv)
rw [← he]
exact hg.continuous_deriv_one⟩
hasDeriv := hasDerivAt_absPowerKernel βFor \(\beta {\gt}1\), the continuously differentiable power kernel has value \(k_\beta (t)=|t|^\beta \) and slope \(s_\beta (t)=\beta |t|^{\beta -1}\operatorname {sign}(t)\) for every \(t\in \mathbb {R}\).
Lean Formalisation
theorem Real.C1ConvolutionKernel.power_value (β : ↑(Set.Ioi 1)) (t : ℝ) : (Real.C1ConvolutionKernel.power β).value t = |t| ^ ↑βLean proof
theorem C1ConvolutionKernel.power_value (β : Ioi (1 : ℝ)) (t : ℝ) :
(C1ConvolutionKernel.power β).value t = |t|^β.val := rflFor \(\beta \ge 0\), \(x\in \mathbb {R}\), and an integrable real function \(f\) on \((-1,1)\), regard \(f|_{D_x}\) as an element of the domain of \(u\mapsto Q_\beta u(x)\): its product with \(|x-y|^\beta \) is integrable on \(D_x\).
Lean Formalisation
def Real.PowerLawInput.ofL1 (β : NNReal) (x : ℝ)
(f : MeasureTheory.IntegrableInput (MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume)) :
(↑β).PowerLawInput xLean definition
def PowerLawInput.ofL1 (β : ℝ≥0) (x : ℝ) (f : IntegrableInput μI) : PowerLawInput β x := by
refine ⟨fun y ↦ f.val ⟨y.val,y.property.1⟩, ?_⟩
have h := (integrable_integral_powerLawDomain x (convolutionInput (absPowerKernel β) x f)).1
convert h using 1
all_goals rflFor \(\beta \ge 0\), \(x\in \mathbb {R}\) and integrable \(f\) on \((-1,1)\), the restriction \(f|_{D_x}\) retains the values \(f(y)\) at every \(y\in D_x\), and
Lean Formalisation
theorem Real.PowerLawInput.ofL1_apply (β : NNReal) (x : ℝ)
(f : MeasureTheory.IntegrableInput (MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume))
(y : x.PowerLawDomain) : ↑(Real.PowerLawInput.ofL1 β x f) y = ↑f ⟨↑y, ⋯⟩Lean proof
theorem PowerLawInput.ofL1_apply (β : ℝ≥0) (x : ℝ) (f : IntegrableInput μI)
(y : PowerLawDomain x) : (PowerLawInput.ofL1 β x f).val y = f.val ⟨y.val,y.property.1⟩ := rflFor \(\beta {\gt}1\) and any integrable input \(f\) on \([-1,1]\),
The derivative exists. In the weighted Gegenbauer parameter range the shifted zeroth mode also has a derivative and this gives \(U_1=2\lambda (xU_0-(Q_{\alpha +2}w_\lambda )'/(\alpha +2))\).
Reference: [GCO22, Section 2].
Lean Formalisation
theorem Real.hasDerivAt_powerLawIntegralOn (β : ↑(Set.Ioi 1))
(f : MeasureTheory.IntegrableInput (MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume))
(x : ↑(Set.Ioo (-1) 1)) :
HasDerivAt (fun t => Real.powerLawIntegral (Real.PowerLawInput.ofL1 ⟨↑β, ⋯⟩ t f))
(Real.intervalConvolution (Real.C1ConvolutionKernel.power β).slope f ↑x) ↑xLean proof
theorem hasDerivAt_powerLawIntegralOn (β : Ioi (1 : ℝ)) (f : IntegrableInput μI)
(x : Ioo (-1 : ℝ) 1) :
HasDerivAt (fun t ↦ powerLawIntegral (.ofL1
⟨β.val,by have hb : 1 < β.val := β.property; linarith⟩ t f))
(intervalConvolution (C1ConvolutionKernel.power β).slope f x.val) x.val := by
have he : (fun t ↦ powerLawIntegral (.ofL1
⟨β.val,by have hb : 1 < β.val := β.property; linarith⟩ t f)) =
intervalConvolution (C1ConvolutionKernel.power β).value f :=
funext (fun t ↦ powerLawIntegral_ofL1_eq_convolution _ t f)
rw [he]
exact hasDerivAt_intervalConvolution (C1ConvolutionKernel.power β) f xThe proof uses dominated differentiation for a smooth convolution kernel; it allows integrable endpoint-singular weights.
Reference details: Classical initial power-law polynomial and related results
Initial data \((\alpha ,\lambda )\) require all three arguments \((\alpha +1)/2\), \(\lambda +1/2\), and \(\lambda +\alpha /2+1\) to avoid the nonpositive integers. For every \(k\in \mathbb {N}\), define
Here \(H_k\) is the terminating polynomial of Definition 6.2.23. No compatibility or positivity is required for this polynomial definition.
Lean Formalisation
inductive Real.PowerLawInitialData : TypeLean definition
/-- The exact non-pole domain of the three Gamma factors in the initial mode. -/
structure PowerLawInitialData where
alpha : ℝ
lam : ℝ
alphaRegular : ∀ n : ℕ, (alpha+1)/2 ≠ -(n : ℝ)
lamRegular : ∀ n : ℕ, lam+1/2 ≠ -(n : ℝ)
sumRegular : ∀ n : ℕ, lam+alpha/2+1 ≠ -(n : ℝ)The initial polynomial has degree at most \(2k\) throughout this non-pole domain. Shifting \(\alpha \) to \(\alpha +2\) preserves admissibility. Every \(\alpha {\gt}-1\), \(\lambda {\gt}-1/2\) gives admissible initial data.
Lean Formalisation
theorem Real.natDegree_powerLawGegenbauerInitialPolynomial_le (p : Real.PowerLawInitialData) (k : ℕ) :
(Real.powerLawGegenbauerInitialPolynomial p k).natDegree ≤ 2 * kLean proof
/-- Initial degree does not require positivity or power-law compatibility. -/
theorem natDegree_powerLawGegenbauerInitialPolynomial_le (p : PowerLawInitialData) (k : ℕ) :
(powerLawGegenbauerInitialPolynomial p k).natDegree ≤ 2*k := by
apply (natDegree_C_mul_le _ _).trans
rw [natDegree_comp, natDegree_X_pow]
have h := natDegree_ordinaryHypergeometricPolynomial_le k (.ofNoPole (-p.alpha/2) (1/2 : ℝ) k
(by intro n hn; have h := Nat.cast_nonneg (α := ℝ) n; linarith))
omegaFor a mode \(n\), take initial data and require \(\alpha +2\ne 0\) if \(n\ge 1\), and \(m+2\lambda +\alpha +2\ne 0\) for every \(m+2\le n\). Define the finite recurrence by the preceding \(q_0\),
and, through the requested mode,
Whole-family data require these nonzero-denominator conditions at every step. A finite mode requires no conditions on later unused steps.
Lean Formalisation
inductive Real.PowerLawRecurrenceData (n : ℕ) : TypeLean definition
/-- Finite-prefix recurrence data require exactly the denominators actually used. -/
structure PowerLawRecurrenceData (n : ℕ) extends PowerLawInitialData where
firstDenominator : 1 ≤ n → alpha+2 ≠ 0
leadingDenominator : ∀ m : ℕ, m+2 ≤ n → (m : ℝ)+2*lam+alpha+2 ≠ 0Admissibility restricts to every earlier mode, and whole-family data give every finite prefix. Each used denominator is nonzero and \(\deg q_n\le n+2k\). The natural range \(\alpha {\gt}-1\), \(\lambda {\gt}-1/2\) gives whole-family data; there \((m+1)(m+2)(m+2\lambda +\alpha +2){\gt}0\) for every \(m\ge 0\).
Lean Formalisation
theorem Real.PowerLawRecurrenceData.denominator_ne_zero {n : ℕ} (p : Real.PowerLawRecurrenceData n) (m : ℕ) (hm : m + 2 ≤ n) :
(↑m + 1) * (↑m + 2) * (↑m + 2 * p.lam + p.alpha + 2) ≠ 0Lean proof
/-- The full recurrence denominator is nonzero whenever this step is in the prefix. -/
theorem PowerLawRecurrenceData.denominator_ne_zero {n : ℕ} (p : PowerLawRecurrenceData n)
(m : ℕ) (hm : m+2 ≤ n) :
((m : ℝ)+1)*((m : ℝ)+2)*((m : ℝ)+2*p.lam+p.alpha+2) ≠ 0 := by
have hn := Nat.cast_nonneg (α := ℝ) m
exact mul_ne_zero (mul_ne_zero (by linarith) (by linarith)) (p.leadingDenominator m hm)Suppose \(\alpha {\gt}-1\), \(\lambda {\gt}-1/2\) and \(k=\lambda +\alpha /2\in \mathbb N\). Each \(U_n\) equals an explicitly defined polynomial \(q_n\) on \((-1,1)\), with \(\deg q_n\le n+2k\). The zeroth polynomial is the terminating Gauss expression, the first uses the derivative of the exponent-shifted zeroth polynomial, and all later polynomials use the fixed-exponent recurrence. Its leading recurrence denominator is strictly positive in this parameter range. Reference: [GCO22, Lemma 2.7 and Theorem 2.4].
Lean Formalisation
theorem Real.eval_powerLawGegenbauerInitialPolynomial (α : ↑(Set.Ioi (-1))) (lam : ↑(Set.Ioi (-(1 / 2)))) {k : ℕ}
(hk : ↑lam + ↑α / 2 = ↑k) (x : ↑(Set.Ioo (-1) 1)) :
Polynomial.eval (↑x) (Real.powerLawGegenbauerInitialPolynomial (Real.PowerLawInitialData.ofIntegrable α lam) k) =
Real.powerLawIntegral (Real.PowerLawInput.gegenbauerWeight α lam x)Lean proof
/-- Classical integral evaluation of the initial terminating polynomial. -/
theorem eval_powerLawGegenbauerInitialPolynomial (α : Ioi (-1 : ℝ))
(lam : Ioi (-(1/2) : ℝ)) {k : ℕ} (hk : lam.val+α.val/2 = k)
(x : Ioo (-1 : ℝ) 1) :
(powerLawGegenbauerInitialPolynomial (.ofIntegrable α lam) k).eval x.val =
powerLawIntegral (.gegenbauerWeight α lam x) := by
rw [powerLawIntegral_gegenbauerWeight_hypergeometricSqOn]
let p : TerminatingGaussParameters ℝ k :=
.ofNoPole (-α.val/2) (1/2 : ℝ) k
(by intro n hn; have h := Nat.cast_nonneg (α := ℝ) n; linarith)
have he := ordinaryHypergeometric_eq_eval_polynomial k p (x.val^2)
let q : GaussParameters ℝ := GaussParameters.ofNoPole (-α.val/2) (-lam.val-α.val/2) (1/2 : ℝ)
(GammaPoint.ofPos _ (by norm_num)).property
let z : Metric.ball (0 : ℝ) 1 := ⟨x.val^2, by
rw [Metric.mem_ball, dist_zero_right, Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)]
nlinarith [x.property.1,x.property.2]⟩
have hc : ordinaryHypergeometricOn q (.ofUnitDisk q z) =
ordinaryHypergeometricOn p.val (.ofTerminating p.val k (Or.inr p.property) (x.val^2)) := by
apply gauss_value_congr
· rfl
· change -lam.val-α.val/2 = -(k : ℝ)
linarith
· rfl
· rfl
rw [hc, he]
simp only [powerLawGegenbauerInitialPolynomial, PowerLawInitialData.ofIntegrable,
GammaOn, GammaPoint.ofPos, eval_mul, eval_C, eval_comp, eval_pow, eval_X, p]Reference details: Classical polynomial power-law functional and related results
For \(\alpha {\gt}-1\), \(\lambda {\gt}-1/2\) and \(x\in (-1,1)\), define the linear functional on real polynomials by \(P\mapsto Q_\alpha (w_\lambda P)(x)\), where \(w_\lambda P\) is restricted to \(D_x=(-1,1)\setminus \{ x\} \).
Lean Formalisation
def Real.PowerLawInput.gegenbauerPolynomial (α : ↑(Set.Ioi (-1))) (lam : ↑(Set.Ioi (-(1 / 2)))) (x : ↑(Set.Ioo (-1) 1))
(p : Polynomial ℝ) : (↑α).PowerLawInput ↑xLean definition
/-- Polynomial inputs use the already constructed integrable weighted domain. -/
def PowerLawInput.gegenbauerPolynomial (α : Ioi (-1 : ℝ)) (lam : Ioi (-(1/2) : ℝ))
(x : Ioo (-1 : ℝ) 1) (p : ℝ[X]) : PowerLawInput α.val x.val :=
.gegenbauerContinuous α lam x ⟨fun y ↦ p.eval y.val, p.continuous.comp continuous_subtype_val⟩For \(\alpha {\gt}-1\), \(\lambda {\gt}-1/2\), \(x\in (-1,1)\) and \(P\in \mathbb {R}[X]\), the weighted polynomial on \(D_x=(-1,1)\setminus \{ x\} \) has values \(w_\lambda (y)P(y)\). The polynomial functional of Definition 6.2.122 therefore satisfies
Lean Formalisation
theorem Real.PowerLawInput.gegenbauerPolynomial_apply (α : ↑(Set.Ioi (-1))) (lam : ↑(Set.Ioi (-(1 / 2))))
(x : ↑(Set.Ioo (-1) 1)) (p : Polynomial ℝ) (y : (↑x).PowerLawDomain) :
↑(Real.PowerLawInput.gegenbauerPolynomial α lam x p) y =
↑((Polynomial.gegenbauerWeight ↑lam) ⟨↑y, ⋯⟩) * Polynomial.eval (↑y) pLean proof
/-- Pointwise characterization of polynomial weighted inputs. -/
theorem PowerLawInput.gegenbauerPolynomial_apply (α : Ioi (-1 : ℝ))
(lam : Ioi (-(1/2) : ℝ)) (x : Ioo (-1 : ℝ) 1) (p : ℝ[X]) (y : PowerLawDomain x.val) :
(PowerLawInput.gegenbauerPolynomial α lam x p).val y =
(Polynomial.gegenbauerWeight lam.val ⟨y.val,y.property.1⟩ : ℝ)*p.eval y.val := rflFor whole-family data with \(\lambda {\gt}-1/2\) and \(\lambda \ne 0\), define the polynomial linear operator \(C_n^{(\lambda )}\mapsto q_n\). An individual coefficient column is the Gegenbauer-basis representation of \(q_n\) and requires only admissible data through degree \(n\), together with the same nondegenerate basis conditions. It does not require later recurrence steps.
Lean Formalisation
def Real.PowerLawOperatorData : TypeLean definition
/-- Whole-family data with a genuine Gegenbauer polynomial basis. -/
abbrev PowerLawOperatorData := {p : PowerLawFamilyData // -(1/2) < p.lam ∧ p.lam ≠ 0}The parameter range \(\alpha {\gt}-1\), \(\lambda {\gt}-1/2\), \(\lambda \ne 0\) satisfies the whole-family admissibility conditions of Definition 6.2.124. On that definition’s full domain, restriction to degree \(n\) satisfies the finite-column conditions. For each \(k\in \mathbb {N}\), the polynomial operator sends \(C_n^{(\lambda )}\) to the recurrence polynomial \(q_n\), and the finite-column coefficients are exactly its Gegenbauer coordinate coefficients. For every admissible finite column, the coefficient at degree \(j{\gt}n+2k\) is zero.
Lean Formalisation
theorem Real.powerLawGegenbauerOperator_gegenbauer (p : Real.PowerLawOperatorData) (k n : ℕ) :
(Real.powerLawGegenbauerOperator p k) (Polynomial.gegenbauer (↑p).lam n) =
Real.powerLawGegenbauerPolynomial k n ((↑p).atDegree n)Lean proof
@[simp] theorem powerLawGegenbauerOperator_gegenbauer (p : PowerLawOperatorData) (k n : ℕ) :
powerLawGegenbauerOperator p k (gegenbauer p.val.lam n) =
powerLawGegenbauerPolynomial k n (p.val.atDegree n) := by
rw [← gegenbauerBasis_apply p.property.1 p.property.2 n]
exact Module.Basis.constr_basis _ _ _ _Under compatibility as above and \(\lambda \ne 0\), the polynomial operator \(C_n^{(\lambda )}\mapsto q_n\) agrees with the actual weighted integral on every polynomial input. Its coefficient matrix in the original Gegenbauer basis has lower and upper bandwidth \(2k\): \(A_{j,n}=0\) if \(j{\gt}n+2k\) or \(n{\gt}j+2k\). The operator is symmetric for the Gegenbauer inner product; in this unnormalized basis this means weighted symmetry, not ordinary matrix symmetry. Reference: [GCO22, Section 2].
Lean Formalisation
theorem Real.eval_powerLawGegenbauerOperator (α : ↑(Set.Ioi (-1))) (lam : ↑(Set.Ioi (-(1 / 2)))) (hzero : ↑lam ≠ 0) {k : ℕ}
(hk : ↑lam + ↑α / 2 = ↑k) (x : ↑(Set.Ioo (-1) 1)) (p : Polynomial ℝ) :
Polynomial.eval (↑x) ((Real.powerLawGegenbauerOperator (Real.PowerLawOperatorData.ofIntegrable α lam hzero) k) p) =
(Real.powerLawPolynomial α lam x) pLean proof
/-- Evaluation of the assembled operator equals the classical integral functional. -/
theorem eval_powerLawGegenbauerOperator (α : Ioi (-1 : ℝ))
(lam : Ioi (-(1/2) : ℝ)) (hzero : lam.val ≠ 0) {k : ℕ}
(hk : lam.val+α.val/2 = k) (x : Ioo (-1 : ℝ) 1) (p : ℝ[X]) :
(powerLawGegenbauerOperator (.ofIntegrable α lam hzero) k p).eval x.val =
powerLawPolynomial α lam x p := by
have h : (aeval x.val : ℝ[X] →ₐ[ℝ] ℝ).toLinearMap.comp
(powerLawGegenbauerOperator (.ofIntegrable α lam hzero) k) =
powerLawPolynomial α lam x := by
apply (gegenbauerBasis lam.property hzero).ext
intro n
erw [gegenbauerBasis_apply]
change (powerLawGegenbauerOperator (.ofIntegrable α lam hzero) k
(gegenbauer lam.val n)).eval x.val =
powerLawPolynomial α lam x (gegenbauer lam.val n)
erw [powerLawGegenbauerOperator_gegenbauer]
change (powerLawGegenbauerPolynomial k n (.ofIntegrable α lam n)).eval x.val =
powerLawIntegral (.gegenbauerMode α lam x n)
exact eval_powerLawGegenbauerPolynomial α lam hk x n
exact congrArg (fun L : ℝ[X] →ₗ[ℝ] ℝ ↦ L p) h