High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Corrector.PushforwardRealTranslateLiouville

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

The residue, discharged: the Liouville class under a real translation

This module closes RealTranslateLiouville d, and with it clause (1) of the stationary corrector family clause becomes unconditional.

The three conjuncts of MemLiouvilleClass are discharged by the three transports proved here:

conjunct	transport
MemH1sLoc	memH1sLoc_realTranslate_subConst
IsWeakSolutionOn _ univ	IsWeakSolutionOn.translateCoeffField_univ (available)
growth	tendsto_growth_realTranslate_subConst

The coefficient identification translateCoeffField t b = fun y ↦ b (y + t) is definitional, so the weak-solution conjunct needs no rewriting at all.

The 0 < theta binder is necessary; see PushforwardEngineInput.

theorem HCPolySupport.HighContrast.Root.memLiouvilleClass_realTranslate_subConst {d : ℕ} {b : CoeffField d} {theta : ℝ} (htheta : 0 < theta) {v : Vec d → ℝ} {Dv : Vec d → Vec d} (h : MemLiouvilleClass b theta v Dv) (t : Vec d) (c : ℝ) : MemLiouvilleClass (fun (y : Vec d) => b (y + t)) theta (fun (y : Vec d) => v (y + t) - c) fun (y : Vec d) => Dv (y + t)

The Liouville class transports along a translation by an arbitrary real vector, the coefficient field translating with the pair and an arbitrary additive constant absorbed.

The statement is unconditional in b, v, Dv, t and c; the only hypothesis is 0 < theta, which is necessary — see PushforwardEngineInput.

theorem HCPolySupport.HighContrast.Root.realTranslateLiouville (d : ℕ) : RealTranslateLiouville d

The residue, discharged.

theorem HCPolySupport.HighContrast.Root.engine_liouville_input {d : ℕ} [NeZero d] (a : CoeffSpace d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (G : NormalizedLocalH1Carrier d) (e : Vec d) {theta : ℝ} (htheta : 0 < theta) (hLiou : MemLiouvilleClass (gaugeCoeff a abar hS) theta (fun (y : Vec d) => vecDot (matVecMul (gaugeRoot abar) e) y + G.globalValueRepresentative y) fun (y : Vec d) => matVecMul (gaugeRoot abar) e + G.globalGradientRepresentative y) (z : Fin d → ℤ) : MemLiouvilleClass (gaugeCoeff (translateCoeff z a) abar hS) theta (fun (y : Vec d) => vecDot (matVecMul (gaugeRoot abar) e) y + G.globalValueRepresentative (y + matVecMul (gaugeRoot abar)⁻¹ (Source.AKL.intTranslation z))) fun (y : Vec d) => matVecMul (gaugeRoot abar) e + G.globalGradientRepresentative (y + matVecMul (gaugeRoot abar)⁻¹ (Source.AKL.intTranslation z))

Clause (1)'s engine input, unconditional. On the translated sample the normalized-gauge Liouville membership needed by the translated-gradient identification engine follows from the untranslated one and nothing else.

Every binder is consumer-supplied: hS is RootAssembly's own positive-definite binder, htheta is 0 < rootCorrectorGrowth = 1/2 at the frozen constant, and hLiou is the corrector construction applied at normalizedSample abar hS a.