High-contrast homogenization: Analytic.AffineFractionalKernel

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

Kernel distortion under an invertible linear change of variables

The Gagliardo double integral of e.physical.fractional.norm measures the increment of a field against the Euclidean distance between its two arguments. An invertible linear map distorts that distance by a factor lying between the extreme singular values of the map, and rescales the outer normalized average and the inner integral by the determinant.

This module records the ingredients the fractional comparison needs: the unnormalized Lebesgue integral over a linear image, the two singular-value bounds written through the ℓ² operator norm, and the pointwise comparison of the Gagliardo kernels before and after the change of variables.

The singular-value datum is carried abstractly, as a constant N satisfying |w| ≤ N |L w| for every w; the operator norm of L⁻¹ is always such a constant, and a sharper one may be substituted wherever it is known.

Unnormalized integrals over a linear image

theorem HCPolySupport.HighContrast.setLIntegral_matImage {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} (hU : MeasurableSet U) (f : Vec d → ENNReal) : ∫⁻ (x : Vec d) in matImage L U, f x = ENNReal.ofReal |Matrix.det L| * ∫⁻ (y : Vec d) in U, f (matVecMul L y)

The Lebesgue integral of a nonnegative function over an invertible linear image carries the determinant Jacobian.

Singular-value bounds through the ℓ² operator norm

theorem HCPolySupport.HighContrast.vecNormSq_matVecMul_le {d : ℕ} (M : Mat d) (x : Vec d) : vecNormSq (matVecMul M x) ≤ ‖M‖ ^ 2 * vecNormSq x

The ℓ² operator norm controls the squared length of a matrix-vector product.

theorem HCPolySupport.HighContrast.sqrt_vecNormSq_matVecMul_le {d : ℕ} (M : Mat d) (x : Vec d) : √(vecNormSq (matVecMul M x)) ≤ ‖M‖ * √(vecNormSq x)

The largest singular value bound. The Euclidean length of M x is at most the ℓ² operator norm of M times the Euclidean length of x.

theorem HCPolySupport.HighContrast.sqrt_vecNormSq_le_norm_inv_mul {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) (x : Vec d) : √(vecNormSq x) ≤ ‖L⁻¹‖ * √(vecNormSq (matVecMul L x))

The smallest singular value bound. For an invertible L the Euclidean length of x is at most the ℓ² operator norm of L⁻¹ times the Euclidean length of L x.

Elementary matrix-vector identities

theorem HCPolySupport.HighContrast.matVecMul_sub_vec {d : ℕ} (M : Mat d) (x y : Vec d) : matVecMul M x - matVecMul M y = matVecMul M (x - y)

A matrix acts linearly on differences.

theorem HCPolySupport.HighContrast.matVecMul_zero_vec {d : ℕ} (M : Mat d) : matVecMul M 0 = 0

A matrix sends the origin to the origin.

theorem HCPolySupport.HighContrast.sqrt_vecNormSq_matVecMul_eq_zero {d : ℕ} {M : Mat d} {w : Vec d} (h : √(vecNormSq w) = 0) : √(vecNormSq (matVecMul M w)) = 0

A linear map cannot separate a point from itself: a vanishing Euclidean length is preserved.

The pointwise kernel comparison

theorem HCPolySupport.HighContrast.gagliardo_kernel_matVecMul_le {d : ℕ} {L : Mat d} {N p : ℝ} (hN : 0 ≤ N) (hp : 0 ≤ p) (hker : ∀ (w : Vec d), √(vecNormSq w) ≤ N * √(vecNormSq (matVecMul L w))) {a : ℝ} (ha : 0 ≤ a) (w : Vec d) : a / √(vecNormSq (matVecMul L w)) ^ p ≤ N ^ p * (a / √(vecNormSq w) ^ p)

The Gagliardo kernel comparison. With |w| ≤ N |L w| the kernel written in the image variables is at most N ^ p times the kernel written in the source variables, for every nonnegative numerator.