High-contrast homogenization: Provider.Regularity.FiniteAffineSuccessorGradient

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

Successive finite-corrector gradient estimate

This module combines the two-scale local energy estimate with finite large-scale Lipschitz descent on centered Euclidean cubes.

theorem HCPolySupport.HighContrast.exists_finiteAffineSuccessorWeightedGradientEstimateConstant (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) (δ : ℝ) (n m : ℤ) (e : Vec d), δ ∈ Set.Ioc 0 c → n ≤ m - 2 → ScalarIdentityGoodTailOnInterval a s δ n (m + 1) → weightedGradNorm (a.coeffOn (originCube d n)).toCoeffField (openCubeSet (originCube d n)) (finiteAffineSuccessorDifference a m e).toH1.grad ≤ ENNReal.ofReal (C * (scalarIdentityCorrectedWeakError a s m + scalarIdentityCorrectedWeakError a s (m + 1)) * euclideanNorm e)

A finite good tail bounds the successive finite-corrector gradient on every centered cube at least two scales below the parent cube.