High-contrast homogenization: Provider.Regularity.LiouvilleTranslatedGradientIdentification

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

Translated-gradient identification from reverse Liouville classification

The reverse theorem classifies a translated affine-corrector pair using an initially unknown slope. Intrinsic normalization identifies that slope with the original one, after which the corrector gradients agree almost everywhere. The fixed-translation boundary cost is carried by the weak corrector row of the source carrier.

theorem HCPolySupport.HighContrast.exists_scalarIdentityGoodTailLiouvilleTranslatedGradientIdentificationConstant (d : ℕ) [NeZero d] (s theta : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) (htheta : theta < 1) : ∃ c ∈ Set.Ioo 0 1, ∀ (a : Book.Ch02.TriadicCoeffFamily d) (delta : ℝ) (n : ℤ), delta ∈ Set.Ioc 0 c → ScalarIdentityGoodTail a s delta n → ∀ (PhiTarget : Vec d → NormalizedLocalH1Carrier d), IsFiniteAffineCorrectionJointLocalEquation a PhiTarget → ∀ {b : CoeffField d}, IsAELocallyUniformlyElliptic b → (∀ (q : ℕ), Book.Ch03.publicCoeffField (originCube d ↑q) a =ᵐ[MeasureTheory.volume.restrict (localGradientCube d q)] b) → ∀ (PhiSource : NormalizedLocalH1Carrier d) (e t : Vec d) (sRow N : ℝ) (q0 : ℕ), 0 < sRow → sRow < 1 / 2 → HasIntrinsicNormalizedSlope e PhiSource → (∀ (e' : Vec d), HasIntrinsicNormalizedSlope e' (PhiTarget e')) → (∀ (q : ℕ), q0 ≤ q → (cubeScaleNormalizedDualNegativeBesovVectorNormTwo (originCube d ↑q) sRow fun (x : Vec d) => e + PhiSource.globalGradientRepresentative x) ≤ N) → ∀ {v : Vec d → ℝ}, (MemLiouvilleClass b theta v fun (x : Vec d) => e + PhiSource.globalGradientRepresentative (x + t)) → (fun (x : Vec d) => PhiSource.globalGradientRepresentative (x + t)) =ᵐ[MeasureTheory.volume] (PhiTarget e).globalGradientRepresentative

Under one small scalar good-tail threshold, reverse Liouville classification plus intrinsic normalization identifies a translated corrector gradient with the target joint family at the original slope.