High-contrast homogenization: Provider.Regularity.OrderDecoupledRoundedApplication

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

Order-decoupled rounded coefficient application

The deterministic Dirichlet response selects its fractional order before any coefficient sample is introduced. The stochastic certificate selects its printed order after g. Their common output consists only of the rounded coefficient family, the corrected effective scale, and response rows at the printed order.

structure HCPolySupport.HighContrast.PrivateRoundedPhysicalDirichletSpine (d : ℕ) [NeZero d] : Type

The deterministic rounded Dirichlet response with its internally selected small order.

• order : ↑FractionalOrder

  Fractional order, smaller than one twelfth, used by the private Dirichlet response.

• order_lt_one_twelfth : ↑self.order < 1 / 12
• responseConstant : ENNReal

  Finite extended nonnegative constant controlling the rounded Dirichlet response.

• responseConstant_lt_top : self.responseConstant < ⊤
• respond (m : ℤ) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (h : CenteredCubeEuclideanL2Field d m) : MemCenteredCubeEuclideanHs self.order h → ∃ (w : H10Function (openCubeSet (originCube d m))), (IsZeroTraceDirichletRhsWeakSolution (constantCoeffField (roundedReferenceMatrix abar hS)) (openCubeSet (originCube d m)) w fun (y : Vec d) => -h.toField y) ∧ MemCenteredCubeEuclideanHs self.order (centeredCubeGradientEuclideanL2Field w) ∧ centeredCubeEuclideanHsFullENorm self.order (centeredCubeGradientEuclideanL2Field w) ≤ self.responseConstant * centeredCubeEuclideanHsFullENorm self.order h ∧ ∃ (wPhysical : H10Function (roundedPhysicalCube abar m)), (wPhysical.toFun = fun (x : Vec d) => w.toFun (matVecMul (baseRoundedGrid (symmPart abar))⁻¹ x)) ∧ (wPhysical.grad = fun (x : Vec d) => matVecMul (baseRoundedGrid (symmPart abar))⁻¹ (w.grad (matVecMul (baseRoundedGrid (symmPart abar))⁻¹ x))) ∧ (IsZeroTraceDirichletRhsWeakSolution (constantCoeffField (roundedPhysicalReferenceMatrix abar)) (roundedPhysicalCube abar m) wPhysical fun (x : Vec d) => -roundedPhysicalDirichletDatum abar h x) ∧ wPhysical.gradToHilbertVectorL2 = affineGradientQuotientPushforward ⋯ ⋯ ⋯ (baseRoundedGrid (symmPart abar))⁻¹ w.gradToHilbertVectorL2 ∧ hsNormSq (roundedPhysicalCube abar m) (↑self.order) wPhysical.grad ≤ roundedPhysicalGradientHsLoss abar ↑self.order * hsNormSq (openCubeSet (originCube d m)) (↑self.order) w.grad

theorem HCPolySupport.HighContrast.nonempty_privateRoundedPhysicalDirichletSpine (d : ℕ) [NeZero d] : Nonempty (PrivateRoundedPhysicalDirichletSpine d)

The continuity-at-zero construction inhabits the private response spine.

noncomputable def HCPolySupport.HighContrast.privateRoundedPhysicalDirichletSpine (d : ℕ) [NeZero d] : PrivateRoundedPhysicalDirichletSpine d

A fixed choice of the deterministic response spine, made before any stochastic exponent or sample is introduced.

Equations

• HCPolySupport.HighContrast.privateRoundedPhysicalDirichletSpine d = Classical.choice ⋯