High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Corrector.PushforwardH1sLocTranslate

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

Local Sobolev membership under a translation by an arbitrary real vector

MemH1sLoc is a conjunction of a measurability clause, a weak-gradient clause on every centred ball, and a smooth-approximation clause in the H¹_s norm. All three transport along v ↦ v (· + t) with the coefficient field translating with them, for an arbitrary real vector t, and an additive recentring v ↦ v - c is free.

Two facts do the work.

• The weak-gradient clause on B_R follows from the clause on B_{R + ‖t‖} because B_R + t ⊆ B_{R + ‖t‖}: the available HasWeakGradientOn.untranslate moves a pair from a translated set, and hasWeakGradientOn_subset restricts. The additive constant needs the vanishing of ∫_U ∂_i φ for a test supported in U, which is the constant case of HasWeakPartialDerivOn.of_contDiff.
• h1sNormSqOn is an unnormalized integral, so it is monotone in the domain with no volume factor; the approximants transport with no constant at all.

Recentring a weak-gradient pair

theorem HCPolySupport.HighContrast.Root.HasWeakGradientOn.sub_const {d : ℕ} {U : Set (Vec d)} {u : Vec d → ℝ} {Du : Vec d → Vec d} (h : HasWeakGradientOn U u Du) (c : ℝ) : HasWeakGradientOn U (fun (x : Vec d) => u x - c) Du

A weak-gradient pair survives subtraction of a constant from its value field. The gradient is unchanged.

The proof is the vanishing of ∫_U c ∂_i φ, which is the constant case of HasWeakPartialDerivOn.of_contDiff, together with a case split on whether u ∂_i φ is integrable on U: the definition uses a totalized Bochner integral, so the split is what keeps the additive step honest.

Geometry: a ball translated by t sits in the ball grown by ‖t‖

theorem HCPolySupport.HighContrast.Root.euclideanBallAt_subset_euclideanBall_add {d : ℕ} (t : Vec d) {r : ℝ} (hr : 0 ≤ r) : euclideanBallAt t r ⊆ euclideanBall d (r + √(vecNormSq t))

The ball of radius r centred at t sits inside the centred ball of radius r + ‖t‖, the Euclidean length being written through vecNormSq.

The H¹_s norm is monotone under a translated inclusion

theorem HCPolySupport.HighContrast.Root.lintegral_translate_le {d : ℕ} {U V : Set (Vec d)} (t : Vec d) (hUV : translateSet t U ⊆ V) (g : Vec d → ENNReal) : ∫⁻ (x : Vec d) in U, g (x + t) ≤ ∫⁻ (y : Vec d) in V, g y

Lower Lebesgue integrals transport along a translation and are monotone in the domain.

theorem HCPolySupport.HighContrast.Root.h1sNormSqOn_translate_le {d : ℕ} (b : CoeffField d) {U V : Set (Vec d)} (t : Vec d) (hUV : translateSet t U ⊆ V) (f : Vec d → ℝ) (F : Vec d → Vec d) : (h1sNormSqOn (fun (y : Vec d) => b (y + t)) U (fun (y : Vec d) => f (y + t)) fun (y : Vec d) => F (y + t)) ≤ h1sNormSqOn b V f F

The coefficient-weighted H¹_s norm square of a translated pair on U is at most the norm square of the untranslated pair on any set containing the translate of U. The norm is unnormalized, so there is no volume factor.

The coordinate gradient under a translation

theorem HCPolySupport.HighContrast.Root.smoothGrad_comp_addRight_sub_const {d : ℕ} (f : Vec d → ℝ) (t : Vec d) (c : ℝ) (x : Vec d) : smoothGrad (fun (y : Vec d) => f (y + t) - c) x = smoothGrad f (x + t)

The coordinate gradient of a translated and recentred smooth function is the translated coordinate gradient.

The MemH1sLoc conjunct of the Liouville class, transported

theorem HCPolySupport.HighContrast.Root.memH1sLoc_realTranslate_subConst {d : ℕ} {b : CoeffField d} {v : Vec d → ℝ} {Dv : Vec d → Vec d} (h : MemH1sLoc b v Dv) (t : Vec d) (c : ℝ) : MemH1sLoc (fun (y : Vec d) => b (y + t)) (fun (y : Vec d) => v (y + t) - c) fun (y : Vec d) => Dv (y + t)

MemH1sLoc transports along a translation by an arbitrary real vector, the coefficient field translating with the pair, and an arbitrary additive recentring is free.