High-contrast homogenization: Provider.Response.ProfileRecentPointwise #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Pointwise bounds for the recent profile terms #
The recent cell defect is split at its scale-dependent annealed mean. The two centered pieces are read from the terminal centered maximum, while the positive mean increment is read from the nonlinear gain. The averaged defect uses the same positive increment after expectation.
Normalized block algebra #
theorem
HCPolySupport.HighContrast.Response.blockSize_blockSub_comm
{d : ℕ}
{A B F : BlockMat d}
(hA : IsSymmetricBlockMat A)
(hB : IsSymmetricBlockMat B)
(hF : IsSymmetricBlockMat F)
(hFpd : Book.Ch02.BlockPosDef F)
:
The scalar size of a difference is symmetric in its two endpoints.
theorem
HCPolySupport.HighContrast.Response.blockSize_blockSub_triangle
{d : ℕ}
{A B C F : BlockMat d}
(hA : IsSymmetricBlockMat A)
(hB : IsSymmetricBlockMat B)
(hC : IsSymmetricBlockMat C)
(hF : IsSymmetricBlockMat F)
(hFpd : Book.Ch02.BlockPosDef F)
:
The normalized scalar size obeys the triangle inequality through an intermediate symmetric block.
The nonlinear mean increment #
Reading the centered maximum #
theorem
HCPolySupport.HighContrast.Response.ofReal_centered_cell_le_profileCenteredMaximum
{d : ℕ}
{P : MeasureTheory.Measure (CoeffSpace d)}
{rhoMax : ℝ}
{q : Mat d}
{jStar k t : ℤ}
(hjk : jStar ≤ k)
(hkt : k ≤ t)
{w : Fin d → ℤ}
(hw : adaptedCellCenter q k w ∈ adaptedCell q t)
(a : CoeffSpace d)
:
ENNReal.ofReal
(3 ^ (-rhoMax * (↑t - ↑k)) * blockSize (blockSub (adaptedResponse q k w a) (adaptedMean P q k)) (adaptedMean P q t)) ≤ profileCenteredMaximum P rhoMax q jStar t a
A centered cell on a retained scale is one of the terms of Z_t.
theorem
HCPolySupport.HighContrast.Response.centered_cell_le_profileCenteredMaximum_toReal
{d : ℕ}
{P : MeasureTheory.Measure (CoeffSpace d)}
{rhoMax : ℝ}
{q : Mat d}
{jStar k t : ℤ}
(hjk : jStar ≤ k)
(hkt : k ≤ t)
{w : Fin d → ℤ}
(hw : adaptedCellCenter q k w ∈ adaptedCell q t)
{a : CoeffSpace d}
(htop : profileCenteredMaximum P rhoMax q jStar t a ≠ ⊤)
(hsize : 0 ≤ blockSize (blockSub (adaptedResponse q k w a) (adaptedMean P q k)) (adaptedMean P q t))
:
blockSize (blockSub (adaptedResponse q k w a) (adaptedMean P q k)) (adaptedMean P q t) ≤ 3 ^ (rhoMax * (↑t - ↑k)) * (profileCenteredMaximum P rhoMax q jStar t a).toReal
On the finite branch, a centered cell is bounded by the growing terminal
weight times Z_t.