High-contrast homogenization: Provider.Sharp.CoarseBlockOrder

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

The pathwise block bounds of the coarse response

The elementary bounds for the coarse block (s.introduction) assert the sharp order 𝐀^♯(U) ≤ 𝐀(U) along every realization of the coefficient field. By the reduction of ReflectionOrder this is the pair of signed reflection bounds ±R ≤ 𝐀(U), that is, the pair of scalar inequalities

± P₁ · P₂ ≤ ½ P · 𝐀(U) P

over doubled vectors P = (P₁, P₂). Both are the same variational statement about the coarse energy μ(U; P) whose Hessian 𝐀(U) is: the pointwise Young inequality on the doubled coefficient matrix bounds the block energy density below by the pairing of the potential and flux fields, and that pairing averages to P₁ · P₂ because the potential correction is a gradient of zero trace and the flux correction is solenoidal of zero normal trace — the div-curl cancellation.

Only the first sign has to be quoted: the second is the first read on the adjoint field, since flipping the flux half of a doubled vector and transposing the coefficient field leaves the coarse energy invariant and reverses the pairing.

The identification of μ(U; ·) with the quadratic form of the coarse block matrix holds over every bounded open convex domain, not only over cubes; it comes from the canonical recovery data of the variational problem, exactly as the subadditivity of the response does.

The conclusion is unconditional along the coefficient space: the sample field only enters through a measurable pointwise uniformly elliptic representative, which every member of the class has, and the coarse response only sees the almost everywhere class of the field.

Ellipticity of a pointwise representative

theorem HCPolySupport.HighContrast.Sharp.isEllipticFieldOn_of_measurable {d : ℕ} {lam Lam : ℝ} {f : CoeffField d} (hf : Measurable f) {U : Set (Vec d)} (hell : ∀ x ∈ U, IsEllipticMatrix lam Lam (f x)) (hU : MeasurableSet U) : IsEllipticFieldOn lam Lam U f

A measurable field uniformly elliptic at every point of a measurable set is elliptic on that set, in the sense the coarse energy consumes.

The coarse energy is the quadratic form of the coarse block

theorem HCPolySupport.HighContrast.Sharp.mu_eq_half_blockQuadratic {d : ℕ} [NeZero d] {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {lam Lam : ℝ} {f : CoeffField d} (hEll : IsEllipticFieldOn lam Lam U f) (hvol : 0 < (MeasureTheory.volume U).toReal) (P : BlockVec d) : Mu U P f = 1 / 2 * blockVecDot P (blockMatVecMul (coarseBlockMatrix U f) P)

The coarse energy is half the quadratic form of the coarse block matrix, on every bounded open convex domain. This is the identity that carries the variational bounds of the coarse energy onto the block matrix of the variational coarse block.

The two signed pairing bounds

theorem HCPolySupport.HighContrast.Sharp.pairing_le_half_blockQuadratic {d : ℕ} [NeZero d] {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {lam Lam : ℝ} {f : CoeffField d} (hEll : IsEllipticFieldOn lam Lam U f) (hvol : 0 < (MeasureTheory.volume U).toReal) (P : BlockVec d) : vecDot P.1 P.2 ≤ 1 / 2 * blockVecDot P (blockMatVecMul (coarseBlockMatrix U f) P)

The lower pairing bound P₁ · P₂ ≤ ½ P · 𝐀(U) P: the div-curl form of the first half of the elementary block bounds.

theorem HCPolySupport.HighContrast.Sharp.neg_pairing_le_half_blockQuadratic {d : ℕ} [NeZero d] {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {lam Lam : ℝ} {f : CoeffField d} (hEll : IsEllipticFieldOn lam Lam U f) (hvol : 0 < (MeasureTheory.volume U).toReal) (P : BlockVec d) : -vecDot P.1 P.2 ≤ 1 / 2 * blockVecDot P (blockMatVecMul (coarseBlockMatrix U f) P)

The opposite pairing bound -P₁ · P₂ ≤ ½ P · 𝐀(U) P, the second half of the elementary block bounds: the lower bound read on the adjoint field, whose coarse energy at the flux-flipped vector is the coarse energy of the field.

The pathwise block bounds

theorem HCPolySupport.HighContrast.Sharp.blockMatLoewnerLE_blockSharp_coarseBlockMatrix {d : ℕ} [NeZero d] {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {lam Lam : ℝ} {f : CoeffField d} (hEll : IsEllipticFieldOn lam Lam U f) (hvol : 0 < (MeasureTheory.volume U).toReal) : BlockMatLoewnerLE (blockSharp (coarseBlockMatrix U f)) (coarseBlockMatrix U f)

The pathwise block bounds for a field with a pointwise uniformly elliptic representative, on a bounded open convex domain of positive volume.

theorem HCPolySupport.HighContrast.Sharp.blockMatLoewnerLE_blockSharp_coarseBlock {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hvol : 0 < (MeasureTheory.volume U).toReal) (a : CoeffSpace d) : BlockMatLoewnerLE (blockSharp (coarseBlock U a)) (coarseBlock U a)

The pathwise block bounds on the coefficient space: along every realization the variational coarse block response dominates its own sharp, on every bounded open convex domain of positive volume. No positivity or invertibility of the response is assumed, and no dimension is excluded.

theorem HCPolySupport.HighContrast.Sharp.blockMatLoewnerLE_blockSharp_coarseBlock_of_nonempty {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (a : CoeffSpace d) : BlockMatLoewnerLE (blockSharp (coarseBlock U a)) (coarseBlock U a)

The pathwise block bounds on a nonempty bounded open convex domain: the form in which the elementary block bounds are consumed, the positivity of the volume being that of a nonempty open set.