High-contrast homogenization: Provider.Regularity.FiniteLipschitz

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

Finite large-scale Lipschitz estimate on centered cubes

The comparison coefficient is the identity matrix and every spatial domain is a centered Euclidean triadic cube.

theorem HCPolySupport.HighContrast.exists_scalarIdentityFiniteLipschitzConstant (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) : ∃ (C : ℝ) (c : ℝ), 1 ≤ C ∧ c ∈ Set.Ioo 0 1 ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (n m : ℤ), n < m → ScalarIdentityGoodTailOnInterval a s c n m → ∀ (u : Book.Ch03.CubeSolution (originCube d m) a), weightedGradNorm (a.coeffOn (originCube d n)).toCoeffField (openCubeSet (originCube d n)) u.toH1.grad ≤ ENNReal.ofReal C * weightedGradNorm (a.coeffOn (originCube d m)).toCoeffField (openCubeSet (originCube d m)) u.toH1.grad

A summably small identity-comparison error row gives a uniform weighted gradient bound between centered Euclidean cubes.