High-contrast homogenization: Provider.PolynomialHomogenization.PhysicalFullDualBesovNorm

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

The physical full-dual Besov vector norm on a triadic cube

The unnormalized componentwise dual Besov norm of a vector field on a cube, its parent-scale weight, and the identity relating it to the scale-normalized public norm of HCPolySupport.Book.Ch03.

noncomputable def HCPolySupport.HighContrast.physicalFullDualBesovVectorNorm {d : ℕ} (Q : TriadicCube d) (s : ℝ) (F : Vec d → Vec d) : ℝ

The physical vector full-dual Besov norm on a cube, before the public parent-scale normalization is applied.

Equations

• HCPolySupport.HighContrast.physicalFullDualBesovVectorNorm Q s F = ∑ i : Fin d, HCPolySupport.cubeBesovDualFullNorm Q s 2 2 fun (x : HCPolySupport.Vec d) => F x i

noncomputable def HCPolySupport.HighContrast.physicalDualBesovScaleFactor {d : ℕ} (Q : TriadicCube d) (s : ℝ) : ℝ

The inverse of the public dual-Besov parent-scale weight.

Equations

• HCPolySupport.HighContrast.physicalDualBesovScaleFactor Q s = (Real.rpow 3 (-s * ↑Q.scale))⁻¹

theorem HCPolySupport.HighContrast.physicalDualBesovScaleFactor_nonneg {d : ℕ} (Q : TriadicCube d) (s : ℝ) : 0 ≤ physicalDualBesovScaleFactor Q s

theorem HCPolySupport.HighContrast.physicalFullDualBesovVectorNorm_eq_scaleFactor_mul_normalized {d : ℕ} (Q : TriadicCube d) (s : ℝ) (F : Vec d → Vec d) : physicalFullDualBesovVectorNorm Q s F = physicalDualBesovScaleFactor Q s * Book.Ch03.scaleNormalizedDualNegativeBesovVectorNormTwo Q s F