Documentation

LeanPool.HighContrastHomogenization.Provider.Quenched.SmallContrastAverageDrops

High-contrast homogenization: Provider.Quenched.SmallContrastAverageDrops #

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

The averaged-defect drop bound #

The printed weak-norm estimate consumes the subdivision-averaged defect — the average of the aligned child responses against the parent response — through its first moment. By the pathwise subadditivity of the aligned subdivision the averaged defect is positive semidefinite, so its identity norm is dominated by its trace, whose expectation is exactly the trace of the normalized annealed mean drop by stationarity. This yields the per-depth L² bound by the root of the mean drop alone — the sharp replacement for the crude per-cell variance budget, and the shape the printed one-step estimate HC (4.17) requires (the drops enter linearly; no per-cell variance in the rooted sum).

source
noncomputable def HCPolySupport.HighContrast.Quenched.entryCLM' {n : Type u_1} [Fintype n] (i j : n) :
Matrix n n ℝ →L[ℝ] ℝ

Evaluation of the (i, j) entry of a finite real matrix as a continuous linear map.

Equations
Instances For
    source
    theorem HCPolySupport.HighContrast.Quenched.eLpNorm_sqrt_blockSize_averageDefect_le_drop {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} (hstat : IsStationaryLaw P) {l : ℤ} {q : Mat d} (hgrid : IsRoundedGrid l q) {k t : ℤ} (hlk : l ≤ k) (hkt : k ≤ t) (hintk : HasFiniteAdaptedMean P q k) (hintt : HasFiniteAdaptedMean P q t) {F : BlockMat d} (hFsym : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) :
    MeasureTheory.eLpNorm (fun (a : CoeffSpace d) => √(blockSize (Response.diagonalWeakAverageDefect q k t F a) (Book.Ch02.blockIdentity d))) 2 P ≤ ENNReal.ofReal √(2 * ↑d * blockSize (blockSub (adaptedMean P q k) (adaptedMean P q t)) F)

    The per-depth averaged defect through its trace. By the pathwise subadditivity of the aligned subdivision, the normalized averaged defect is positive semidefinite; its identity-size is therefore at most its trace, whose expectation is the trace of the normalized annealed mean drop by stationarity of the coefficient law, and the L² norm of its root is bounded by the root of 2 d times the size of the mean drop.

    source
    theorem HCPolySupport.HighContrast.Quenched.eLpNorm_diagonalWeakAverageSum_le_drops {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} (hstat : IsStationaryLaw P) {l : ℤ} {q : Mat d} (hgrid : IsRoundedGrid l q) {t : ℤ} (H : ℕ) {rho : ℝ} (hstart : l ≤ t - ↑H) (hintAll : ∀ (k : ℤ), HasFiniteAdaptedMean P q k) {F : BlockMat d} (hFsym : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) :
    MeasureTheory.eLpNorm (fun (a : CoeffSpace d) => Response.diagonalWeakAverageSum q t H (1 / 2) rho F a) 2 P ≤ ∑ j ∈ Finset.range (H + 1), ENNReal.ofReal (3 ^ (-(1 / 2 - rho / 2) * ↑j)) * ENNReal.ofReal √(2 * ↑d * blockSize (blockSub (adaptedMean P q (t - ↑j)) (adaptedMean P q t)) F)

    The rooted average sum by the mean drops alone. The L² norm of the weighted rooted average-defect sum is bounded by the weighted roots of the annealed mean drops — the sharp replacement for the crude per-cell variance budget in the printed weak estimate.