High-contrast homogenization: Provider.Regularity.FiniteAffineAverageSlopeGoodTail

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

Finite affine average-slope control from a scalar good tail

The summable corrected weak-error row controls, uniformly in the outer scale, the average gradient of every finite zero-trace corrector on a fixed inner cube. Consequently the average full gradient of a finite affine solution is close to its boundary slope. This is the finite quantitative form of the normalized-slope uniqueness input in the Liouville endgame.

theorem HCPolySupport.HighContrast.exists_scalarIdentityGoodTailFiniteCorrectionGradientAverageConstant (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) : ∃ (C : ℝ) (c : ℝ), 0 < C ∧ 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), ‖cubeAverageVec (originCube d ↑q) (finiteAffineCorrection a (↑(q + t + 2)) e).grad‖ ≤ C * (1 + delta) * delta * euclideanNorm e

A scalar good tail uniformly controls the average gradient of a finite correction two or more scales outside a fixed centered cube.

theorem HCPolySupport.HighContrast.exists_scalarIdentityGoodTailFiniteAffineAverageSlopeConstant (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) : ∃ (C : ℝ) (c : ℝ), 0 < C ∧ 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 (cubeAverageVec (originCube d ↑q) (finiteAffineSolution a (↑(q + t + 2)) e).toH1.grad - e) ≤ C * (1 + delta) * delta * euclideanNorm e

The average full gradient of a finite affine solution is uniformly close to its boundary slope on every fixed inner cube at good-tail order.

theorem HCPolySupport.HighContrast.exists_scalarIdentityGoodTailFiniteAffineSlopeAverageCoercivityThreshold (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) : ∃ 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)

At a sufficiently small good tail, a finite affine boundary slope is controlled by the average gradient on any fixed admissible inner cube.