HalfScaleExponentBridge #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Half-scale finite-exponent comparison #
This file compares the finite q = 1 multiscale ellipticity gauges at scale
parameter s with the finite q = 2 gauges at parameter s / 2.
The comparison combines CoarseGraining's Jensen bounds for q = 1 with the
exact weight identity geometricWeight (s / 2) 2 = geometricWeight s 1.
Main results #
LambdaSq_finite_one_le_half_two:Λ_{s,1} ≤ Λ_{s/2,2}.lambdaSq_finite_one_inv_le_half_two:λ_{s,1}^{-1} ≤ λ_{s/2,2}^{-1}.
theorem
Algsuperdiff.Section3.Provider.ErrorComparison.LambdaSq_finite_one_le_half_two
{d : ℕ}
[NeZero d]
(Q : HCPolySupport.TriadicCube d)
(a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d)
{s : ℝ}
(hs : 0 < s)
:
The finite q = 1 upper multiscale ellipticity at s is bounded by the
finite q = 2 upper multiscale ellipticity at s / 2.
theorem
Algsuperdiff.Section3.Provider.ErrorComparison.lambdaSq_finite_one_inv_le_half_two
{d : ℕ}
[NeZero d]
(Q : HCPolySupport.TriadicCube d)
(a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d)
{s : ℝ}
(hs : 0 < s)
:
The inverse finite q = 1 lower multiscale ellipticity at s is bounded
by the inverse finite q = 2 lower multiscale ellipticity at s / 2.