High-contrast homogenization: Provider.Regularity.AffineGradientQuotientInverse

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

Inverse law for affine gradient quotient pullback

The quotient transport is inverted on the same fixed source and target domains by the inverse coordinate matrix and inverse value action.

theorem HCPolySupport.HighContrast.affinePullbackDomain_inverse {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U V : Set (Vec d)} (hV : V = matImage L⁻¹ U) : U = matImage L⁻¹⁻¹ V

If V is the inverse-image of U under L, then U is the inverse-image of V under L⁻¹.

noncomputable def HCPolySupport.HighContrast.affineGradientQuotientPushforward {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U V : Set (Vec d)} (hU : MeasurableSet U) (hV : V = matImage L⁻¹ U) (A : Mat d) : ↥(HilbertVectorL2 V) → ↥(HilbertVectorL2 U)

Push a gradient quotient from the affine inverse-image domain back to the original domain.

Equations

• HCPolySupport.HighContrast.affineGradientQuotientPushforward hL hU hV A = HCPolySupport.HighContrast.affineGradientQuotientPullback ⋯ ⋯ ⋯ A

theorem HCPolySupport.HighContrast.coeFn_affineGradientQuotientPushforward {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U V : Set (Vec d)} (hU : MeasurableSet U) (hV : V = matImage L⁻¹ U) (A : Mat d) (F : ↥(HilbertVectorL2 V)) : ↑↑(affineGradientQuotientPushforward hL hU hV A F) =ᵐ[volumeMeasureOn U] fun (x : Vec d) => HilbertVec.ofVec (matVecMul A (↑↑F (matVecMul L⁻¹ x)).toVec)

The quotient pushforward has the literal inverse-coordinate representative almost everywhere on the original domain.