High-contrast homogenization: Provider.Quenched.UnitRangeBlockCutoff

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

The local block cutoff

The concentration estimate needs an observable that is bounded, local to its own cell, below the coarse block at every sample, and equal to the coarse block on the event that the source has burnt in. The printed argument uses a smooth spectral cutoff of the normalized block; the smoothness is there only to bound the multiplicative derivative that the printed mixing hypothesis asks for, and unit range supplies exact independence instead.

On this carrier the cutoff may therefore be taken to be the hard one that keeps the block when all of its entries respect a threshold and discards it otherwise. It is local, because the branch condition is a finite conjunction of conditions on entries that are already known to be local; it is bounded by the threshold; it is below the block at every sample, the discarded branch being the zero block and the coarse block being positive; and the coarse-ellipticity datum makes the branch condition hold on the burnt-in event, so nothing is discarded there.

The cutoff

noncomputable def HCPolySupport.HighContrast.Quenched.blockCutoff {d : ℕ} (B : ℝ) (H : BlockMat d) : BlockMat d

The local block cutoff at the level B: the block itself when every entry respects the level, and the zero block otherwise.

Equations

• HCPolySupport.HighContrast.Quenched.blockCutoff B H = if ∀ (α β : HCPolySupport.BlockCoord d), |HCPolySupport.blockMatEntry H α β| ≤ B then H else HCPolySupport.HighContrast.blockScale 0 H

theorem HCPolySupport.HighContrast.Quenched.blockMatEntry_blockCutoff {d : ℕ} (B : ℝ) (H : BlockMat d) (α β : BlockCoord d) : blockMatEntry (blockCutoff B H) α β = if ∀ (α' β' : BlockCoord d), |blockMatEntry H α' β'| ≤ B then blockMatEntry H α β else 0

theorem HCPolySupport.HighContrast.Quenched.blockCutoff_eq_self {d : ℕ} {B : ℝ} {H : BlockMat d} (h : ∀ (α β : BlockCoord d), |blockMatEntry H α β| ≤ B) : blockCutoff B H = H

The cutoff keeps the block when the level is respected.

theorem HCPolySupport.HighContrast.Quenched.abs_blockMatEntry_blockCutoff_le {d : ℕ} {B : ℝ} (hB : 0 ≤ B) (H : BlockMat d) (α β : BlockCoord d) : |blockMatEntry (blockCutoff B H) α β| ≤ B

The cutoff respects its level.

theorem HCPolySupport.HighContrast.Quenched.blockMatLoewnerLE_blockCutoff {d : ℕ} {B : ℝ} {H : BlockMat d} (hH : Book.Ch02.BlockPosDef H) : BlockMatLoewnerLE (blockCutoff B H) H

The cutoff is below the block at every sample.

Locality

The cutoff is inactive on the burnt-in event

Integrability