High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Corrector.PushforwardAffineGeometry

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

Geometry and locality for the affine pushforward

Two facts the pushforward construction needs and the tree does not have.

• the reverse sandwich: every centered exhaustion cube is contained in the matrix image of a fixed coarser one, so the affine pullback of a carrier can be read on the exhaustion in either direction;
• locality of the global weak gradient: a weak-gradient pair on every centered exhaustion cube is a weak-gradient pair on all of Vec d. The available affine-pullback transports of HasWeakGradientOn demand L² or integrability on the source domain, which no corrector satisfies globally; locality is what lets them be applied cube by cube and assembled.

Test functions live in a centered cube

theorem HCPolySupport.HighContrast.Root.exists_tsupport_subset_localGradientCube {d : ℕ} {phi : Vec d → ℝ} (hphi : HasCompactSupport phi) : ∃ (n : ℕ), tsupport phi ⊆ localGradientCube d n

A compactly supported test function is supported in some centered exhaustion cube.

Locality of the global weak gradient

theorem HCPolySupport.HighContrast.Root.setIntegral_eq_of_vanishing {d : ℕ} {f : Vec d → ℝ} {U V : Set (Vec d)} (hU : ∀ x ∉ U, f x = 0) (hV : ∀ x ∉ V, f x = 0) : ∫ (x : Vec d) in U, f x = ∫ (x : Vec d) in V, f x

Two set integrals of a function vanishing off both sets agree.

theorem HCPolySupport.HighContrast.Root.hasWeakGradientOn_univ_of_localGradientCube {d : ℕ} {u : Vec d → ℝ} {Du : Vec d → Vec d} (h : ∀ (n : ℕ), HasWeakGradientOn (localGradientCube d n) u Du) : HasWeakGradientOn Set.univ u Du

The weak-gradient identity on a centered cube containing the support of the test is the identity on all of Vec d.

theorem HCPolySupport.HighContrast.Root.hasWeakGradientOn_subset {d : ℕ} {u : Vec d → ℝ} {Du : Vec d → Vec d} {U V : Set (Vec d)} (hVU : V ⊆ U) (h : HasWeakGradientOn U u Du) : HasWeakGradientOn V u Du

A weak-gradient pair on a set restricts to every subset, because the test is supported in the subset.

The reverse sandwich

theorem HCPolySupport.HighContrast.Root.exists_localGradientCube_subset_matImage {d : ℕ} (L : Mat d) (hL : IsUnit (Matrix.det L)) : ∃ (k : ℕ), ∀ (n : ℕ), localGradientCube d n ⊆ matImage L (localGradientCube d (n + k))

Every centered exhaustion cube sits inside the matrix image of a fixed coarser one. This is the direction the pushforward needs; the inclusion into the affine pullback gives the other one.