High-contrast homogenization:

Provider.Regularity.RoundedNormalizedRootDoubledResponseSubadditivity

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

Doubled-response subadditivity over the normalized-root filling

The doubled response is the sum of the primal and reflected half-quadratic forms, less the fixed pairing of the two loads. On a countable almost- everywhere partition, the weights sum to one, so the pairing cancels exactly. This upgrades coarse-block subadditivity to the full response used by the normalized reference certificate.

noncomputable def HCPolySupport.HighContrast.Transport.coeffSpaceDoubledResponse {d : ℕ} (U : Set (Vec d)) (a : CoeffSpace d) (P Q : BlockVec d) : ℝ

The doubled response of a coefficient-space sample on a set, written in the coarse-block splitting used by the source.

Equations

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

theorem HCPolySupport.HighContrast.Transport.coeffSpaceDoubledResponse_eq_doubledResponseJ {d : ℕ} (U : Book.Ch02.Domain d) (a : CoeffSpace d) (P Q : BlockVec d) : coeffSpaceDoubledResponse U.carrier a P Q = Book.Ch02.doubledResponseJ U (a.coeffOn U) P Q

On a Chapter 2 domain, the coefficient-space splitting is exactly the canonical doubled response.

theorem HCPolySupport.HighContrast.Transport.coeffSpaceDoubledResponse_le_tsum_weight_of_countable_aePartition {d : ℕ} [NeZero d] {ι : Type u_1} [Countable ι] {U : Set (Vec d)} {c : ι → Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hU0 : MeasureTheory.volume U ≠ 0) (a : CoeffSpace d) (hc : ∀ (i : ι), IsOpenBoundedConvexDomain (c i)) (hsub : ∀ (i : ι), c i ⊆ U) (hdisj : Pairwise fun (i k : ι) => Disjoint (c i) (c k)) (hnull : MeasureTheory.volume (U \ ⋃ (i : ι), c i) = 0) (hcell0 : ∀ (i : ι), MeasureTheory.volume (c i) ≠ 0) (P Q : BlockVec d) (hsum : Summable fun (i : ι) => (MeasureTheory.volume (c i)).toReal / (MeasureTheory.volume U).toReal * coeffSpaceDoubledResponse (c i) a P Q) : coeffSpaceDoubledResponse U a P Q ≤ ∑' (i : ι), (MeasureTheory.volume (c i)).toReal / (MeasureTheory.volume U).toReal * coeffSpaceDoubledResponse (c i) a P Q

The coefficient-space doubled response is subadditive over a countable almost-everywhere partition whenever the weighted cell responses are summable. Summability of the two nonnegative half-quadratic series is derived from response summability and the summable partition weights.