High-contrast homogenization: #
Provider.PolynomialHomogenization.Root.RowSupply.ObservationNormalizedResponseParentRow
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Observation normalized responses priced by one parent row #
The geometric parent is selected before the unit load. Hence the exact observation realization and the adapted-target filling estimate may be maximized over all normalized identity loads without changing that parent.
theorem
HCPolySupport.HighContrast.RowSupply.observationNormalizedBlockResponseMax_le_normalizedParentRow_of_enclosed
{d : ℕ}
[NeZero d]
{s epsilon : ℝ}
(hs : 0 < s)
(hsHalf : s < 1 / 2)
(hepsilon : 0 < epsilon)
(center : Vec 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)
(k M : ℤ)
(hkM : k ≤ M)
(w : Fin d → ℤ)
(aObs : Book.Ch03.CoeffFamily d)
(hObs :
(aObs.coeffOn
(translateCube w
(originCube d k))).toCoeffField =ᵐ[volumeMeasureOn (openCubeSet (translateCube w (originCube d k)))]
fun (x : Vec d) =>
affineCoefficient (matSqrt (symmPart abar)) ⋯ (fun (y : Vec d) => scaledCoeff epsilon a y - skewPart abar)
(x + center))
(hEnclose :
adaptedCellTranslate (epsilonAffineGrid epsilon abar) k
(epsilon⁻¹ • matVecMul (matSqrt (symmPart abar)) center + adaptedCellCenter (epsilonAffineGrid epsilon abar) k w) ⊆
adaptedCell (Selection.normalizedRoot (symmPart abar)) M)
:
Book.Ch02.normalizedBlockResponseMax (translateCube w (originCube d k)) aObs 1 ≤ ∑' (u : ℕ), (if u = 0 then 1
else 6 * ↑d * √↑d * ‖(epsilonAffineGrid epsilon abar)⁻¹ * Selection.normalizedRoot (symmPart abar)‖ * 3 ^ (-↑u)) * Book.Ch02.maxDescendantNormalizedBlockResponseAtScale (originCube d M) (k - ↑u) aRef 1
A prescribed enclosing parent controls the normalized observation response; the estimate is uniform over the unit identity load.