Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.RoundedPhysicalDirichletAffineResponse

High-contrast homogenization: Provider.Regularity.RoundedPhysicalDirichletAffineResponse #

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

Quotient-first physical rounded Dirichlet response #

The rounded reference-cube response is pushed to the physical adapted cube by the inverse rounded map. The weak right-hand side and the constant reference coefficient are transported together, while the gradient is identified on the Hilbert L² quotient before any representative is used downstream. The Euclidean fractional distortion is recorded in one named affine factor.

source
def HCPolySupport.HighContrast.roundedPhysicalCube {d : ℕ} (abar : Mat d) (m : ℤ) :
Set (Vec d)

The physical adapted cube selected by the source's rounded map.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def HCPolySupport.HighContrast.roundedPhysicalReferenceMatrix {d : ℕ} (abar : Mat d) :
    Mat d

    The scalar-normalized physical symmetric reference whose rounded pullback is roundedReferenceMatrix.

    Equations
    Instances For
      source
      noncomputable def HCPolySupport.HighContrast.roundedPhysicalDirichletDatum {d : ℕ} {m : ℤ} (abar : Mat d) (h : CenteredCubeEuclideanL2Field d m) :
      Vec d → Vec d

      Contravariant transport of a reference-cube divergence datum to the physical rounded cube.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def HCPolySupport.HighContrast.roundedPhysicalGradientHsLoss {d : ℕ} (abar : Mat d) (s : ℝ) :
        ENNReal

        The single Euclidean fractional loss for pushing a gradient from the reference cube to the physical rounded cube. It contains both the domain distortion and the inverse-transpose value action.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem HCPolySupport.HighContrast.exists_roundedPhysicalDirichletAffineResponse {d : ℕ} {m : ℤ} [NeZero d] (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (h : CenteredCubeEuclideanL2Field d m) (w : H10Function (openCubeSet (originCube d m))) (hw : IsZeroTraceDirichletRhsWeakSolution (constantCoeffField (roundedReferenceMatrix abar hS)) (openCubeSet (originCube d m)) w fun (y : Vec d) => -h.toField y) :
          ∃ (wPhysical : H10Function (roundedPhysicalCube abar m)), (wPhysical.toFun = fun (x : Vec d) => w.toFun (matVecMul (baseRoundedGrid (symmPart abar))⁻¹ x)) ∧ (wPhysical.grad = fun (x : Vec d) => matVecMul (baseRoundedGrid (symmPart abar))⁻¹ (w.grad (matVecMul (baseRoundedGrid (symmPart abar))⁻¹ x))) ∧ (IsZeroTraceDirichletRhsWeakSolution (constantCoeffField (roundedPhysicalReferenceMatrix abar)) (roundedPhysicalCube abar m) wPhysical fun (x : Vec d) => -roundedPhysicalDirichletDatum abar h x) ∧ wPhysical.gradToHilbertVectorL2 = affineGradientQuotientPushforward ⋯ ⋯ ⋯ (baseRoundedGrid (symmPart abar))⁻¹ w.gradToHilbertVectorL2 ∧ ∀ (s : ↑FractionalOrder), hsNormSq (roundedPhysicalCube abar m) (↑s) wPhysical.grad ≤ roundedPhysicalGradientHsLoss abar ↑s * hsNormSq (openCubeSet (originCube d m)) (↑s) w.grad

          A normalized rounded-reference response has one physical adapted-cube representative. Its weak equation is the inverse affine image of the reference equation, its gradient is identified on the quotient carrier, and its physical fractional norm pays exactly the named affine loss once.