High-contrast homogenization: Provider.Regularity.HarmonicGradientOscillation

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

noncomputable def HCPolySupport.CubeCalderonZygmund.depthTargetExponent (d p : ℕ) [NeZero d] (hp : 0 < p) : FiniteLpExponent

The finite exponent 2 * d * p used to control restriction to depth 2 * p * t.

Equations

• HCPolySupport.CubeCalderonZygmund.depthTargetExponent d p hp = { exponent := ENNReal.ofReal (2 * ↑d * ↑p), one_lt := ⋯, lt_top := ⋯ }

theorem HCPolySupport.CubeCalderonZygmund.exists_harmonic_gradient_oscillation_decay_at_integer_rate (d p : ℕ) [NeZero d] (hp : 0 < p) : ∃ (depth : ℕ) (C : ENNReal), C ≠ ⊤ ∧ ∀ (Q : TriadicCube d) (u : H1Function (openCubeSet Q)), (WeakPoissonEquationOn (openCubeSet Q) u fun (x : Vec d) => 0) → ∀ (t : ℕ), have R := centralDescendant (centralDescendant (centralChild Q) depth) (2 * p * t); MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertVec.ofVec (u.grad x - cubeAverageVec R u.grad)) 2 (normalizedCubeMeasure R) ≤ C * 3⁻¹ ^ ((2 * p - 1) * t) * MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertVec.ofVec (u.grad x)) 2 (normalizedCubeMeasure Q)

A harmonic gradient becomes geometrically close in normalized L² to its average on sufficiently deep central descendants. Both the gain depth and the prefactor are dimension-only construction data.

theorem HCPolySupport.CubeCalderonZygmund.exists_pos_nat_harmonic_integer_rate_gt {eta : ℝ} (heta : eta < 1) : ∃ (p : ℕ), 0 < p ∧ eta < 1 - 1 / (2 * ↑p)

The effective per-scale exponents of the integer-rate family approach one from below.