High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Dirichlet.ObservationFamilyRow

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

The composed row 6

Module the aObs premise/hObs pair: an observation coefficient family, one per ruled cell, agreeing a.e. on the observation cube with the gauge coefficient translated to that cell's centre.

The producer is the exists_observationCoeffFamily_and_forcedEquation (HCPoly.Provider.Regularity.ObservationCoefficientTransport), at center := ruledObservationCenter system i and m := (ruledObservationCube system i).scale. Its domain premise openCubeAtScale center m ⊆ U is the composition translateSet_observationCube_subset_interiorBuffer ∘ interiorBuffer_subset, the same pair CommonResidualObservationParent uses; the two cube spellings are reconciled by openCubeAtScale_eq_translateSet and openCubeAtScale_zero_eq_openCubeSet_originCube.

The weak-solution premise is row 4′ of module that module, and the source witness is exists_gaugeReducedSource.

theorem HCPolySupport.HighContrast.RowSupply.exists_frozenWitnessObservationFamily {d : ℕ} {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {epsilon : ℝ} (hepsilon : 0 < epsilon) {a : CoeffSpace d} {Uhat : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem Uhat rho Rad) {aHat : CoeffField d} (haHat : aHat = affineCoefficient (matSqrt (symmPart abar)) ⋯ fun (z : Vec d) => scaledCoeff epsilon a z - skewPart abar) (uHat : H1Function Uhat) (hWeak : IsWeakSolutionOn aHat Uhat uHat.grad) : ∃ (aObs : system.CellIndex → Book.Ch03.CoeffFamily d), ∀ (i : system.CellIndex), ((aObs i).coeffOn (ruledObservationCube system i)).toCoeffField =ᵐ[volumeMeasureOn (openCubeSet (ruledObservationCube system i))] fun (y : Vec d) => affineCoefficient (matSqrt (symmPart abar)) ⋯ (fun (z : Vec d) => scaledCoeff epsilon a z - skewPart abar) (y + ruledObservationCenter system i)

Row 6 — aObs, hObs. One observation coefficient family per ruled cell, in exact spelling.