High-contrast homogenization: Analytic.AffinePairing

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

Pairings under an invertible affine normalization

An invertible matrix transports absolute integrability between a set and its linear image. Consequently the determinant Jacobian cancels in the normalized duality pairing.

theorem HCPolySupport.HighContrast.measurableEmbedding_matVecMul {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) : MeasurableEmbedding (matVecMul L)

Multiplication by an invertible matrix is a measurable embedding.

theorem HCPolySupport.HighContrast.IsLocalVecTest.comp_matVecMul {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} {psi : Vec d → Vec d} (hpsi : IsLocalVecTest (matImage L U) psi) : IsLocalVecTest U fun (y : Vec d) => psi (matVecMul L y)

Pulling a compactly supported smooth vector test back by an invertible matrix gives a test on the inverse-image domain.

theorem HCPolySupport.HighContrast.integrableOn_matImage_iff {d : ℕ} {F : Type u_1} [NormedAddCommGroup F] {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} (hU : MeasurableSet U) (f : Vec d → F) : MeasureTheory.IntegrableOn f (matImage L U) MeasureTheory.volume ↔ MeasureTheory.IntegrableOn (fun (y : Vec d) => f (matVecMul L y)) U MeasureTheory.volume

Absolute integrability is equivalent before and after an invertible linear change of variables.

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

Normalized nonnegative averages are unchanged after affine pullback.

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

The normalized scalar L² norm is invariant under simultaneous affine transport of the domain and field.

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

The symmetric energy density is invariant under the dual affine actions on gradients and fluxes.

theorem HCPolySupport.HighContrast.weightedGradNorm_matImage {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} (hU : MeasurableSet U) (a : CoeffField d) (F : Vec d → Vec d) : weightedGradNorm a (matImage L U) F = weightedGradNorm (affineCoefficient L hL a) U fun (y : Vec d) => matVecMul (matTranspose L) (F (matVecMul L y))

The normalized coefficient-weighted gradient norm is invariant under the divergence-form affine pullback.

theorem HCPolySupport.HighContrast.dualPairing_matImage {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} (hU : MeasurableSet U) (F psi : Vec d → Vec d) : dualPairing (matImage L U) F psi = dualPairing U (fun (y : Vec d) => F (matVecMul L y)) fun (y : Vec d) => psi (matVecMul L y)

The normalized pairing is unchanged when both fields are pulled back by the same invertible coordinate map.