Upper semicontinuity of the exponential-sum growth exponent

This file proves the upper semicontinuity assertion in the blueprint. The main input is scale transference: dilation and finite Fourier inversion increase the scale, while decomposition into residue classes decreases it. Both operations preserve the fixed model order of the phase.

Scale transference

theorem Expdb.exponentSumGrowthExponent_monoOn_Icc : MonotoneOn exponentSumGrowthExponent (Set.Icc 0 1)

On the subcritical interval, the exponential-sum growth exponent is monotone.

theorem Expdb.exponentSumGrowthExponent_le_add_sub {α γ : NNReal} (hαγ : α ≤ γ) : exponentSumGrowthExponent γ ≤ exponentSumGrowthExponent α + ↑γ - ↑α

Increasing the scale by γ - α costs at most that amount in the growth exponent.

theorem Expdb.lipschitzOnWith_exponentSumGrowthExponent : LipschitzOnWith 1 exponentSumGrowthExponent (Set.Icc 0 1)

The growth exponent is 1-Lipschitz on the subcritical interval.

theorem Expdb.continuousOn_exponentSumGrowthExponent : ContinuousOn exponentSumGrowthExponent (Set.Icc 0 1)

The exponential-sum growth exponent is continuous on the subcritical interval.

theorem Expdb.upperSemicontinuous_exponentSumGrowthExponent : UpperSemicontinuous exponentSumGrowthExponent

The exponential-sum growth exponent is upper semicontinuous.