High-contrast homogenization: Provider.Response.AdaptedLinearOscillation #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Linear cutoff oscillation on an adapted child #
An aligned physical child pulls back to an ordinary triadic descendant. The cutoff loses one full power of the child depth, while the endpoint field norm uses a half-power weight. Oscillation duality therefore controls the literal cutoff readout by the terminal adapted weak seminorm.
theorem
HCPolySupport.HighContrast.Response.translateCube_mem_descendantsAtDepth_of_mem_alignedIndex
{d : ℕ}
{q : Mat d}
(hq : Matrix.PosDef q)
{s t : ℤ}
(hst : s ≤ t)
{w : Fin d → ℤ}
(hw : w ∈ alignedIndex q s t)
:
An aligned child label gives the corresponding ordinary descendant of the terminal reference cube.
theorem
HCPolySupport.HighContrast.Response.ofReal_abs_volumeAverage_adaptedCellAt_cutoffOscillation_le
{d : ℕ}
[NeZero d]
{q S : Mat d}
(hq : Matrix.PosDef q)
(hS : Matrix.PosDef S)
{s t : ℤ}
(hst : s ≤ t)
{w : Fin d → ℤ}
(hw : w ∈ alignedIndex q s t)
(F : Vec d → BlockVec d)
(alpha : BlockCoord d)
(hF₁ : MemVectorL2 (adaptedCell q t) fun (x : Vec d) => matVecMul S (F x).1)
(hF₂ : MemVectorL2 (adaptedCell q t) fun (x : Vec d) => matVecMul S⁻¹ (F x).2)
:
ENNReal.ofReal
|volumeAverage (adaptedCellAt q s w) fun (x : Vec d) =>
(adaptedPreYoungCutoff q hq t x - volumeAverage (adaptedCellAt q s w) (adaptedPreYoungCutoff q hq t)) * toFullBlockVec (F x) alpha| ≤ ENNReal.ofReal
(1024 * ↑d ^ 4 * max 1 (max smoothTransitionProfile.derivBound smoothTransitionProfile.secondDerivBound) ^ 2 * 3 ^ (-(t - s)) * (cubeBesovCircDepthWeight (translateCube w (originCube d s)) (1 / 2) 1)⁻¹) * (ENNReal.ofReal √↑(descendantsAtDepth (originCube d t) (t - s).toNat).card * ENNReal.ofReal (cubeBesovScaleWeight (-(1 / 2)) (originCube d t)) * ENNReal.ofReal (3 ^ (-(1 / 2 * ↑t))) * ENNReal.ofReal √(max (Book.Ch02.matrixFrobeniusNormSq S⁻¹) (Book.Ch02.matrixFrobeniusNormSq S)) * adaptedWeakSeminorm q t (1 / 2) fun (x : Vec d) => (matVecMul S (F x).1, matVecMul S⁻¹ (F x).2))
The literal cutoff-oscillation readout on an aligned adapted child is controlled by the terminal metric weak seminorm. All child-cardinality, scale, cutoff, and affine-metric factors remain explicit.