High-contrast homogenization: Provider.Regularity.LocalGradientTranslation

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

Translation of projective local gradients

Translating a local gradient class moves each exhaustion cube off centre, so a compatible translate is read off a larger cube. A fixed index shift, depending only on the translation vector, suffices for every cube of the exhaustion, and the resulting componentwise maps are norm-nonincreasing continuous linear maps.

They assemble into a translation operator on the projective carrier which is linear, measurable, and compatible with the raw-field constructor. This is the covariance carrier for translation-covariant local gradient families.

The cube-index shift of a translation

theorem HCPolySupport.HighContrast.exists_translationDepth {d : ℕ} (z : Vec d) : ∃ (N : ℕ), 1 + 2 * ‖z‖ ≤ 3 ^ N

noncomputable def HCPolySupport.HighContrast.translationDepth {d : ℕ} (z : Vec d) : ℕ

An exhaustion-index shift large enough that translation by z carries every centered cube into the shifted one.

Equations

• HCPolySupport.HighContrast.translationDepth z = Classical.choose ⋯

theorem HCPolySupport.HighContrast.translationDepth_spec {d : ℕ} (z : Vec d) : 1 + 2 * ‖z‖ ≤ 3 ^ translationDepth z

theorem HCPolySupport.HighContrast.add_mem_localGradientCube {d : ℕ} (z : Vec d) (n : ℕ) {x : Vec d} (hx : x ∈ localGradientCube d n) : x + z ∈ localGradientCube d (n + translationDepth z)

Translation by z carries the nth exhaustion cube into the cube shifted by the translation depth.

Translation on one local class

theorem HCPolySupport.HighContrast.memVectorL2_translate_localGradientCube {d : ℕ} (z : Vec d) (f : Vec d → Vec d) (hf : ∀ (n : ℕ), MemVectorL2 (localGradientCube d n) f) (n : ℕ) : MemVectorL2 (localGradientCube d n) fun (x : Vec d) => f (x + z)

A locally square-integrable vector field stays locally square-integrable after translation.

Translation on the projective carrier