High-contrast homogenization: Provider.Regularity.RoundedNormalizedRootCellResponseMax

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

Normalized-root cell responses below the reference response maximum

A unit doubled load on the identity reference cube has physical inverse loads that are independent of the cell. Exact normalized-response covariance then bounds every corresponding normalized-root cell response by the canonical one-cube response maximum.

theorem HCPolySupport.HighContrast.exists_normalizedRootCell_doubledResponseJ_le_normalizedBlockResponseMax {d : ℕ} [NeZero d] (a : CoeffSpace d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (t : ℤ) (aRef : Book.Ch03.CoeffFamily d) (haRef : ∀ (R : TriadicCube d), (aRef.coeffOn R).toCoeffField = affineCoefficient (Selection.normalizedRoot (symmPart abar)) ⋯ ((normalizedCenteredCoeff a abar hS).coeffOn (Response.adaptedDomain ⋯ t)).toCoeffField) (e : FullBlockVec d) (he : Book.Ch02.fullBlockVecNormSq e = 1) : ∃ (P : BlockVec d) (Q : BlockVec d), normalizedReferencePrimalLoad abar P = ofFullBlockVec e ∧ normalizedReferenceDualLoad abar Q = ofFullBlockVec e ∧ ∀ (k : ℤ) (w : Fin d → ℤ), Book.Ch02.doubledResponseJ (Response.adaptedDomainAt ⋯ k w) (a.coeffOn (Response.adaptedDomainAt ⋯ k w)) P Q ≤ Book.Ch02.normalizedBlockResponseMax (translateCube w (originCube d k)) aRef 1

A unit identity-reference load has one pair of inverse physical loads, independent of the cell, whose response on every exact normalized-root cell is bounded by that reference cell's canonical normalized-response maximum.