High-contrast homogenization: #
Provider.PolynomialHomogenization.Root.Corrector.AffineLiouvilleGrowth
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Continuous-radius Liouville growth under affine pullback #
The normalized scalar norm is compared on a source ball enlarged by the fixed matrix distortion. Homothetic ball volume scaling makes the comparison constant independent of the radius.
theorem
HCPolySupport.HighContrast.Root.matImage_smul_one_euclideanBall
{d : ℕ}
{q : ℝ}
(hq : 0 < q)
(R : ℝ)
:
theorem
HCPolySupport.HighContrast.Root.volume_euclideanBall_mul
{d : ℕ}
{q : ℝ}
(hq : 0 < q)
(R : ℝ)
:
MeasureTheory.volume (euclideanBall d (q * R)) = ENNReal.ofReal (q ^ d) * MeasureTheory.volume (euclideanBall d R)
theorem
HCPolySupport.HighContrast.Root.normalizedL2Norm_affinePullback_ball_le
{d : ℕ}
{L : Mat d}
(hL : IsUnit (Matrix.det L))
{R : ℝ}
(hR : 0 < R)
(v : Vec d → ℝ)
:
(normalizedL2Norm (euclideanBall d R) fun (y : Vec d) => v (matVecMul L y)) ≤ ENNReal.ofReal (|Matrix.det L|⁻¹ * affineBallFactor L ^ d) ^ (1 / 2) * normalizedL2Norm (euclideanBall d (affineBallFactor L * R)) v
The normalized pullback norm on a centered ball is bounded by a fixed determinant-and-distortion factor times the source norm on the enlarged ball.
theorem
HCPolySupport.HighContrast.Root.liouvilleGrowth_affinePullback
{d : ℕ}
{L : Mat d}
(hL : IsUnit (Matrix.det L))
{theta : ℝ}
{v : Vec d → ℝ}
(hgrowth :
Filter.Tendsto (fun (R : ℝ) => ENNReal.ofReal (R ^ (-(1 + theta))) * normalizedL2Norm (euclideanBall d R) v)
Filter.atTop (nhds 0))
:
Filter.Tendsto
(fun (R : ℝ) =>
ENNReal.ofReal (R ^ (-(1 + theta))) * normalizedL2Norm (euclideanBall d R) fun (y : Vec d) => v (matVecMul L y))
Filter.atTop (nhds 0)
Continuous-radius Liouville growth is preserved by a fixed invertible affine pullback.