High-contrast homogenization: Provider.Recurrence.AdaptedResponseSubadditivity

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

Subadditivity of the coarse block over a partition into convex cells

e.fixed.geometry.parent.child states 𝐀(U) ≤ Σ (|U_i| / |U|) 𝐀(U_i) for a disjoint partition of U up to a null set. The mathematics behind it is one line: the coarse block is the Hessian of the response functional J(U; p, q), which is a supremum over the a-harmonic competitors on U, and an a-harmonic function on U restricts to an a-harmonic function on every open subset; so each competitor for the parent is, cell by cell, a competitor for the cell, and averaging its integrand over the partition gives the bound.

Two facts turn that line into a proof over cells that are not triadic cubes. First, the identity reading the coarse block off the response functional, J(U; p, q) = ½ (-p, q) · 𝐀(U) (-p, q) - p · q, holds over every bounded open convex domain, not only over cubes: this is responseJ_eq_blockQuadratic below, assembled from the canonical recovery data of the variational problem. Second, the affine term - p · q is the same on the parent and on every cell, and the weights sum to one, so it cancels from the averaged inequality.

The subadditivity is proved here for an arbitrary finite family of bounded open convex cells of one common volume, pairwise disjoint and covering the parent up to a null set. The aligned subdivision of an adapted cell is such a family.

Ellipticity of a pointwise representative on a measurable set

theorem HCPolySupport.HighContrast.Recurrence.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 response functional consumes.

The response functional reads off the coarse block on any convex domain

theorem HCPolySupport.HighContrast.Recurrence.responseJ_eq_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 q : Vec d) : ResponseJ U p q f = 1 / 2 * blockVecDot (-p, q) (blockMatVecMul (coarseBlockMatrix U f) (-p, q)) - vecDot p q

The response functional is the coarse block quadratic form, on every bounded open convex domain. This is the identity that frees e.fixed.geometry.parent.child from the triadic cube.

Competitor restriction

theorem HCPolySupport.HighContrast.Recurrence.responseJ_le_sum_weight_of_aePartition {d : ℕ} {ι : Type u_1} {U : Set (Vec d)} {Z : Finset ι} {c : ι → Set (Vec d)} {f : CoeffField d} {lam Lam : ℝ} (hU : IsOpenBoundedConvexDomain U) (hEll : IsEllipticFieldOn lam Lam U f) (hc : ∀ i ∈ Z, IsOpenBoundedConvexDomain (c i)) (hsub : ∀ i ∈ Z, c i ⊆ U) (hdisj : (↑Z).PairwiseDisjoint c) (hnull : MeasureTheory.volume (U \ ⋃ i ∈ ↑Z, c i) = 0) (hcell0 : ∀ i ∈ Z, MeasureTheory.volume (c i) ≠ 0) (p q : Vec d) : ResponseJ U p q f ≤ ∑ i ∈ Z, (MeasureTheory.volume (c i)).toReal / (MeasureTheory.volume U).toReal * ResponseJ (c i) p q f

Subadditivity of the response functional. Every a-harmonic competitor on the parent restricts to a competitor on each cell, so the average of its integrand is bounded by the average of the cells' suprema.

Subadditivity of the coarse block

theorem HCPolySupport.HighContrast.Recurrence.blockQuadratic_le_sum_weight_of_aePartition {d : ℕ} [NeZero d] {ι : Type u_1} {U : Set (Vec d)} {Z : Finset ι} {c : ι → Set (Vec d)} {f : CoeffField d} {lam Lam : ℝ} (hU : IsOpenBoundedConvexDomain U) (hEll : IsEllipticFieldOn lam Lam U f) (hU0 : MeasureTheory.volume U ≠ 0) (hc : ∀ i ∈ Z, IsOpenBoundedConvexDomain (c i)) (hsub : ∀ i ∈ Z, c i ⊆ U) (hdisj : (↑Z).PairwiseDisjoint c) (hnull : MeasureTheory.volume (U \ ⋃ i ∈ ↑Z, c i) = 0) (hcell0 : ∀ i ∈ Z, MeasureTheory.volume (c i) ≠ 0) (X : BlockVec d) : 1 / 2 * blockVecDot X (blockMatVecMul (coarseBlockMatrix U f) X) ≤ ∑ i ∈ Z, (MeasureTheory.volume (c i)).toReal / (MeasureTheory.volume U).toReal * (1 / 2 * blockVecDot X (blockMatVecMul (coarseBlockMatrix (c i) f) X))

Subadditivity of the coarse block over a partition into convex cells, in the quadratic form that defines the Loewner order. This is the first display of e.fixed.geometry.parent.child, with its printed weights |U_i| / |U|.