Radial
Abstract
Mixed norms and power-family point evaluations.
Definition 1.1 (The radial norm integral).
Lean statement: D5/S3/Analytic/MixedNorm/DmitrovicPointEvaluation/Radial.radialIntegral
Formalization. D5/S3/Analytic/MixedNorm/DmitrovicPointEvaluation/Radial.radialIntegral (✓ std3).
Source. Repository-derived.
Commentary.
For finite positive p and q, this real interval integral is the q-th power of the power-family mixed norm. Its parameter t is the square of the affine parameter a. The weight may have an integrable singularity at radius one.
Definition 1.2 (The normalized evaluation power).
Lean statement: D5/S3/Analytic/MixedNorm/DmitrovicPointEvaluation/Radial.evaluationExcess
Formalization. D5/S3/Analytic/MixedNorm/DmitrovicPointEvaluation/Radial.evaluationExcess (✓ std3).
Source. Repository-derived.
Commentary.
Put c=1/(1+alpha p). The expression (1+ct) raised to 2q/p times (1-c squared t) raised to alpha q+q/p is the q-th power of the normalized evaluation at ca, where t=a squared.