High-contrast homogenization: Provider.Response.CutoffDerivatives

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

Quantitative adapted-coordinate derivatives

Pulling the physical cutoff back by the grid matrix is the normalized reference cutoff. The estimates below therefore control exactly the tensors denoted by q ∇φ and q² ∇²φ in the response argument.

theorem HCPolySupport.HighContrast.Response.adaptedPreYoungCutoff_transitionScale {d : ℕ} [NeZero d] (t : ℤ) : 2 / ((1 - 1 / (4 * ↑d) - (1 - 1 / (2 * ↑d))) * cubeRadius (originCube d t)) = 16 * ↑d * 3 ^ (-t)

The reciprocal transition width for the chosen two concentric cubes.

theorem HCPolySupport.HighContrast.Response.adaptedPreYoungCutoff_gradientCoefficient_le_common (d : ℕ) [NeZero d] : 32 * ↑d ^ 2 * smoothTransitionProfile.derivBound ≤ 1024 * ↑d ^ 4 * max 1 (max smoothTransitionProfile.derivBound smoothTransitionProfile.secondDerivBound) ^ 2

The common second-order coefficient also dominates the sharper gradient coefficient.

theorem HCPolySupport.HighContrast.Response.adaptedPreYoungCutoff_pullback_fderiv_bound {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (x : Vec d) : ‖fderiv ℝ (fun (y : Vec d) => adaptedPreYoungCutoff q hq t (matVecMul q y)) x‖ ≤ 1024 * ↑d ^ 4 * max 1 (max smoothTransitionProfile.derivBound smoothTransitionProfile.secondDerivBound) ^ 2 * 3 ^ (-t)

The adapted-coordinate first derivative has the common dimension-only bound used for both derivative orders.

theorem HCPolySupport.HighContrast.Response.adaptedPreYoungCutoff_pullback_iteratedFDeriv_two_bound {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (x : Vec d) : ‖iteratedFDeriv ℝ 2 (fun (y : Vec d) => adaptedPreYoungCutoff q hq t (matVecMul q y)) x‖ ≤ 1024 * ↑d ^ 4 * max 1 (max smoothTransitionProfile.derivBound smoothTransitionProfile.secondDerivBound) ^ 2 * 3 ^ (-2 * t)

The adapted-coordinate Hessian has the same dimension-only coefficient as the first derivative.