High-contrast homogenization: Provider.Regularity.LiouvilleReverseClassification

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

Reverse Liouville classification

This module composes fixed-cube excess vanishing, compact slope selection, canonical slope compatibility, and additive-gauge recovery.

theorem HCPolySupport.HighContrast.exists_affineCorrectorRepresentation_of_liouvilleFixedCubeExcess {d : ℕ} [NeZero d] {s : ℝ} {a : Book.Ch02.TriadicCoeffFamily d} {delta c : ℝ} {n : ℤ} (hthreshold : c ∈ Set.Ioo 0 1 ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (delta : ℝ) (n : ℤ), delta ∈ Set.Ioc 0 c → ScalarIdentityGoodTail a s delta n → ∀ (q t : ℕ), n ≤ ↑q → ∀ (e : Vec d), euclideanNorm e ≤ 2 * euclideanNorm (cubeAverageVec (originCube d ↑q) (finiteAffineSolution a (↑(q + t + 2)) e).toH1.grad)) (hcoercive : ∀ (hCauchy : FiniteAffineCorrectionLocalCauchy a) (e : Vec d) (q : ℕ), n ≤ ↑q → euclideanNorm e ≤ 2 * euclideanNorm (localGradientClassAverage ((have this := constantGradientOnOriginCube e ↑q; this) + (finiteAffineCorrectionJointLocalLimit a hCauchy e).gradientComponent q))) (hdelta : delta ∈ Set.Ioc 0 c) (hgood : ScalarIdentityGoodTail a s delta n) (hCauchy : FiniteAffineCorrectionLocalCauchy a) (u : (p : ℕ) → Book.Ch03.CubeSolution (originCube d (↑p - 2)) a) (v : Vec d → ℝ) (Dv : Vec d → Vec d) (hu : ∀ (p : ℕ), (u p).toH1.toFun = v ∧ (u p).toH1.grad = Dv) (hexcess : ∀ (k : ℤ), n ≤ k → Filter.Tendsto (fun (p : ℕ) => finiteAffineGradientExcess a k (↑p - 2) (u p)) Filter.atTop (nhds 0)) : ∃ (e : Vec d) (c₀ : ℝ), v =ᵐ[MeasureTheory.volume] fun (x : Vec d) => vecDot e x + (finiteAffineCorrectionJointLocalLimit a hCauchy e).globalValueRepresentative x + c₀

Deterministic composition of the global-slope and additive-constant engines.

theorem HCPolySupport.HighContrast.exists_scalarIdentityGoodTailLiouvilleReverseConstant (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 =ᵐ[volumeMeasureOn (openCubeSet (originCube d ↑q))] b) → ∀ {v : Vec d → ℝ} {Dv : Vec d → Vec d}, MemLiouvilleClass b theta v Dv → ∃ (hCauchy : FiniteAffineCorrectionLocalCauchy a) (e : Vec d) (c₀ : ℝ), v =ᵐ[MeasureTheory.volume] fun (x : Vec d) => vecDot e x + (finiteAffineCorrectionJointLocalLimit a hCauchy e).globalValueRepresentative x + c₀

Quantitative reverse Liouville classification under one sufficiently small scalar good-tail threshold.

theorem HCPolySupport.HighContrast.exists_scalarIdentityGoodTailLiouvilleReverseForJointEquationConstant (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 =ᵐ[volumeMeasureOn (openCubeSet (originCube d ↑q))] b) → ∀ {v : Vec d → ℝ} {Dv : Vec d → Vec d}, MemLiouvilleClass b theta v Dv → ∃ (e : Vec d) (c₀ : ℝ), v =ᵐ[MeasureTheory.volume] fun (x : Vec d) => vecDot e x + (Phi e).globalValueRepresentative x + c₀

Reverse classification stated for any joint corrector family satisfying the frozen local-limit/equation predicate.