High-contrast homogenization: Analytic.AffineGeometry

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

Affine geometry and coefficient pullback

An invertible matrix sends a coefficient field to its divergence-form pullback, sends the corresponding domain to a linear image, and rescales both volume and unnormalized integrals by its determinant. The determinant cancels from normalized averages.

noncomputable def HCPolySupport.HighContrast.affineCoefficient {d : ℕ} (L : Mat d) (_hL : IsUnit (Matrix.det L)) (a : CoeffField d) : CoeffField d

The divergence-form coefficient after the invertible change of variables x = L y.

Equations

• HCPolySupport.HighContrast.affineCoefficient L _hL a y = L⁻¹ * a (HCPolySupport.matVecMul L y) * HCPolySupport.matTranspose L⁻¹

@[simp]

theorem HCPolySupport.HighContrast.affineCoefficient_apply {d : ℕ} (L : Mat d) (hL : IsUnit (Matrix.det L)) (a : CoeffField d) (y : Vec d) : affineCoefficient L hL a y = L⁻¹ * a (matVecMul L y) * matTranspose L⁻¹

theorem HCPolySupport.HighContrast.matTranspose_affineCoefficient_apply {d : ℕ} (L : Mat d) (hL : IsUnit (Matrix.det L)) (a : CoeffField d) (y : Vec d) : matTranspose (affineCoefficient L hL a y) = L⁻¹ * matTranspose (a (matVecMul L y)) * matTranspose L⁻¹

Transposition commutes with the congruence used by the affine coefficient.

theorem HCPolySupport.HighContrast.symmPart_affineCoefficient_apply {d : ℕ} (L : Mat d) (hL : IsUnit (Matrix.det L)) (a : CoeffField d) (y : Vec d) : symmPart (affineCoefficient L hL a y) = L⁻¹ * symmPart (a (matVecMul L y)) * matTranspose L⁻¹

The symmetric part of an affine coefficient is the congruence of the symmetric part of the original coefficient.

theorem HCPolySupport.HighContrast.skewPart_affineCoefficient_apply {d : ℕ} (L : Mat d) (hL : IsUnit (Matrix.det L)) (a : CoeffField d) (y : Vec d) : skewPart (affineCoefficient L hL a y) = L⁻¹ * skewPart (a (matVecMul L y)) * matTranspose L⁻¹

The skew part of an affine coefficient is the congruence of the skew part of the original coefficient.

theorem HCPolySupport.HighContrast.affineCoefficient_mul_transpose {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) (a : CoeffField d) (y : Vec d) : affineCoefficient L hL a y * matTranspose L = L⁻¹ * a (matVecMul L y)

The right inverse-transpose factor cancels the transformed gradient.

theorem HCPolySupport.HighContrast.affineCoefficient_flux {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) (a : CoeffField d) (y ξ : Vec d) : matVecMul (affineCoefficient L hL a y) (matVecMul (matTranspose L) ξ) = matVecMul L⁻¹ (matVecMul (a (matVecMul L y)) ξ)

Fluxes transform contravariantly under the affine coefficient pullback.

theorem HCPolySupport.HighContrast.affineCoefficient_energy {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) (a : CoeffField d) (y ξ : Vec d) : vecDot (matVecMul (matTranspose L) ξ) (matVecMul (affineCoefficient L hL a y) (matVecMul (matTranspose L) ξ)) = vecDot ξ (matVecMul (a (matVecMul L y)) ξ)

The potential--flux pairing is invariant under the dual affine actions.

Linear images and volume

theorem HCPolySupport.HighContrast.matImage_matImage {d : ℕ} (M N : Mat d) (U : Set (Vec d)) : matImage M (matImage N U) = matImage (M * N) U

Linear images compose by matrix multiplication.

theorem HCPolySupport.HighContrast.matImage_inv_eq_preimage {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) (U : Set (Vec d)) : matImage L⁻¹ U = (fun (y : Vec d) => matVecMul L y) ⁻¹' U

Pulling a domain back by L⁻¹ is the same as taking its preimage by L.

theorem HCPolySupport.HighContrast.volume_matImage {d : ℕ} (L : Mat d) (U : Set (Vec d)) : MeasureTheory.volume (matImage L U) = ENNReal.ofReal |Matrix.det L| * MeasureTheory.volume U

An invertible linear image rescales volume by the absolute determinant.

theorem HCPolySupport.HighContrast.volume_matImage_toReal {d : ℕ} (L : Mat d) (U : Set (Vec d)) : (MeasureTheory.volume (matImage L U)).toReal = |Matrix.det L| * (MeasureTheory.volume U).toReal

The real-valued volume obeys the same determinant scaling.

theorem HCPolySupport.HighContrast.map_restrict_volume_matVecMul {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} (hU : MeasurableSet U) : MeasureTheory.Measure.map (matVecMul L) (MeasureTheory.volume.restrict U) = ENNReal.ofReal |Matrix.det L|⁻¹ • MeasureTheory.volume.restrict (matImage L U)

The restricted source volume pushed through an invertible matrix is the restricted target volume with the inverse Jacobian density.

theorem HCPolySupport.HighContrast.setIntegral_matImage {d : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} (hU : MeasurableSet U) (f : Vec d → F) : ∫ (x : Vec d) in matImage L U, f x = |Matrix.det L| • ∫ (y : Vec d) in U, f (matVecMul L y)

Bochner integration over a linear image carries the determinant Jacobian.

theorem HCPolySupport.HighContrast.volumeAverage_matImage {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} (hU : MeasurableSet U) (f : Vec d → ℝ) : volumeAverage (matImage L U) f = volumeAverage U fun (y : Vec d) => f (matVecMul L y)

Normalized scalar averages are unchanged after affine pullback.

theorem HCPolySupport.HighContrast.matImage_adaptedCell {d : ℕ} (M q : Mat d) (j : ℤ) : matImage M (adaptedCell q j) = adaptedCell (M * q) j

A matrix image sends an adapted cell to the cell with the multiplied grid.