Documentation

LeanPool.HighContrastHomogenization.Provider.PolynomialHomogenization.Root.Corrector.PushforwardWeakGradient

High-contrast homogenization: #

Provider.PolynomialHomogenization.Root.Corrector.PushforwardWeakGradient

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

The pushforward pair is a global weak-gradient pair #

hasWeakGradientOn_affinePullback transports a weak-gradient pair along an invertible matrix, but it demands L² control on the source domain, which no corrector satisfies globally. The locality lemma (hasWeakGradientOn_univ_of_localGradientCube) and reverse sandwich (exists_localGradientCube_subset_matImage) are exactly what lets it be applied cube by cube and assembled on Set.univ.

The gauge root is symmetric, so the transpose factor produced by the pullback is the inverse root itself and the conclusion is literally pushforwardGradient.

source
theorem HCPolySupport.HighContrast.Root.isUnit_det_gaugeRoot_inv {d : ℕ} [NeZero d] {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) :
IsUnit (Matrix.det (gaugeRoot abar)⁻¹)

The inverse gauge root is invertible.

source
theorem HCPolySupport.HighContrast.Root.matTranspose_gaugeRoot_inv {d : ℕ} [NeZero d] {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) :
matTranspose (gaugeRoot abar)⁻¹ = (gaugeRoot abar)⁻¹

The inverse gauge root is symmetric.

source
theorem HCPolySupport.HighContrast.Root.hasWeakGradientOn_univ_pushforward {d : ℕ} [NeZero d] {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) (G : NormalizedLocalH1Carrier d) :
HasWeakGradientOn Set.univ (pushforwardValue abar G) (pushforwardGradient abar G)

Clause (3) for the pushforward family. The affine pushforward of a normalized-gauge carrier's canonical representatives is a weak-gradient pair on all of Vec d.