High-contrast homogenization: #
Provider.PolynomialHomogenization.Root.RowSupply.FixedParentObservationResponse
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Observation response at a fixed common parent #
The bounded-domain parent is selected once for the whole Whitney family. The usual descendant filling and boundary convolution can then be evaluated at this fixed parent, retaining the upper generation needed by the physical frame estimate.
theorem
HCPolySupport.HighContrast.RowSupply.observationAllDepth_normalizedFixedParentMajorant
{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)
(aObs : Book.Ch03.CoeffFamily d)
(hObs :
(aObs.coeffOn (originCube d K)).toCoeffField =ᵐ[volumeMeasureOn (openCubeSet (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 0) ⊆
adaptedCell (Selection.normalizedRoot (symmPart abar)) M)
(l : ℕ)
:
Book.Ch02.maxDescendantNormalizedBlockResponseAtScale (originCube d K) (K - ↑l) 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 - ↑l - ↑u) aRef 1
A supplied enclosing parent controls every descendant response of one centered observation cube.
theorem
HCPolySupport.HighContrast.RowSupply.observationHomogenizationError_le_referencePowerTail_fixedParent
{d : ℕ}
[NeZero d]
{s epsilon amplitude kappa : ℝ}
(hs : 0 < s)
(hsHalf : s < 1 / 2)
(hepsilon : 0 < epsilon)
(hAmplitude : 0 ≤ amplitude)
(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)
(N K M : ℤ)
(hNM : N ≤ M)
(hKM : K ≤ M)
(hTail : ScalarIdentityPowerTail aRef s amplitude kappa (3 ^ N))
(aObs : Book.Ch03.CoeffFamily d)
(hObs :
(aObs.coeffOn (originCube d K)).toCoeffField =ᵐ[volumeMeasureOn (openCubeSet (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 0) ⊆
adaptedCell (Selection.normalizedRoot (symmPart abar)) M)
:
(Summable fun (l : ℕ) => Book.Ch02.geometricWeight s 2 l * observationParentRowMajorant epsilon abar aRef M K l) ∧ (∀ (l : ℕ),
Book.Ch02.maxDescendantNormalizedBlockResponseAtScale (originCube d K) (K - ↑l) aObs 1 ≤ observationParentRowMajorant epsilon abar aRef M K l) ∧ Book.Ch02.HomogenizationErrorOnCube (originCube d K) s Book.Ch02.MultiscaleExponent.infinity
(Book.Ch02.MultiscaleExponent.finite 2) aObs 1 ≤ √(observationParentConvolutionFactor d s epsilon abar M K * (amplitude * (3 ^ M / 3 ^ N) ^ (-kappa)) ^ 2)
A fixed parent above the activation generation gives the same power-tail response estimate as the cellwise construction, with its parent generation now bounded by construction.