High-contrast homogenization: Analytic.AffineNegSobolevNorm

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

The negative fractional norm under an invertible affine normalization

The dual norm of e.physical.negative.norm is a supremum of normalized pairings over the smooth compactly supported fields of unit H^s norm. Under an invertible change of variables the pairing itself is unchanged — the determinant cancels from a normalized average — and the admissible index family is transported by pullback, at the cost of the affine distortion factor of the H^s norm square. Because the norm square is quadratic and the pairing is linear in the test, the dual norm therefore costs the square root of that factor.

The same rescaling argument gives the cost of multiplying the values of a field by a fixed matrix: the matrix moves onto the test field through its transpose, so the dual norm costs one power of the ℓ² operator norm of the transpose.

Rescaling an admissible test

theorem HCPolySupport.HighContrast.IsLocalVecTest.const_smul {d : ℕ} {V : Set (Vec d)} {ψ : Vec d → Vec d} (h : IsLocalVecTest V ψ) (c : ℝ) : IsLocalVecTest V fun (x : Vec d) => c • ψ x

A scalar multiple of a local vector test is a local vector test.

theorem HCPolySupport.HighContrast.dualPairing_const_smul {d : ℕ} (V : Set (Vec d)) (F ψ : Vec d → Vec d) {c : ℝ} (hc : 0 < c) : (dualPairing V F fun (x : Vec d) => c • ψ x) = ENNReal.ofReal c * dualPairing V F ψ

The normalized pairing is homogeneous of degree one in the test field.

theorem HCPolySupport.HighContrast.dualPairing_le_negSobolevNorm_of_hsNormSq_le {d : ℕ} {V : Set (Vec d)} {s : ℝ} (F ψ : Vec d → Vec d) {K : ℝ} (hK : 0 < K) (htest : IsLocalVecTest V ψ) (hnorm : hsNormSq V s ψ ≤ ENNReal.ofReal K) : dualPairing V F ψ ≤ ENNReal.ofReal √K * negSobolevNorm V s F

The rescaling bound. A local vector test whose H^s norm square is at most K pairs against a field by at most √K times the dual norm.

The domain transport

theorem HCPolySupport.HighContrast.negSobolevNorm_matImage_le {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} (hU : MeasurableSet U) (hU0 : MeasureTheory.volume U ≠ 0) {s N : ℝ} (hs : 0 ≤ ↑d + 2 * s) (hN : 0 ≤ N) (hker : ∀ (w : Vec d), √(vecNormSq w) ≤ N * √(vecNormSq (matVecMul L⁻¹ w))) (F : Vec d → Vec d) : negSobolevNorm (matImage L U) s F ≤ ENNReal.ofReal √(hsAffineFactor L⁻¹ s N) * negSobolevNorm U s fun (y : Vec d) => F (matVecMul L y)

The dual fractional norm under an invertible change of variables. The constant is the square root of the affine distortion factor of the inverse map.

The operator-norm instantiations

theorem HCPolySupport.HighContrast.negSobolevNorm_matImage_le_opNorm {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} (hU : MeasurableSet U) (hU0 : MeasureTheory.volume U ≠ 0) {s : ℝ} (hs : 0 ≤ ↑d + 2 * s) (F : Vec d → Vec d) : negSobolevNorm (matImage L U) s F ≤ ENNReal.ofReal √(hsAffineFactor L⁻¹ s ‖L‖) * negSobolevNorm U s fun (y : Vec d) => F (matVecMul L y)

The dual comparison with the explicit constant built from the determinant of L and the ℓ² operator norm of L.

The pointwise matrix action on field values