High-contrast homogenization: Provider.Regularity.LiouvilleReverseValueGradient

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

Reverse Liouville classification with gradient readout

The available reverse theorem identifies the scalar representative. Uniformly elliptic weak-gradient uniqueness upgrades that result to the global gradient identity needed by phase covariance.

theorem HCPolySupport.HighContrast.exists_scalarIdentityGoodTailLiouvilleReverseValueGradientForJointEquationConstant (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 → ∀ (Phi : Vec d → NormalizedLocalH1Carrier d), IsFiniteAffineCorrectionJointLocalEquation a Phi → ∀ {b : CoeffField d}, IsAELocallyUniformlyElliptic b → (∀ (q : ℕ), Book.Ch03.publicCoeffField (originCube d ↑q) a =ᵐ[MeasureTheory.volume.restrict (localGradientCube d q)] b) → ∀ {v : Vec d → ℝ} {Dv : Vec d → Vec d}, MemLiouvilleClass b theta v Dv → ∃ (e : Vec d) (c0 : ℝ), (v =ᵐ[MeasureTheory.volume] fun (x : Vec d) => vecDot e x + (Phi e).globalValueRepresentative x + c0) ∧ Dv =ᵐ[MeasureTheory.volume] fun (x : Vec d) => e + (Phi e).globalGradientRepresentative x

Reverse Liouville classification for a joint corrector family, augmented with the globally almost-everywhere gradient identity.