High-contrast homogenization:

Provider.PolynomialHomogenization.Root.RowSupplyAssembly.H10AffinePullback

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

The H10Function affine pullback: the zero-trace half

HCPoly.Analytic.AffineWeakGradient already transports H1Function along an invertible affine map (exists_h1Function_affinePullback). What is missing — and what IsPotentialZeroTraceOn needs, since it is stated as existence of an H10Function whose gradient is the field — is the zero-trace half: the approximating sequence and its two eLpNorm convergences.

Three of the six H10Function fields come free from the isLocalTest_comp_matVecMul, which is exactly "smooth, compactly supported, supported in the preimage". The two convergences transport through the measure pushforward map_restrict_volume_affinePullback, which contributes the fixed Jacobian factor |det L|⁻¹; since that factor is a nonzero constant, convergence to 0 is preserved.

theorem HCPolySupport.HighContrast.RowSupply.eLpNorm_comp_matVecMul {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} (hU : MeasurableSet U) {f : Vec d → ℝ} (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict U)) : MeasureTheory.eLpNorm (fun (y : Vec d) => f (matVecMul L y)) 2 (MeasureTheory.volume.restrict (matImage L⁻¹ U)) = ENNReal.ofReal |Matrix.det L|⁻¹ ^ (1 / 2) * MeasureTheory.eLpNorm f 2 (MeasureTheory.volume.restrict U)

eLpNorm of an affine pullback, in terms of the original, with the Jacobian factor supplied by map_restrict_volume_affinePullback.

theorem HCPolySupport.HighContrast.RowSupply.tendsto_eLpNorm_comp_matVecMul_zero {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} (hU : MeasurableSet U) {F : ℕ → Vec d → ℝ} (hmeas : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (F n) (MeasureTheory.volume.restrict U)) (h : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (F n) 2 (MeasureTheory.volume.restrict U)) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (y : Vec d) => F n (matVecMul L y)) 2 (MeasureTheory.volume.restrict (matImage L⁻¹ U))) Filter.atTop (nhds 0)

Convergence to zero of an L² sequence survives the affine pullback.

theorem HCPolySupport.HighContrast.RowSupply.tendsto_eLpNorm_transpose_comp_zero {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} (hU : MeasurableSet U) {D : ℕ → Vec d → Vec d} (hmeas : ∀ (n : ℕ) (j : Fin d), MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => D n x j) (MeasureTheory.volume.restrict U)) (hmeasV : ∀ (n : ℕ) (j : Fin d), MeasureTheory.AEStronglyMeasurable (fun (y : Vec d) => D n (matVecMul L y) j) (MeasureTheory.volume.restrict (matImage L⁻¹ U))) (h : ∀ (j : Fin d), Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => D n x j) 2 (MeasureTheory.volume.restrict U)) Filter.atTop (nhds 0)) (i : Fin d) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (y : Vec d) => matVecMul (matTranspose L) (D n (matVecMul L y)) i) 2 (MeasureTheory.volume.restrict (matImage L⁻¹ U))) Filter.atTop (nhds 0)

Componentwise convergence of the transposed pullback gradient.