Documentation

LeanPool.HighContrastHomogenization.Provider.Response.AdaptedWeakProduct

High-contrast homogenization: Provider.Response.AdaptedWeakProduct #

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

Separate affine distortions for the weak product #

The gradient and flux slots of the reference-cube div--curl estimate are transported separately. For a rounded grid the scalar normalization of the metric square root appears reciprocally in the two slots and cancels in their product.

source
theorem HCPolySupport.HighContrast.Response.roundedGrid_metricFrobenius_product_le {d : ℕ} [NeZero d] {l : ℤ} (hl : ↑(kZero d) ≤ l) {m : Mat d} (hm : Matrix.PosDef m) :
√(Book.Ch02.matrixFrobeniusNormSq (matTranspose (roundedGrid l m) * (matSqrt m)⁻¹)) * √(Book.Ch02.matrixFrobeniusNormSq ((roundedGrid l m)⁻¹ * matSqrt m)) ≤ 51 / 50 * ↑d ^ 2

The product of the two metric-slot Frobenius distortions is bounded only by the dimension when the grid is the rounded normalized metric root.

source
theorem HCPolySupport.HighContrast.Response.ofReal_partialSeminorm_metricPullback_fst_le_separate {d : ℕ} {q S : Mat d} (hq : Matrix.PosDef q) (hS : Matrix.PosDef S) (t : ℤ) (s : ℝ) (N : ℕ) (F : Vec d → BlockVec d) (hF₁ : MemVectorL2 (adaptedCell q t) fun (x : Vec d) => matVecMul S (F x).1) (hF₂ : MemVectorL2 (adaptedCell q t) fun (x : Vec d) => matVecMul S⁻¹ (F x).2) :
ENNReal.ofReal (cubeBesovNegativeVectorPartialSeminorm (originCube d t) s N fun (y : Vec d) => matVecMul (matTranspose q) (F (matVecMul q y)).1) ≤ ENNReal.ofReal (3 ^ (-(s * ↑t))) * ENNReal.ofReal √(Book.Ch02.matrixFrobeniusNormSq (matTranspose q * S⁻¹)) * adaptedWeakSeminorm q t s fun (x : Vec d) => (matVecMul S (F x).1, matVecMul S⁻¹ (F x).2)

The gradient partial seminorm uses only the first affine distortion.

source
theorem HCPolySupport.HighContrast.Response.ofReal_partialSeminorm_metricPullback_snd_le_separate {d : ℕ} {q S : Mat d} (hq : Matrix.PosDef q) (hS : Matrix.PosDef S) (t : ℤ) (s : ℝ) (N : ℕ) (F : Vec d → BlockVec d) (hF₁ : MemVectorL2 (adaptedCell q t) fun (x : Vec d) => matVecMul S (F x).1) (hF₂ : MemVectorL2 (adaptedCell q t) fun (x : Vec d) => matVecMul S⁻¹ (F x).2) :
ENNReal.ofReal (cubeBesovNegativeVectorPartialSeminorm (originCube d t) s N fun (y : Vec d) => matVecMul q⁻¹ (F (matVecMul q y)).2) ≤ ENNReal.ofReal (3 ^ (-(s * ↑t))) * ENNReal.ofReal √(Book.Ch02.matrixFrobeniusNormSq (q⁻¹ * S)) * adaptedWeakSeminorm q t s fun (x : Vec d) => (matVecMul S (F x).1, matVecMul S⁻¹ (F x).2)

The flux partial seminorm uses only the second affine distortion.