High-contrast homogenization: Provider.Regularity.CorrectorIntrinsicSlopeGoodTail

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

Intrinsic slope from a scalar good tail

This module supplies the analytic input missing from the topology-only diagonal argument. Cube averages are controlled through the negative Besov seminorm and the multiscale lower-ellipticity factor, never through a pointwise ellipticity constant.

theorem HCPolySupport.HighContrast.norm_cubeAverageVec_le_sqrt_card_mul_rpow_mul_negativeSeminormTwo_of_mem_descendant {d : ℕ} (Q R : TriadicCube d) (s : ℝ) (j : ℕ) (F : Vec d → Vec d) (hR : R ∈ descendantsAtDepth Q j) (hs : 0 < s) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) : ‖cubeAverageVec R F‖ ≤ √↑(descendantsAtDepth Q j).card * Real.rpow 3 (s * ↑j) * cubeBesovNegativeVectorSeminormTwo Q s F

A descendant cube average is controlled by the parent negative Besov seminorm, with the explicit finite-depth loss.

theorem HCPolySupport.HighContrast.exists_finiteAffineCorrectionDepthTwoGradientAverageEstimateConstant (d : ℕ) [NeZero d] (sOut b : ℝ) (hb : 0 < b) (h2b : 2 * b < sOut) (hsOut_lt : sOut < 1) : ∃ (C : ℝ), 0 < C ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (q : ℕ) (e : Vec d), ‖cubeAverageVec (originCube d ↑q) (finiteAffineCorrection a (↑(q + 2)) e).grad‖ ≤ C * scalarIdentityCorrectedWeakError a b ↑(q + 2) * euclideanNorm e

The average gradient of the finite correction two scales inside its Dirichlet cube is controlled by the corrected scalar weak error.

theorem HCPolySupport.HighContrast.exists_cubeSolutionGradientAverageEnergyConstant (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) : ∃ (C : ℝ), 0 < C ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (k : ℤ) (u : Book.Ch03.CubeSolution (originCube d k) a), scalarIdentityWeakError a s k ≤ 1 → ‖cubeAverageVec (originCube d k) u.toH1.grad‖ ≤ C * Book.Ch03.h1EnergyNormOnCube (originCube d k) a u.toH1

Under a unit scalar weak-error bound, the average gradient of a cube solution is controlled by its normalized coefficient-energy norm, with a constant depending only on dimension and the weak-norm order.

theorem HCPolySupport.HighContrast.exists_finiteAffineSuccessorGradientAverageEstimateConstant (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 m : ℤ) (e : Vec d), delta ∈ Set.Ioc 0 c → n ≤ m - 2 → ScalarIdentityGoodTailOnInterval a s delta n (m + 1) → ‖cubeAverageVec (originCube d n) (finiteAffineSuccessorDifference a m e).toH1.grad‖ ≤ C * (scalarIdentityCorrectedWeakError a s m + scalarIdentityCorrectedWeakError a s (m + 1)) * euclideanNorm e

A finite good tail uniformly controls the average gradient of every successive finite-corrector difference on an inner centered cube.

theorem HCPolySupport.HighContrast.exists_scalarIdentityGoodTailIntrinsicSlopeThreshold (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 → ∀ (e : Vec d), ∃ (hloc : FiniteAffineCorrectionLocalCauchy a), HasIntrinsicNormalizedSlope e (finiteAffineCorrectionJointLocalLimit a hloc e)

Every sufficiently small scalar good tail produces the canonical intrinsically normalized corrector with the prescribed affine slope.