Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Fractional.ContinuousInterpolation.ZeroDimensionalClosure

Coarse-graining support: Support.Sobolev.Fractional.ContinuousInterpolation.ZeroDimensionalClosure #

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

Zero-dimensional closure of the continuous interpolation quantities #

All vector fields and gradient matrices in dimension zero are forced to vanish. This module records the resulting exact zero identities for the normalized L², continuous K, sampled series, and Euclidean fractional quantities.

source
theorem HCPolySupport.normalizedEuclideanLpENorm_zero_dim (F : UnitCubeEuclideanL2Field 0) :
(unitCenteredCubeDomain 0).normalizedEuclideanLpENorm 2 F.toField = 0

The normalized Euclidean extended L² norm vanishes in dimension zero.

source
theorem HCPolySupport.continuousKFunctional_zero_dim (t : ↑ContinuousKScale) (F : UnitCubeEuclideanL2Field 0) :
continuousKFunctional t F = 0

The continuous K-functional vanishes at every scale in dimension zero.

source
theorem HCPolySupport.triadicContinuousKSampleTerm_zero_dim (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field 0) (j : ℕ) :
triadicContinuousKSampleTerm s F j = 0

Every weighted triadic K sample vanishes in dimension zero.

source
theorem HCPolySupport.triadicContinuousKSampleEnergy_zero_dim (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field 0) :
triadicContinuousKSampleEnergy s F = 0

The full triadic sampled K energy vanishes in dimension zero.

source
theorem HCPolySupport.triadicContinuousKShiftedSampleEnergy_zero_dim (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field 0) :
triadicContinuousKShiftedSampleEnergy s F = 0

The shifted triadic sampled K energy vanishes in dimension zero.

source
theorem HCPolySupport.continuousKSeminorm_zero_dim (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field 0) :
continuousKSeminorm s F = 0

The continuum interpolation seminorm vanishes in dimension zero.

source
theorem HCPolySupport.euclideanHsESeminorm_zero_dim (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field 0) :
euclideanHsESeminorm s F = 0

The exact Euclidean fractional seminorm vanishes in dimension zero.