High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Corrector.PhysicalLiouvilleDoubleInclusion

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

Physical Liouville double inclusion

The scalar normalized classification is transported through the exact normalized-root gauge while retaining the same physical corrector family.

theorem HCPolySupport.HighContrast.Root.CanonicalPullbackCorrectorFamily.physicalLiouvilleDoubleInclusion {d : ℕ} [NeZero d] {GoodScale : Mat d → CoeffSpace d → ℝ → Prop} {abar : Mat d} {Phi : Vec d → CoeffSpace d → Vec d → ℝ} {gradPhi : Vec d → CoeffSpace d → Vec d → Vec d} (hfamily : CanonicalPullbackCorrectorFamily GoodScale abar Phi gradPhi) (a : CoeffSpace d) (x : ℝ) (hgood : GoodScale abar a x) (theta : ℝ) : theta ∈ Set.Ioo 0 1 → (∀ (v : Vec d → ℝ) (Dv : Vec d → Vec d), MemLiouvilleClass (fun (y : Vec d) => ↑↑a y) theta v Dv → ∃ (e : Vec d) (c : ℝ), v =ᵐ[MeasureTheory.volume] fun (y : Vec d) => vecDot e y + Phi e a y + c) ∧ ∀ (e : Vec d) (c : ℝ), MemLiouvilleClass (fun (y : Vec d) => ↑↑a y) theta (fun (y : Vec d) => vecDot e y + Phi e a y + c) fun (y : Vec d) => e + gradPhi e a y

A canonical physical corrector family satisfies the full two-sided Liouville classification on every certified sample.