High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Corrector.LiouvillePrivateThresholdFixedFamily

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

Private Liouville restart for a fixed joint corrector family

Restarting the summable error tail changes only its first index. The unique joint corrector limit already retained by the physical family is therefore kept fixed throughout the two inclusions.

theorem HCPolySupport.HighContrast.Root.scalarIdentityGoodTail_liouvilleDoubleInclusion_fixedFamily_after_restart (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) {b : CoeffField d} (hb : IsAELocallyUniformlyElliptic b) (a : Book.Ch02.TriadicCoeffFamily d) (delta : ℝ) (n : ℤ) (hgood : ScalarIdentityGoodTail a s delta n) (hcoeff : ∀ (q : ℕ), Book.Ch03.publicCoeffField (originCube d ↑q) a =ᵐ[volumeMeasureOn (localGradientCube d q)] b) (hCauchy : FiniteAffineCorrectionLocalCauchy a) (hPhi : IsFiniteAffineCorrectionJointLocalEquation a (finiteAffineCorrectionJointLocalLimit a hCauchy)) (theta : ℝ) : theta ∈ Set.Ioo 0 1 → (∀ {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 + (finiteAffineCorrectionJointLocalLimit a hCauchy e).globalValueRepresentative x + c₀) ∧ ∀ (e : Vec d) (c₀ : ℝ), MemLiouvilleClass b theta (fun (x : Vec d) => vecDot e x + (finiteAffineCorrectionJointLocalLimit a hCauchy e).globalValueRepresentative x + c₀) fun (x : Vec d) => e + (finiteAffineCorrectionJointLocalLimit a hCauchy e).globalGradientRepresentative x

The private threshold restart supplies both scalar Liouville inclusions for the particular joint corrector family supplied by the root.