High-contrast homogenization: Provider.Regularity.CorrectorCoarseOscillationGrowth

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

Coarse-grained cube growth of the anchored corrector

At a good scale the large-scale Poincare inequality on nested adapted cubes bounds the normalized L² oscillation of a cube solution by the scale times its coefficient energy, with a constant depending only on the dimension and the multiscale order: the lower ellipticity entering it is the coarse-grained response average of the good cube, never a pointwise ellipticity constant.

Applied to the affine-plus-corrector cube solution, and after removing the affine part by the elementary bound on a centered linear function, this is the scale-linear oscillation growth of the anchored corrector itself, which is what the anchored mean telescope consumes. No representative of the physical coefficient field appears in it.

theorem HCPolySupport.HighContrast.cubeLpNorm_le_of_bound_on_cubeSet {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (hp : p ≠ 0) (f : Vec d → ℝ) {B : ℝ} (hB : 0 ≤ B) (hbound : ∀ x ∈ cubeSet Q, ‖f x‖ ≤ B) : cubeLpNorm Q p f ≤ B

A pointwise bound on a cube controls every finite normalized cube Lᵖ norm.

theorem HCPolySupport.HighContrast.cubeLpNorm_originCube_vecDot_le {d : ℕ} (q : ℕ) (e : Vec d) : (cubeLpNorm (originCube d ↑q) 2 fun (x : Vec d) => vecDot e x) ≤ (∑ i : Fin d, |e i|) / 2 * 3 ^ q

The normalized L² norm of a centered affine function is bounded by half its coordinate ℓ¹ slope times the cube side length.

theorem HCPolySupport.HighContrast.exists_scalarIdentityGoodTailCorrectorOscillationConstant (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) : ∃ (K : ℝ) (c : ℝ), 0 < K ∧ c ∈ Set.Ioo 0 1 ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (delta : ℝ) (n : ℤ), delta ∈ Set.Ioc 0 c → ScalarIdentityGoodTail a s delta n → ∀ (hCauchy : FiniteAffineCorrectionLocalCauchy a) (e : Vec d) (q : ℕ), n ≤ ↑q → cubeBesovOscillation (originCube d ↑q) 2 ((finiteAffineCorrectionJointLocalLimit a hCauchy e).localH1Function q).toFun ≤ K * euclideanNorm e * 3 ^ q

Coarse-grained Poincare for the joint local corrector. At a good scale the normalized L² oscillation of the anchored corrector on a centered triadic cube is bounded by the scale times the Euclidean slope, with a constant depending only on the dimension and the multiscale order.