Documentation

LeanPool.HighContrastHomogenization.Provider.PolynomialHomogenization.Root.RowSupply.EpsilonAffineLoadNormalization

High-contrast homogenization: #

Provider.PolynomialHomogenization.Root.RowSupply.EpsilonAffineLoadNormalization

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

Load normalization for the microscopic affine gauge #

Microscopic dilation is absorbed into the affine grid and the positive scalar coefficient normalization. The resulting transformed loads are exactly the usual normalized-reference loads.

source
noncomputable def HCPolySupport.HighContrast.RowSupply.epsilonAffineGrid {d : ℕ} (epsilon : ℝ) (abar : Mat d) :
Mat d

The affine grid after passing from physical to microscopic coordinates.

Equations
Instances For
    source
    noncomputable def HCPolySupport.HighContrast.RowSupply.epsilonCoefficientScale (epsilon : ℝ) :
    ℝ

    The coefficient multiplier paired with epsilonAffineGrid.

    Equations
    Instances For
      source
      theorem HCPolySupport.HighContrast.RowSupply.epsilonAffineGrid_posDef {d : ℕ} {epsilon : ℝ} (hepsilon : 0 < epsilon) {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) :
      Matrix.PosDef (epsilonAffineGrid epsilon abar)
      source
      theorem HCPolySupport.HighContrast.RowSupply.epsilonCoefficientScale_pos {epsilon : ℝ} (hepsilon : 0 < epsilon) :
      0 < epsilonCoefficientScale epsilon
      source
      theorem HCPolySupport.HighContrast.RowSupply.sqrt_epsilonCoefficientScale {epsilon : ℝ} (hepsilon : 0 < epsilon) :
      √(epsilonCoefficientScale epsilon) = epsilon⁻¹
      source
      theorem HCPolySupport.HighContrast.RowSupply.affine_scalar_skew_primalLoad_epsilon_eq_normalizedReference {d : ℕ} [NeZero d] {epsilon : ℝ} (hepsilon : 0 < epsilon) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (P : BlockVec d) :
      affineReferencePrimalLoad (epsilonAffineGrid epsilon abar) (scalarNormalizedPrimalLoad (√(epsilonCoefficientScale epsilon)) (skewCenteredPrimalLoad (skewPart abar) P)) = normalizedReferencePrimalLoad abar P

      Primal loads transformed by microscopic scalar normalization and the microscopic affine grid coincide with the normalized-reference primal load.

      source
      theorem HCPolySupport.HighContrast.RowSupply.affine_scalar_skew_dualLoad_epsilon_eq_normalizedReference {d : ℕ} [NeZero d] {epsilon : ℝ} (hepsilon : 0 < epsilon) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (Q : BlockVec d) :
      affineReferenceDualLoad (epsilonAffineGrid epsilon abar) (scalarNormalizedDualLoad (√(epsilonCoefficientScale epsilon)) (skewCenteredDualLoad (skewPart abar) Q)) = normalizedReferenceDualLoad abar Q

      The analogous identity for dual loads.