High-contrast homogenization: Provider.Regularity.LiouvilleSlopeCompactness

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

Compactness of finite affine slopes in the Liouville endgame

This module converts vanishing weighted affine residuals on one fixed cube into vanishing residual-gradient averages. Combined with the small-tail average-slope coercivity estimate, this is the local compactness input for selecting a limiting Liouville slope.

theorem HCPolySupport.HighContrast.exists_boundarySlopeSequence_residual_tendsto_zero {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (n : ℤ) (m : ℕ → ℤ) (hm : ∀ (q : ℕ), n ≤ m q) (u : (q : ℕ) → Book.Ch03.CubeSolution (originCube d (m q)) a) (hexcess : Filter.Tendsto (fun (q : ℕ) => finiteAffineGradientExcess a n (m q) (u q)) Filter.atTop (nhds 0)) : ∃ (e : ℕ → Vec d), Filter.Tendsto (fun (q : ℕ) => weightedGradNorm (a.coeffOn (originCube d n)).toCoeffField (openCubeSet (originCube d n)) fun (x : Vec d) => (u q).toH1.grad x - (finiteAffineSolution a (m q) (e q)).toH1.grad x) Filter.atTop (nhds 0)

Vanishing finite affine excess admits boundary slopes whose actual weighted residuals vanish, without assuming attainment of the infimum.

theorem HCPolySupport.HighContrast.tendsto_finiteAffineGradientResidual_localGradient_zero {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (n : ℕ) (m : ℕ → ℤ) (hm : ∀ (j : ℕ), ↑n ≤ m j) (u : (j : ℕ) → Book.Ch03.CubeSolution (originCube d (m j)) a) (e : ℕ → Vec d) (hresidual : Filter.Tendsto (fun (j : ℕ) => weightedGradNorm (a.coeffOn (originCube d ↑n)).toCoeffField (openCubeSet (originCube d ↑n)) fun (x : Vec d) => (u j).toH1.grad x - (finiteAffineSolution a (m j) (e j)).toH1.grad x) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (j : ℕ) => (finiteAffineGradientResidual a ⋯ (u j) (e j)).toH1.gradToHilbertVectorL2) Filter.atTop (nhds 0)

Vanishing weighted finite-affine residuals on a fixed cube force their local Hilbert-gradient classes to converge to zero.

theorem HCPolySupport.HighContrast.tendsto_finiteAffineGradientResidual_cubeAverageVec_zero {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (n : ℕ) (m : ℕ → ℤ) (hm : ∀ (j : ℕ), ↑n ≤ m j) (u : (j : ℕ) → Book.Ch03.CubeSolution (originCube d (m j)) a) (e : ℕ → Vec d) (hresidual : Filter.Tendsto (fun (j : ℕ) => weightedGradNorm (a.coeffOn (originCube d ↑n)).toCoeffField (openCubeSet (originCube d ↑n)) fun (x : Vec d) => (u j).toH1.grad x - (finiteAffineSolution a (m j) (e j)).toH1.grad x) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (j : ℕ) => cubeAverageVec (originCube d ↑n) (finiteAffineGradientResidual a ⋯ (u j) (e j)).toH1.grad) Filter.atTop (nhds 0)

Vanishing weighted finite-affine residuals on a fixed cube force the ordinary averages of their gradients to vanish.

theorem HCPolySupport.HighContrast.exists_uniform_euclideanBound_finiteAffineSlopes_of_residual_tendsto_zero {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)) (hdelta : delta ∈ Set.Ioc 0 c) (hgood : ScalarIdentityGoodTail a s delta n₀) (n : ℕ) (hn : n₀ ≤ ↑n) (u : (j : ℕ) → Book.Ch03.CubeSolution (originCube d ↑(n + j + 2)) a) (Dv : Vec d → Vec d) (huGrad : ∀ (j : ℕ), (u j).toH1.grad = Dv) (e : ℕ → Vec d) (hresidual : Filter.Tendsto (fun (j : ℕ) => weightedGradNorm (a.coeffOn (originCube d ↑n)).toCoeffField (openCubeSet (originCube d ↑n)) fun (x : Vec d) => (u j).toH1.grad x - (finiteAffineSolution a (↑(n + j + 2)) (e j)).toH1.grad x) Filter.atTop (nhds 0)) : ∃ (R : ℝ), ∀ (j : ℕ), euclideanNorm (e j) ≤ R

If exact realizations of one global gradient admit finite-affine approximants with vanishing residual on a fixed cube, then their boundary slopes are uniformly bounded under the small good-tail threshold.

theorem HCPolySupport.HighContrast.exists_tendsto_subsequence_of_uniform_euclideanBound {d : ℕ} (e : ℕ → Vec d) (hbound : ∃ (R : ℝ), ∀ (j : ℕ), euclideanNorm (e j) ≤ R) : ∃ (eLim : Vec d) (φ : ℕ → ℕ), StrictMono φ ∧ Filter.Tendsto (e ∘ φ) Filter.atTop (nhds eLim)

A sequence of project vectors with a uniform explicit Euclidean bound has a convergent subsequence in the native project-vector topology.