High-contrast homogenization: Analytic.AffineFractionalNorm

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

The normalized fractional norm under an invertible affine normalization

The fractional carriers of e.physical.fractional.norm are compared across the change of variables x = L y for an invertible matrix L. Two mechanisms are separated:

• the domain transport, which sends the domain V to its linear image and the field to its pullback. The volume-normalized L² term acquires exactly the determinant power |det L| ^ (-2s/d), while the Gagliardo term acquires the determinant factor of the inner integral together with the distortion of the kernel, controlled by the extreme singular values of L;
• the pointwise action, which multiplies the values of the field by a fixed matrix. This costs the squared ℓ² operator norm of that matrix and leaves the domain untouched.

Both comparisons are two-sided: the reverse inequality of the domain transport is the forward inequality for L⁻¹, and its constant is written explicitly through |det L|⁻¹ and the operator norm of L. Every constant depends only on the dimension, on the fractional parameter, and on the transporting matrix.

Monotonicity of the normalized average

theorem HCPolySupport.HighContrast.eVolumeAverage_mono {d : ℕ} (V : Set (Vec d)) {f g : Vec d → ENNReal} (h : ∀ (x : Vec d), f x ≤ g x) : eVolumeAverage V f ≤ eVolumeAverage V g

The normalized nonnegative average is monotone.

theorem HCPolySupport.HighContrast.eVolumeAverage_le_const_mul {d : ℕ} (V : Set (Vec d)) {a : ENNReal} (ha : a ≠ ⊤) {f g : Vec d → ENNReal} (h : ∀ (x : Vec d), f x ≤ a * g x) : eVolumeAverage V f ≤ a * eVolumeAverage V g

A pointwise bound by a finite constant multiple passes to the normalized average.

Linear images of the whole space

theorem HCPolySupport.HighContrast.measurableSet_matImage {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} (hU : MeasurableSet U) : MeasurableSet (matImage L U)

An invertible linear image of a measurable set is measurable.

theorem HCPolySupport.HighContrast.volume_matImage_ne_zero {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} (hU0 : MeasureTheory.volume U ≠ 0) : MeasureTheory.volume (matImage L U) ≠ 0

An invertible linear image of a set of positive volume has positive volume.

The Gagliardo term under a pointwise bound on increments

theorem HCPolySupport.HighContrast.fracSeminormSq_mono_of_le {d : ℕ} (V : Set (Vec d)) (s : ℝ) {c : ℝ} (hc : 0 ≤ c) {F G : Vec d → Vec d} (h : ∀ (x y : Vec d), vecNormSq (F x - F y) ≤ c * vecNormSq (G x - G y)) : fracSeminormSq V s F ≤ ENNReal.ofReal c * fracSeminormSq V s G

A pointwise comparison of increments passes to the Gagliardo double integral.

The domain transport

theorem HCPolySupport.HighContrast.fracSeminormSq_matImage_le {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} (hU : MeasurableSet U) {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) : fracSeminormSq (matImage L U) s F ≤ ENNReal.ofReal (|Matrix.det L| * N ^ (↑d + 2 * s)) * fracSeminormSq U s fun (y : Vec d) => F (matVecMul L y)

The Gagliardo term under an invertible change of variables. The determinant of the inner integral and the kernel distortion N ^ (d + 2s) are the only losses, where N is any constant with |w| ≤ N |L w|.

theorem HCPolySupport.HighContrast.l2Term_matImage {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} (hU : MeasurableSet U) (hU0 : MeasureTheory.volume U ≠ 0) (s : ℝ) (F : Vec d → Vec d) : (MeasureTheory.volume (matImage L U) ^ (-(2 * s) / ↑d) * eVolumeAverage (matImage L U) fun (x : Vec d) => ENNReal.ofReal (vecNormSq (F x))) = ENNReal.ofReal (|Matrix.det L| ^ (-(2 * s) / ↑d)) * (MeasureTheory.volume U ^ (-(2 * s) / ↑d) * eVolumeAverage U fun (y : Vec d) => ENNReal.ofReal (vecNormSq (F (matVecMul L y))))

The normalized L² term of the fractional norm square rescales by a pure determinant power under an invertible change of variables.

noncomputable def HCPolySupport.HighContrast.hsAffineFactor {d : ℕ} (L : Mat d) (s N : ℝ) : ℝ

The affine distortion factor of the normalized H^s norm square: the larger of the determinant power seen by the L² term and the determinant-times-kernel factor seen by the Gagliardo term.

Equations

• HCPolySupport.HighContrast.hsAffineFactor L s N = max (|Matrix.det L| ^ (-(2 * s) / ↑d)) (|Matrix.det L| * N ^ (↑d + 2 * s))

theorem HCPolySupport.HighContrast.hsAffineFactor_pos {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) (s N : ℝ) : 0 < hsAffineFactor L s N

The affine distortion factor is positive for an invertible matrix.

theorem HCPolySupport.HighContrast.hsNormSq_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) : hsNormSq (matImage L U) s F ≤ ENNReal.ofReal (hsAffineFactor L s N) * hsNormSq U s fun (y : Vec d) => F (matVecMul L y)

The normalized H^s norm square under an invertible change of variables. The constant is the affine distortion factor built from the determinant of L and from any constant N with |w| ≤ N |L w|.

theorem HCPolySupport.HighContrast.hsNormSq_comp_matVecMul_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) : (hsNormSq U s fun (y : Vec d) => F (matVecMul L y)) ≤ ENNReal.ofReal (hsAffineFactor L⁻¹ s N) * hsNormSq (matImage L U) s F

The reverse comparison. The pullback of a field to the source domain is controlled by the field on the image, with the distortion factor of the inverse map.

The operator-norm instantiations

theorem HCPolySupport.HighContrast.hsNormSq_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) : hsNormSq (matImage L U) s F ≤ ENNReal.ofReal (hsAffineFactor L s ‖L⁻¹‖) * hsNormSq U s fun (y : Vec d) => F (matVecMul L y)

The change-of-variables comparison with the explicit constant built from the determinant of L and the ℓ² operator norm of L⁻¹.

The pointwise matrix action on field values

theorem HCPolySupport.HighContrast.fracSeminormSq_matVecMul_le {d : ℕ} (M : Mat d) (V : Set (Vec d)) (s : ℝ) (F : Vec d → Vec d) : (fracSeminormSq V s fun (x : Vec d) => matVecMul M (F x)) ≤ ENNReal.ofReal (‖M‖ ^ 2) * fracSeminormSq V s F

Multiplying the values of a field by a fixed matrix costs the squared ℓ² operator norm of that matrix in the Gagliardo term.

theorem HCPolySupport.HighContrast.hsNormSq_matVecMul_le {d : ℕ} (M : Mat d) (V : Set (Vec d)) (s : ℝ) (F : Vec d → Vec d) : (hsNormSq V s fun (x : Vec d) => matVecMul M (F x)) ≤ ENNReal.ofReal (‖M‖ ^ 2) * hsNormSq V s F

The pointwise matrix action on the normalized H^s norm square. The domain is untouched; the cost is the squared ℓ² operator norm.