Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Fractional.CenteredCubeDivergenceRescaling

Coarse-graining support: Support.Sobolev.Fractional.CenteredCubeDivergenceRescaling #

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Coefficient rescaling for centered-cube divergence solutions #

This file converts the normalized weak formulation with a positive scalar coefficient into the raw cube Dirichlet divergence problem with rescaled data.

source
theorem HCPolySupport.centeredCubeH10ScalarDivergenceSolution_to_cubeDirichletDivergenceProblem {d : ℕ} (m : ℤ) (sigma0 : ℝ) {s : ↑FractionalOrder} {p : FiniteLpExponent} (h : CubeEuclideanWspL2Field (originCube d m) s p) (w : H10Function (openCubeSet (originCube d m))) (hsigma0 : 0 < sigma0) (hsolution : IsCenteredCubeH10ScalarDivergenceSolution m sigma0 w h.toLpTwo) :
CubeDirichletDivergenceProblem (originCube d m) w fun (x : Vec d) => sigma0⁻¹ • h.toField x

Dividing the positive scalar coefficient in the normalized centered-cube weak formulation gives the raw cube divergence problem with inversely scaled datum.