High-contrast homogenization: Provider.Regularity.CorrectorRealRadiusNegOne

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

Quotient-safe negative-one restriction to centered real cubes

This module restricts a Hilbert-vector L² class from an outer domain to a measurable subdomain and compares the normalized negative-one dual norms. A compactly supported test on the inner domain is also a test on the outer domain. Exact support identities for its value and gradient energies produce the inner-to-outer volume ratio in the squared test norm, hence the square root of the reciprocal ratio in the dual norm.

The final specialization uses the canonical real-radius origin cube from CorrectorRealRadiusGeometry. No corrector decay or tail estimate is used.

Restriction of local Hilbert-vector classes

noncomputable def HCPolySupport.HighContrast.localHilbertVectorL2RestrictLinear {d : ℕ} {U V : Set (Vec d)} (hUV : U ⊆ V) : ↥(HilbertVectorL2 V) →ₗ[ℝ] ↥(HilbertVectorL2 U)

The real linear restriction map for Hilbert-vector L² classes along the inclusion U ⊆ V.

Equations

• HCPolySupport.HighContrast.localHilbertVectorL2RestrictLinear hUV = { toFun := fun (F : ↥(HCPolySupport.HilbertVectorL2 V)) => MeasureTheory.MemLp.toLp ↑↑F ⋯, map_add' := ⋯, map_smul' := ⋯ }

theorem HCPolySupport.HighContrast.localHilbertVectorL2RestrictLinear_norm_le {d : ℕ} {U V : Set (Vec d)} (hUV : U ⊆ V) (F : ↥(HilbertVectorL2 V)) : ‖(localHilbertVectorL2RestrictLinear hUV) F‖ ≤ ‖F‖

noncomputable def HCPolySupport.HighContrast.localHilbertVectorL2Restrict {d : ℕ} {U V : Set (Vec d)} (hUV : U ⊆ V) : ↥(HilbertVectorL2 V) →L[ℝ] ↥(HilbertVectorL2 U)

Continuous restriction of a Hilbert-vector L² class to an arbitrary set contained in its original domain.

Equations

• HCPolySupport.HighContrast.localHilbertVectorL2Restrict hUV = (HCPolySupport.HighContrast.localHilbertVectorL2RestrictLinear hUV).mkContinuous 1 ⋯

theorem HCPolySupport.HighContrast.localHilbertVectorL2Restrict_coeFn_ae {d : ℕ} {U V : Set (Vec d)} (hUV : U ⊆ V) (F : ↥(HilbertVectorL2 V)) : ↑↑((localHilbertVectorL2Restrict hUV) F) =ᵐ[volumeMeasureOn U] ↑↑F

Local Hilbert-vector restriction agrees almost everywhere with the outer representative on the inner domain.

Compact support and normalized test energies

theorem HCPolySupport.HighContrast.IsLocalVecTest.mono_set {d : ℕ} {U V : Set (Vec d)} {psi : Vec d → Vec d} (hpsi : IsLocalVecTest U psi) (hUV : U ⊆ V) : IsLocalVecTest V psi

A local vector test remains a local test after enlarging its domain.

theorem HCPolySupport.HighContrast.h1NormSq_outer_le_volumeRatio_mul {d : ℕ} [NeZero d] {U V : Set (Vec d)} (hUV : U ⊆ V) (hU0 : MeasureTheory.volume U ≠ 0) (hUtop : MeasureTheory.volume U ≠ ⊤) (hV0 : MeasureTheory.volume V ≠ 0) (hVtop : MeasureTheory.volume V ≠ ⊤) {psi : Vec d → Vec d} (hpsi : IsLocalVecTest U psi) : h1NormSq V psi ≤ MeasureTheory.volume U / MeasureTheory.volume V * h1NormSq U psi

Enlarging the domain decreases the normalized squared H¹ test norm by at least the inner-to-outer volume ratio for a test supported in the inner domain.

The normalized negative-one restriction

theorem HCPolySupport.HighContrast.dualPairing_le_negOneNorm_of_h1NormSq_le {d : ℕ} {V : Set (Vec d)} (F psi : Vec d → Vec d) {K : ℝ} (hK : 0 < K) (htest : IsLocalVecTest V psi) (hnorm : h1NormSq V psi ≤ ENNReal.ofReal K) : dualPairing V F psi ≤ ENNReal.ofReal √K * negOneNorm V F

A local test whose squared H¹ norm is at most K pairs by at most sqrt K times the negative-one norm.

theorem HCPolySupport.HighContrast.negOneNorm_le_sqrt_volumeRatio_of_subset {d : ℕ} [NeZero d] {U V : Set (Vec d)} (hUV : U ⊆ V) (hU0 : MeasureTheory.volume U ≠ 0) (hUtop : MeasureTheory.volume U ≠ ⊤) (hV0 : MeasureTheory.volume V ≠ 0) (hVtop : MeasureTheory.volume V ≠ ⊤) (F : Vec d → Vec d) (hF : MemVectorL2 V F) : negOneNorm U F ≤ ENNReal.ofReal √((MeasureTheory.volume V).toReal / (MeasureTheory.volume U).toReal) * negOneNorm V F

A raw local L² field restricted from V to U has normalized negative-one norm at most the square root of the outer-to-inner volume ratio times its outer norm.

theorem HCPolySupport.HighContrast.localNegOneNorm_restrict_le_sqrt_volumeRatio {d : ℕ} [NeZero d] {U V : Set (Vec d)} (hUV : U ⊆ V) (hU0 : MeasureTheory.volume U ≠ 0) (hUtop : MeasureTheory.volume U ≠ ⊤) (hV0 : MeasureTheory.volume V ≠ 0) (hVtop : MeasureTheory.volume V ≠ ⊤) (F : ↥(HilbertVectorL2 V)) : localNegOneNorm U ((localHilbertVectorL2Restrict hUV) F) ≤ ENNReal.ofReal √((MeasureTheory.volume V).toReal / (MeasureTheory.volume U).toReal) * localNegOneNorm V F

Quotient-safe restriction of a local Hilbert-vector class costs the same square-root volume ratio in the normalized negative-one norm.

Canonical centered-real-cube specialization