High-contrast homogenization: Provider.Regularity.LiouvilleFixedCubeExcess

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

Vanishing finite affine excess on a fixed cube

This module aligns the two-scale Caccioppoli output with the outer scale of finite-excess decay by restricting the exact realization on Q_(q+2) to Q_q. The restricted solutions still represent the frozen global pair exactly, and their excess on every fixed cube tends to zero.

theorem HCPolySupport.HighContrast.exists_scalarIdentityLiouvilleFiniteTopEnergyGrowth (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) (a : Book.Ch02.TriadicCoeffFamily d) (delta : ℝ) (n : ℤ) (hdelta : delta ≤ 1) (hgood : ScalarIdentityGoodTail a s delta n) {b : CoeffField d} {theta : ℝ} (hb : IsAELocallyUniformlyElliptic b) (hcoeff : ∀ (q : ℕ), Book.Ch03.publicCoeffField (originCube d ↑q) a =ᵐ[volumeMeasureOn (openCubeSet (originCube d ↑q))] b) {v : Vec d → ℝ} {Dv : Vec d → Vec d} (hv : MemLiouvilleClass b theta v Dv) : ∃ (u : (q : ℕ) → Book.Ch03.CubeSolution (originCube d (↑q - 2)) a), (∀ (q : ℕ), (u q).toH1.toFun = v ∧ (u q).toH1.grad = Dv) ∧ Filter.Tendsto (fun (q : ℕ) => ENNReal.ofReal (Real.rpow 3 (-theta * ↑q) * Book.Ch03.h1EnergyNormOnCube (originCube d (↑q - 2)) a (u q).toH1)) Filter.atTop (nhds 0)

Restricting the exact realization on Q_q to Q_(q-2) converts the two-scale Caccioppoli growth estimate into a top-scale energy estimate.

theorem HCPolySupport.HighContrast.tendsto_fixedFiniteAffineGradientExcess_of_realRate {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) {theta eta Cdec : ℝ} (hCdec : 0 ≤ Cdec) (heta : theta < eta) (k : ℤ) (u : (q : ℕ) → Book.Ch03.CubeSolution (originCube d (↑q - 2)) a) (hgrowth : Filter.Tendsto (fun (q : ℕ) => ENNReal.ofReal (Real.rpow 3 (-theta * ↑q) * Book.Ch03.h1EnergyNormOnCube (originCube d (↑q - 2)) a (u q).toH1)) Filter.atTop (nhds 0)) (hrate : ∀ᶠ (q : ℕ) in Filter.atTop, finiteAffineGradientExcess a k (↑q - 2) (u q) ≤ ENNReal.ofReal (Cdec * Real.rpow 3 (-eta * ↑(↑q - 2 - k))) * finiteAffineGradientExcess a (↑q - 2) (↑q - 2) (u q)) : Filter.Tendsto (fun (q : ℕ) => finiteAffineGradientExcess a k (↑q - 2) (u q)) Filter.atTop (nhds 0)

A real-rate excess estimate with exponent strictly above the energy-growth exponent forces the excess on a fixed cube to vanish.

theorem HCPolySupport.HighContrast.exists_scalarIdentityLiouvilleFixedCubeExcessVanishingConstants (d : ℕ) [NeZero d] (s theta : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) (htheta : theta < 1) : ∃ (eta : ℝ) (Cfamily : ℝ) (c : ℝ) (Cdec : ℝ), max theta (1 / 2) < eta ∧ eta < 1 ∧ 1 ≤ Cfamily ∧ c ∈ Set.Ioo 0 1 ∧ 0 < Cdec ∧ ∀ (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 → ∃ (u : (q : ℕ) → Book.Ch03.CubeSolution (originCube d (↑q - 2)) a), (∀ (q : ℕ), (u q).toH1.toFun = v ∧ (u q).toH1.grad = Dv) ∧ ∀ (k : ℤ), n ≤ k → Filter.Tendsto (fun (q : ℕ) => finiteAffineGradientExcess a k (↑q - 2) (u q)) Filter.atTop (nhds 0)

Good-tail finite regularity and Liouville growth jointly produce exact finite realizations whose affine-gradient excess vanishes on every fixed centered cube beyond the good-tail base.