Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.AffineGradientQuotientPullback

High-contrast homogenization: Provider.Regularity.AffineGradientQuotientPullback #

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

Affine pullback on gradient quotient classes #

This file defines the affine action directly on the Hilbert L² quotient carrier. Its public characterization is an almost-everywhere formula, so later transfers never need to choose a raw representative.

source
theorem HCPolySupport.HighContrast.ae_affinePullback {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} (hU : MeasurableSet U) {P : Vec d → Prop} (hP : ∀ᵐ (x : Vec d) ∂volumeMeasureOn U, P x) :
∀ᵐ (y : Vec d) ∂volumeMeasureOn (matImage L⁻¹ U), P (matVecMul L y)

Almost-everywhere identities pull back through an invertible matrix on the exact inverse-image domain.

source
theorem HCPolySupport.HighContrast.memVectorL2_affineGradientPullback {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 U)) :
MemVectorL2 V fun (y : Vec d) => matVecMul A (↑↑F (matVecMul L y)).toVec

Square integrability of the literal matrix-valued affine pullback of a Hilbert L² quotient representative.

source
noncomputable def HCPolySupport.HighContrast.affineGradientQuotientPullback {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 U) → ↥(HilbertVectorL2 V)

Pull a Hilbert L² gradient quotient from U to the inverse-image domain V, composing its representative with L and applying the fixed matrix A to its values.

Equations
Instances For
    source
    theorem HCPolySupport.HighContrast.coeFn_affineGradientQuotientPullback {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 U)) :
    ↑↑(affineGradientQuotientPullback hL hU hV A F) =ᵐ[volumeMeasureOn V] fun (y : Vec d) => HilbertVec.ofVec (matVecMul A (↑↑F (matVecMul L y)).toVec)

    The quotient pullback has the literal affine representative almost everywhere on its target domain.