Documentation

LeanPool.HighContrastHomogenization.Provider.PolynomialHomogenization.Root.RowSupply.EpsilonAffineCoefficientRealization

High-contrast homogenization: #

Provider.PolynomialHomogenization.Root.RowSupply.EpsilonAffineCoefficientRealization

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

Exact coefficient realization under microscopic affine scaling #

The physical scaling, real translation, skew removal, and affine square-root gauge are assembled into one coefficient-space sample. The scalar factors cancel exactly in the affine conjugation.

source
noncomputable def HCPolySupport.HighContrast.RowSupply.epsilonAffinePhysicalCoeff {d : ℕ} (epsilon : ℝ) (hepsilon : 0 < epsilon) (center : Vec d) (a : CoeffSpace d) (abar : Mat d) :
CoeffSpace d

The translated, skew-centered, microscopic coefficient sample used before the affine pullback.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem HCPolySupport.HighContrast.RowSupply.epsilonAffinePhysicalCoeff_ae {d : ℕ} {epsilon : ℝ} (hepsilon : 0 < epsilon) (center : Vec d) (a : CoeffSpace d) (abar : Mat d) :
    ↑↑(epsilonAffinePhysicalCoeff epsilon hepsilon center a abar) =ᵐ[MeasureTheory.volume] fun (z : Vec d) => epsilonCoefficientScale epsilon • (↑↑a (z + epsilon⁻¹ • matVecMul (matSqrt (symmPart abar)) center) - skewPart abar)

    The microscopic coefficient sample has the explicit translated and rescaled representative.

    source
    theorem HCPolySupport.HighContrast.RowSupply.affineCoefficient_epsilonAffinePhysicalCoeff_ae {d : ℕ} {epsilon : ℝ} (hepsilon : 0 < epsilon) (center : Vec d) (a : CoeffSpace d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) :
    affineCoefficient (epsilonAffineGrid epsilon abar) ⋯ ↑↑(epsilonAffinePhysicalCoeff epsilon hepsilon center a abar) =ᵐ[MeasureTheory.volume] fun (x : Vec d) => affineCoefficient (matSqrt (symmPart abar)) ⋯ (fun (y : Vec d) => scaledCoeff epsilon a y - skewPart abar) (x + center)

    The affine pullback of the preceding sample is exactly the translated physical gauge coefficient. In particular, real dilation contributes no residual response factor.