High-contrast homogenization: Provider.Response.AdaptedCutoffGradientField

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

The gradient field of the adapted cutoff

The div-curl estimate reads a cutoff through its gradient field: it needs that field to be essentially bounded on the cube, to have smooth components, and to have a bounded componentwise derivative. The adapted cutoff carries instead a bound for its first derivative and a bound for its second iterated derivative, so the componentwise derivative of the gradient field has to be recovered from the second iterated derivative.

This module performs that recovery in adapted coordinates and reads off the three cutoff data of the div-curl estimate with one common dimension-only coefficient. The reference-cube div-curl coefficient then loses both of its free parameters.

The common derivative coefficient

noncomputable def HCPolySupport.HighContrast.Response.adaptedCutoffDerivativeCoeff (d : ℕ) : ℝ

The common dimension-only coefficient of the adapted cutoff's first two derivatives in adapted coordinates.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.Response.adaptedCutoffDerivativeCoeff_eq (d : ℕ) : adaptedCutoffDerivativeCoeff d = 1024 * ↑d ^ 4 * max 1 (max smoothTransitionProfile.derivBound smoothTransitionProfile.secondDerivBound) ^ 2

The defining equation of the common derivative coefficient.

theorem HCPolySupport.HighContrast.Response.adaptedCutoffDerivativeCoeff_nonneg (d : ℕ) : 0 ≤ adaptedCutoffDerivativeCoeff d

The common derivative coefficient is nonnegative.

Smoothness of the pullback

theorem HCPolySupport.HighContrast.Response.adaptedPreYoungCutoff_pullback_smooth {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) : ContDiff ℝ ↑⊤ fun (y : Vec d) => adaptedPreYoungCutoff q hq t (matVecMul q y)

The pullback of the adapted cutoff by the grid matrix is smooth.

The three cutoff data of the div-curl estimate

theorem HCPolySupport.HighContrast.Response.scalarCutoffGradientField_adaptedPreYoungCutoff_pullback_fderiv_bound {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (Q : TriadicCube d) (i : Fin d) (z : Vec d) : z ∈ cubeSet Q → ‖fderiv ℝ (fun (x : Vec d) => scalarCutoffGradientField (fun (y : Vec d) => adaptedPreYoungCutoff q hq t (matVecMul q y)) x i) z‖ ≤ adaptedCutoffDerivativeCoeff d * 3 ^ (-2 * t)

The componentwise derivative of the gradient field. Each component of the gradient field of the pulled-back adapted cutoff has derivative bounded by the common coefficient times the square of the reciprocal side length. The second iterated derivative dominates each componentwise derivative.

theorem HCPolySupport.HighContrast.Response.cubeLpNorm_infty_scalarCutoffGradientField_adaptedPreYoungCutoff_pullback_le {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (Q : TriadicCube d) : cubeLpNorm Q ⊤ (scalarCutoffGradientField fun (y : Vec d) => adaptedPreYoungCutoff q hq t (matVecMul q y)) ≤ adaptedCutoffDerivativeCoeff d * 3 ^ (-t)

The sup norm of the gradient field. It is bounded by the common coefficient times the reciprocal side length.

theorem HCPolySupport.HighContrast.Response.memLp_top_scalarCutoffGradientField_adaptedPreYoungCutoff_pullback {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (Q : TriadicCube d) : MeasureTheory.MemLp (scalarCutoffGradientField fun (y : Vec d) => adaptedPreYoungCutoff q hq t (matVecMul q y)) ⊤ (normalizedCubeMeasure Q)

The gradient field of the pulled-back adapted cutoff is essentially bounded on every triadic cube.

theorem HCPolySupport.HighContrast.Response.contDiff_scalarCutoffGradientField_adaptedPreYoungCutoff_pullback {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (i : Fin d) : ContDiff ℝ ↑⊤ fun (x : Vec d) => scalarCutoffGradientField (fun (y : Vec d) => adaptedPreYoungCutoff q hq t (matVecMul q y)) x i

Each component of that gradient field is smooth.

The div-curl coefficient at the adapted cutoff

theorem HCPolySupport.HighContrast.Response.divCurlWeakNormCoeff_originCube_adaptedPreYoungCutoff_le (d : ℕ) (t : ℤ) : divCurlWeakNormCoeff (originCube d t) (adaptedCutoffDerivativeCoeff d * 3 ^ (-2 * t)) (adaptedCutoffDerivativeCoeff d * 3 ^ (-t)) ≤ divCurlDimensionCoeff d * (adaptedCutoffDerivativeCoeff d * 3 ^ (-t))

The div-curl coefficient at the adapted cutoff. Inserting the two cutoff bounds leaves a dimension-only prefactor times the reciprocal side length; no bound is carried.

The div-curl weak-norm term at the adapted cutoff