High-contrast homogenization: Provider.Regularity.CorrectorRealRadiusGrowth

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

Continuous-radius sublinear growth of anchored correctors

This module turns the discrete centered-cube O(3^q) estimate into the exact continuous-radius vanishing limit used by MemLiouvilleClass.

theorem HCPolySupport.HighContrast.natCast_le_outerTriadicGeneration_of_pow_le {R : ℝ} (hR : 0 < R) {q : ℕ} (hq : 3 ^ q ≤ R) : ↑q ≤ outerTriadicGeneration R hR

If a positive real side length dominates the qth triadic scale, its canonical enclosing generation is at least q.

theorem HCPolySupport.HighContrast.outerTriadicGeneration_nonneg_of_one_le {R : ℝ} (hR : 0 < R) (hRone : 1 ≤ R) : 0 ≤ outerTriadicGeneration R hR

In particular, a side length at least one has a nonnegative canonical generation.

theorem HCPolySupport.HighContrast.exists_eventually_normalizedBallL2_le_linear_cubeGrowth {d : ℕ} [NeZero d] (f : Vec d → ℝ) (q₀ : ℕ) (C : ℝ) (hC : 0 ≤ C) (hmem : ∀ (q : ℕ), MeasureTheory.MemLp f 2 (normalizedCubeMeasure (originCube d ↑q))) (hcube : ∀ (q : ℕ), q₀ ≤ q → cubeLpNorm (originCube d ↑q) 2 f ≤ C * 3 ^ q) : ∃ (D : ENNReal), D ≠ ⊤ ∧ ∀ᶠ (r : ℝ) in Filter.atTop, normalizedL2Norm (euclideanBall d r) f ≤ D * ENNReal.ofReal r

A discrete O(3^q) bound with local square-integrability becomes an eventual O(r) bound for the frozen normalized L² norm on Euclidean balls.

theorem HCPolySupport.HighContrast.NormalizedLocalH1Carrier.exists_eventually_normalizedBallL2_le_linear_cubeGrowth {d : ℕ} [NeZero d] (z : NormalizedLocalH1Carrier d) (q₀ : ℕ) (C : ℝ) (hC : 0 ≤ C) (hcube : ∀ (q : ℕ), q₀ ≤ q → cubeLpNorm (originCube d ↑q) 2 z.globalValueRepresentative ≤ C * 3 ^ q) : ∃ (D : ENNReal), D ≠ ⊤ ∧ ∀ᶠ (r : ℝ) in Filter.atTop, normalizedL2Norm (euclideanBall d r) z.globalValueRepresentative ≤ D * ENNReal.ofReal r

Carrier-specialized form of the preceding real-radius bridge.

theorem HCPolySupport.HighContrast.tendsto_normalizedL2Norm_sublinear_of_eventually_linear {d : ℕ} {v : Vec d → ℝ} {ϑ : ℝ} (hϑ : 0 < ϑ) (hlinear : ∃ (D : ENNReal), D ≠ ⊤ ∧ ∀ᶠ (r : ℝ) in Filter.atTop, normalizedL2Norm (euclideanBall d r) v ≤ D * ENNReal.ofReal r) : Filter.Tendsto (fun (r : ℝ) => ENNReal.ofReal (r ^ (-(1 + ϑ))) * normalizedL2Norm (euclideanBall d r) v) Filter.atTop (nhds 0)

Any eventual linear normalized-ball bound is sublinear of every strictly larger power, in the exact frozen ENNReal formulation.

theorem HCPolySupport.HighContrast.NormalizedLocalH1Carrier.tendsto_normalizedL2Norm_sublinear_of_cubeGrowth {d : ℕ} [NeZero d] (z : NormalizedLocalH1Carrier d) (q₀ : ℕ) (C : ℝ) (hC : 0 ≤ C) (hcube : ∀ (q : ℕ), q₀ ≤ q → cubeLpNorm (originCube d ↑q) 2 z.globalValueRepresentative ≤ C * 3 ^ q) {ϑ : ℝ} (hϑ : 0 < ϑ) : Filter.Tendsto (fun (r : ℝ) => ENNReal.ofReal (r ^ (-(1 + ϑ))) * normalizedL2Norm (euclideanBall d r) z.globalValueRepresentative) Filter.atTop (nhds 0)

A discrete cube-growth estimate for a normalized local carrier therefore implies the exact frozen sublinear-growth limit.

theorem HCPolySupport.HighContrast.tendsto_normalizedL2Norm_sublinear_of_cubeGrowth {d : ℕ} [NeZero d] (f : Vec d → ℝ) (q₀ : ℕ) (C : ℝ) (hC : 0 ≤ C) (hmem : ∀ (q : ℕ), MeasureTheory.MemLp f 2 (normalizedCubeMeasure (originCube d ↑q))) (hcube : ∀ (q : ℕ), q₀ ≤ q → cubeLpNorm (originCube d ↑q) 2 f ≤ C * 3 ^ q) {ϑ : ℝ} (hϑ : 0 < ϑ) : Filter.Tendsto (fun (r : ℝ) => ENNReal.ofReal (r ^ (-(1 + ϑ))) * normalizedL2Norm (euclideanBall d r) f) Filter.atTop (nhds 0)

Generic discrete-to-continuous frozen growth bridge.