High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Corrector.PushforwardBallGrowth

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

The Liouville growth row under a translation by an arbitrary real vector

The growth conjunct of MemLiouvilleClass is a volume-normalized L² average over centred Euclidean balls, rescaled by r ^ (-(1 + ϑ)). This module transports it along a translation v ↦ v (· + t) by an arbitrary real vector and an additive recentring v ↦ v - c.

The geometry is one line: B_r + t ⊆ B_{2 r} as soon as ‖t‖ ≤ r. The work is the ℝ≥0∞ bookkeeping — the division by volume V in eVolumeAverage cancels only after volume V is shown to be neither 0 nor ∞, which for a positive-radius Euclidean ball is exactly isOpen_euclideanBall and Book.Ch01.volume_euclideanBall_ne_top.

The additive constant is the one place a sign condition on ϑ enters: the recentred function only satisfies the same growth row when r ^ (-(1 + ϑ)) itself tends to zero, i.e. when 1 + ϑ > 0. See the sign condition discussed in PushforwardRealTranslateLiouville.

Centred and off-centre Euclidean balls

theorem HCPolySupport.HighContrast.Root.translateSet_euclideanBall {d : ℕ} (t : Vec d) (r : ℝ) : translateSet t (euclideanBall d r) = euclideanBallAt t r

Translating the centred ball by t gives the ball centred at t.

theorem HCPolySupport.HighContrast.Root.volume_euclideanBallAt_eq {d : ℕ} (t : Vec d) (r : ℝ) : MeasureTheory.volume (euclideanBallAt t r) = MeasureTheory.volume (euclideanBall d r)

Lebesgue volume does not see the centre of a Euclidean ball.

theorem HCPolySupport.HighContrast.Root.volume_euclideanBall_ne_zero {d : ℕ} {r : ℝ} (hr : 0 < r) : MeasureTheory.volume (euclideanBall d r) ≠ 0

A positive-radius centred ball has nonzero volume.

theorem HCPolySupport.HighContrast.Root.volume_euclideanBall_ne_top {d : ℕ} (r : ℝ) : MeasureTheory.volume (euclideanBall d r) ≠ ⊤

A centred ball has finite volume.

theorem HCPolySupport.HighContrast.Root.volume_smul_set {d : ℕ} {r : ℝ} (hr : 0 ≤ r) (U : Set (Vec d)) : MeasureTheory.volume (r • U) = ENNReal.ofReal (r ^ d) * MeasureTheory.volume U

Positive dilation scales Lebesgue volume by the dimension power.

theorem HCPolySupport.HighContrast.Root.euclideanBall_eq_smul_unit {d : ℕ} {r : ℝ} (hr : 0 < r) : euclideanBall d r = r • euclideanBall d 1

The centred ball of radius r is the r-dilate of the unit ball.

theorem HCPolySupport.HighContrast.Root.volume_euclideanBall_eq_ofReal_pow_mul {d : ℕ} {r : ℝ} (hr : 0 < r) : MeasureTheory.volume (euclideanBall d r) = ENNReal.ofReal (r ^ d) * MeasureTheory.volume (euclideanBall d 1)

Volume of a centred ball, factored through the unit ball.

theorem HCPolySupport.HighContrast.Root.volume_euclideanBall_two_mul {d : ℕ} {r : ℝ} (hr : 0 < r) : MeasureTheory.volume (euclideanBall d (2 * r)) = ENNReal.ofReal (2 ^ d) * MeasureTheory.volume (euclideanBall d r)

Doubling the radius multiplies the volume by 2 ^ d, exactly.

theorem HCPolySupport.HighContrast.Root.euclideanBallAt_subset_euclideanBall_two_mul {d : ℕ} (t : Vec d) {r : ℝ} (ht : √(vecNormSq t) ≤ r) : euclideanBallAt t r ⊆ euclideanBall d (2 * r)

The one geometric step. A ball of radius r centred at t lies inside the centred ball of radius 2 r as soon as the Euclidean length of t is at most r.

The normalized norm under a translation

theorem HCPolySupport.HighContrast.Root.normalizedL2Norm_translate {d : ℕ} (t : Vec d) (r : ℝ) (f : Vec d → ℝ) : (normalizedL2Norm (euclideanBall d r) fun (x : Vec d) => f (x + t)) = normalizedL2Norm (euclideanBallAt t r) f

The normalized L² norm of a translated function on the centred ball is the normalized norm of the function on the translated ball. Both the numerator and the volume in the denominator move with the translation.

theorem HCPolySupport.HighContrast.Root.normalizedL2Norm_sub_const_le {d : ℕ} {V : Set (Vec d)} (hVzero : MeasureTheory.volume V ≠ 0) (hVtop : MeasureTheory.volume V ≠ ⊤) (f : Vec d → ℝ) (c : ℝ) : (normalizedL2Norm V fun (x : Vec d) => f x - c) ≤ ENNReal.ofReal 2 ^ (1 / 2) * normalizedL2Norm V f + ENNReal.ofReal (2 * c ^ 2) ^ (1 / 2)

Recentring by a constant costs a factor √2 and an additive constant. The bound is stated with the exact ℝ≥0∞ constants it is proved with, so no positivity side condition on the function is needed.

The growth row transports

theorem HCPolySupport.HighContrast.Root.tendsto_growth_realTranslate {d : ℕ} {theta : ℝ} (v : Vec d → ℝ) (t : Vec d) (h : 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 (y + t)) Filter.atTop (nhds 0)

The growth row for the translated function alone: a fixed real translation costs exactly the constant (2 ^ d) ^ (1/2) * 2 ^ (1 + ϑ). No sign condition on ϑ is used here.

theorem HCPolySupport.HighContrast.Root.tendsto_growth_realTranslate_subConst {d : ℕ} {theta : ℝ} (htheta : 0 < theta) (v : Vec d → ℝ) (t : Vec d) (c : ℝ) (h : 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 (y + t) - c) Filter.atTop (nhds 0)

The growth row of MemLiouvilleClass, transported. A translation by an arbitrary real vector together with an arbitrary additive recentring preserves the o(r ^ (1 + ϑ)) normalized growth, provided 1 + ϑ > 0.

The hypothesis 0 < theta is used only for the additive constant, and it is necessary: at theta = -1 the row is scale-invariant and a nonzero constant violates it.