High-contrast homogenization: Provider.Response.DivCurlWeakNormTerm

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

The div-curl weak-norm term on a reference triadic cube

The cutoff-product term of the centered response split is the quantity the manuscript controls by a quantitative div-curl argument: testing the equation for the maximizer with the cutoff multiple of the potential defect and integrating by parts turns the product into a pairing of the potential fluctuation against the flux defect, and Besov duality bounds that pairing by the product of the two negative-order weak seminorms.

The estimate is recorded here for an arbitrary Chapter 2 coefficient on the reference cube domain, with the two weak seminorm bounds as data. This is the carrier on which the manuscript states the estimate; an adapted geometry is reached from it by a change of variables.

theorem HCPolySupport.HighContrast.Response.abs_cutoffProductTermOnCube_le_scaledWeakNormProduct {d : ℕ} (Q : TriadicCube d) {s t : ℝ} (hs_pos : 0 < s) (hs_lt_one : s < 1) (hst : s + t ≤ 1) (a : Book.Ch02.CoeffOn (Book.Ch02.cubeDomain Q)) {φ : Vec d → ℝ} (p q p0 q0 : Vec d) {B gradWeak fluxWeak : ℝ} (hB : 0 ≤ B) (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ openCubeSet Q) (hcutoffGradient : MeasureTheory.MemLp (scalarCutoffGradientField φ) ⊤ (normalizedCubeMeasure Q)) (hcutoffSmooth : ∀ (i : Fin d), ContDiff ℝ ↑⊤ fun (x : Vec d) => scalarCutoffGradientField φ x i) (hcutoffDeriv : ∀ (i : Fin d), ∀ z ∈ cubeSet Q, ‖fderiv ℝ (fun (x : Vec d) => scalarCutoffGradientField φ x i) z‖ ≤ B) (hgradWeak : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q s N (Book.Ch05.Section53.JUpperBoundWeakNorms.canonicalMaximizerGradientDefectOnCube Q a p q p0) ≤ gradWeak) (hfluxWeak : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q t N (Book.Ch05.Section53.JUpperBoundWeakNorms.canonicalMaximizerFluxDefectOnCube Q a p q q0) ≤ fluxWeak) : |Book.Ch05.Section53.JUpperBoundWeakNorms.cutoffProductTermOnCube Q a φ p q p0 q0| ≤ Book.Ch05.Section53.JUpperBoundWeakNorms.cutoffProductScaledWeakNormCoeff Q s t B (scalarCutoffGradientField φ) * (cubeBesovScaleWeight (-s) Q * gradWeak * (cubeBesovScaleWeight (-t) Q * fluxWeak))

The div-curl weak-norm term for a Chapter 2 coefficient on the reference cube: the cutoff-product term of the centered response split is bounded by the product of the scaled gradient-defect and flux-defect weak seminorms, with the coefficient carried by the cutoff's gradient field.

The gradient exponent s and the flux exponent t are only required to satisfy 0 < s < 1 and s + t ≤ 1; the manuscript's own reading is the symmetric one s = t = 1/2.

noncomputable def HCPolySupport.HighContrast.Response.divCurlWeakNormCoeff {d : ℕ} (Q : TriadicCube d) (B Bone : ℝ) : ℝ

The div-curl coefficient at the symmetric exponents, for a cutoff whose gradient field has sup norm at most Bone and derivative at most B. The first factor is the manuscript's scale gain: on a cube of side 3^n a cutoff with ‖∇φ‖ ≲ 3^{-n} and ‖∇²φ‖ ≲ 3^{-2n} makes it O(3^{-n}).

Equations

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

theorem HCPolySupport.HighContrast.Response.divCurlWeakNormCoeff_eq {d : ℕ} (Q : TriadicCube d) (B Bone : ℝ) : divCurlWeakNormCoeff Q B Bone = 3 * (cubeScaleFactor Q * B + Bone) * (Book.Ch01.Legacy.fullVectorPoincareConstant Q * 3 ^ (↑d + 1) * ↑d) * (↑d * 3 ^ (↑d + 1 / 2))

The defining equation of the div-curl coefficient.

theorem HCPolySupport.HighContrast.Response.abs_cutoffProductTermOnCube_le_divCurlWeakNormCoeff {d : ℕ} (Q : TriadicCube d) (a : Book.Ch02.CoeffOn (Book.Ch02.cubeDomain Q)) {φ : Vec d → ℝ} (p q p0 q0 : Vec d) {B Bone gradWeak fluxWeak : ℝ} (hB : 0 ≤ B) (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ openCubeSet Q) (hcutoffGradient : MeasureTheory.MemLp (scalarCutoffGradientField φ) ⊤ (normalizedCubeMeasure Q)) (hcutoffSmooth : ∀ (i : Fin d), ContDiff ℝ ↑⊤ fun (x : Vec d) => scalarCutoffGradientField φ x i) (hcutoffDeriv : ∀ (i : Fin d), ∀ z ∈ cubeSet Q, ‖fderiv ℝ (fun (x : Vec d) => scalarCutoffGradientField φ x i) z‖ ≤ B) (hBone : cubeLpNorm Q ⊤ (scalarCutoffGradientField φ) ≤ Bone) (hgradWeak : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q (1 / 2) N (Book.Ch05.Section53.JUpperBoundWeakNorms.canonicalMaximizerGradientDefectOnCube Q a p q p0) ≤ gradWeak) (hfluxWeak : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q (1 / 2) N (Book.Ch05.Section53.JUpperBoundWeakNorms.canonicalMaximizerFluxDefectOnCube Q a p q q0) ≤ fluxWeak) : |Book.Ch05.Section53.JUpperBoundWeakNorms.cutoffProductTermOnCube Q a φ p q p0 q0| ≤ divCurlWeakNormCoeff Q B Bone * (cubeBesovScaleWeight (-(1 / 2)) Q * gradWeak * (cubeBesovScaleWeight (-(1 / 2)) Q * fluxWeak))

The div-curl weak-norm term at the manuscript's exponents. Both weak seminorms are read at order -1/2, and the cutoff enters only through the sup norm Bone of its gradient field and the bound B on that field's derivative.