Coarse-graining support:

Support.Deterministic.ConstantCoefficientDirichletBesov.CenteredCubeScaleTransport

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

Centered-cube transport for the Dirichlet divergence problem

This module transports the zero-trace weak problem on originCube d m to the centered unit cube. The solution is normalized as wHat(x) = (3 ^ m)⁻¹ w((3 ^ m) x), so its weak gradient is the unscaled pullback of the physical gradient.

Main definitions

• centeredCubeGradientEuclideanL2Field: the physical gradient as an exact centered-cube Euclidean L² field.
• centeredCubeNormalizedPullback: the normalized zero-trace pullback.

Main results

• centeredCubeNormalizedPullback_grad: exact pointwise gradient transport.
• cubeDirichletDivergenceProblem_normalizedPullback: transport of the weak divergence problem to the unit cube.
• unitCubeGradientEuclideanL2Field_normalizedPullback_apply: compatibility of the unit gradient carrier with centered-cube field pullback.

theorem HCPolySupport.centeredOpenCube_eq_smul_unitCenteredOpenCube {d : ℕ} (m : ℤ) : openCubeSet (originCube d m) = centeredCubeScale m • openCubeSet (originCube d 0)

theorem HCPolySupport.unitCenteredOpenCube_eq_inv_smul_centeredOpenCube {d : ℕ} (m : ℤ) : openCubeSet (originCube d 0) = (centeredCubeScale m)⁻¹ • openCubeSet (originCube d m)

noncomputable def HCPolySupport.centeredCubeGradientEuclideanL2Field {d : ℕ} {m : ℤ} (w : H10Function (openCubeSet (originCube d m))) : CenteredCubeEuclideanL2Field d m

The gradient of a physical centered-cube zero-trace function, packaged as the exact Euclidean L² field used by the fractional scale-transport API.

Equations

• HCPolySupport.centeredCubeGradientEuclideanL2Field w = { toField := fun (x : HCPolySupport.Vec d) => w.grad x, euclideanMemL2 := ⋯ }

@[simp]

theorem HCPolySupport.centeredCubeGradientEuclideanL2Field_apply {d : ℕ} {m : ℤ} (w : H10Function (openCubeSet (originCube d m))) (x : Vec d) : (centeredCubeGradientEuclideanL2Field w).toField x = w.grad x

noncomputable def HCPolySupport.centeredCubeNormalizedPullback {d : ℕ} {m : ℤ} (w : H10Function (openCubeSet (originCube d m))) : H10Function (openCubeSet (originCube d 0))

The normalized zero-trace pullback wHat(x) = (3 ^ m)⁻¹ w((3 ^ m) x) from the centered physical cube to the centered unit cube.

Equations

• HCPolySupport.centeredCubeNormalizedPullback w = (HCPolySupport.centeredCubeScale m)⁻¹ • HCPolySupport.H10Function.unscale ⋯ (⋯ ▸ w)

@[simp]

theorem HCPolySupport.centeredCubeNormalizedPullback_apply {d : ℕ} {m : ℤ} (w : H10Function (openCubeSet (originCube d m))) (x : Vec d) : (centeredCubeNormalizedPullback w).toFun x = (centeredCubeScale m)⁻¹ * w.toFun (centeredCubeScale m • x)

Pointwise value formula for the normalized zero-trace pullback.

@[simp]

theorem HCPolySupport.centeredCubeNormalizedPullback_grad {d : ℕ} {m : ℤ} (w : H10Function (openCubeSet (originCube d m))) (x : Vec d) : (centeredCubeNormalizedPullback w).grad x = w.grad (centeredCubeScale m • x)

The normalized pullback has the unscaled physical gradient pointwise.

noncomputable def HCPolySupport.centeredCubeNormalizedTestPushforward {d : ℕ} {m : ℤ} (phi : H10Function (openCubeSet (originCube d 0))) : H10Function (openCubeSet (originCube d m))

Inverse normalized transport of a unit-cube zero-trace test: phi_m(y) = (3 ^ m) phi((3 ^ m)⁻¹ y).

Equations

• HCPolySupport.centeredCubeNormalizedTestPushforward phi = HCPolySupport.centeredCubeScale m • HCPolySupport.H10Function.unscale ⋯ (⋯ ▸ phi)

theorem HCPolySupport.cubeDirichletDivergenceProblem_normalizedPullback {d : ℕ} {m : ℤ} (h : CenteredCubeEuclideanL2Field d m) (w : H10Function (openCubeSet (originCube d m))) (hproblem : CubeDirichletDivergenceProblem (originCube d m) w h.toField) : CubeDirichletDivergenceProblem (originCube d 0) (centeredCubeNormalizedPullback w) h.pullbackToUnit.toField

Exact transport of -Delta w = div h from a centered physical cube to the centered unit cube under the normalized pullback.

theorem HCPolySupport.unitCubeGradientEuclideanL2Field_normalizedPullback_apply {d : ℕ} {m : ℤ} (w : H10Function (openCubeSet (originCube d m))) (x : Vec d) : (unitCubeGradientEuclideanL2Field (centeredCubeNormalizedPullback w)).toField x = (centeredCubeGradientEuclideanL2Field w).pullbackToUnit.toField x

The unit gradient field is pointwise the centered-cube pullback of the physical gradient field.

theorem HCPolySupport.unitCubeGradientEuclideanL2Field_normalizedPullback_ae_eq {d : ℕ} {m : ℤ} (w : H10Function (openCubeSet (originCube d m))) : (unitCubeGradientEuclideanL2Field (centeredCubeNormalizedPullback w)).toField =ᵐ[(unitCenteredCubeDomain d).normalizedVolume] (centeredCubeGradientEuclideanL2Field w).pullbackToUnit.toField

The unit gradient field agrees almost everywhere with the pullback of the physical gradient field.