High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Duality.H10AffinePullbackAssembly

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

The H10Function affine pullback, assembled: the potential half

HCPoly.Analytic.AffineWeakGradient transports H1Function along an invertible matrix, and HCPoly.Provider.PolynomialHomogenization.Root.RowSupplyAssembly.H10AffinePullback supplies the two eLpNorm convergences of the approximating sequence. This file assembles the six H10Function fields and reads off the covariant transport of IsPotentialZeroTraceOn, which is the potential half of the affine gauge move.

The H1Function pullback is built here as an explicit structure rather than taken from the existential exists_h1Function_affinePullback, so that its two projections reduce by rfl and the convergence fields are never matched through an opaque witness.

theorem HCPolySupport.HighContrast.RowSupply.gradMemL2On_affinePullbackTranspose {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} (hU : MeasurableSet U) {Du : Vec d → Vec d} (hDu : GradMemL2On U Du) : GradMemL2On (matImage L⁻¹ U) fun (y : Vec d) => matVecMul (matTranspose L) (Du (matVecMul L y))

The gradient L² condition transports with the transpose matrix. (The proof of exists_h1Function_affinePullback uses a private lemma of the same content; it is reproved here rather than imported.)

theorem HCPolySupport.HighContrast.RowSupply.tendsto_pullback_approx {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} (hU : MeasurableSet U) (u : H10Function U) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (y : Vec d) => u.approx n (matVecMul L y) - u.toFun (matVecMul L y)) 2 (MeasureTheory.volume.restrict (matImage L⁻¹ U))) Filter.atTop (nhds 0)

The scalar convergence field of the pulled-back H¹₀ witness.

theorem HCPolySupport.HighContrast.RowSupply.tendsto_pullback_approx_grad {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} (hU : MeasurableSet U) (u : H10Function U) (i : Fin d) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (y : Vec d) => (fderiv ℝ (fun (x : Vec d) => u.approx n (matVecMul L x)) y) (basisVec i) - matVecMul (matTranspose L) (u.grad (matVecMul L y)) i) 2 (MeasureTheory.volume.restrict (matImage L⁻¹ U))) Filter.atTop (nhds 0)

The gradient convergence field of the pulled-back H¹₀ witness.

def HCPolySupport.HighContrast.RowSupply.h1AffinePullback {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} (hU : MeasurableSet U) (u : H1Function U) : H1Function (matImage L⁻¹ U)

The affine pullback of an H¹ witness, as an explicit structure.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.HighContrast.RowSupply.h10AffinePullback {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} (hU : MeasurableSet U) (u : H10Function U) : H10Function (matImage L⁻¹ U)

The affine pullback of an H¹₀ witness, as an explicit structure.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.RowSupply.isPotentialZeroTraceOn_affinePullback {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} (hU : MeasurableSet U) {f : Vec d → Vec d} (hf : IsPotentialZeroTraceOn U f) : IsPotentialZeroTraceOn (matImage L⁻¹ U) fun (y : Vec d) => matVecMul (matTranspose L) (f (matVecMul L y))

The covariant transport of the zero-trace potential predicate under an invertible matrix: this is the potential half of the affine gauge move.