High-contrast homogenization: Provider.Quenched.UnitRangeBlockReassembly

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

From entrywise deviations to the Loewner order

The concentration estimate produced by unit range is a statement about scalar observables; the renormalization of ellipticity consumes a statement in the Loewner order of doubled blocks. This file performs the passage between them, in the two directions the argument needs.

Downwards, a coarse-ellipticity datum bounds the entries of a coarse block on the event that the source has burnt in, which is what makes the cutoff of the truncation argument inactive there: the truncated readout is then the readout itself, so no truncation error is incurred on the event where the estimate is used.

Upwards, entrywise bounds on a doubled block give a Loewner bound against any reference block dominating the identity, at the cost of the factor 2d — the number of coordinates of a doubled block. Combining that with the concentration estimate, applied once to each of the 4d² entries and collected by a union bound, gives the block-level deviation estimate.

The cutoff is inactive on the source event

Entrywise bounds give a Loewner bound

theorem HCPolySupport.HighContrast.Quenched.card_blockCoord (d : ℕ) : Finset.univ.card = 2 * d

The number of coordinates of a doubled block.

theorem HCPolySupport.HighContrast.Quenched.blockMatLoewnerLE_blockScale_of_abs_blockMatEntry_le {d : ℕ} {H F : BlockMat d} {eta : ℝ} (heta : 0 ≤ eta) (hF : ∀ (X : BlockVec d), ∑ α : BlockCoord d, toFullBlockVec X α * toFullBlockVec X α ≤ blockVecDot X (blockMatVecMul F X)) (hH : ∀ (α β : BlockCoord d), |blockMatEntry H α β| ≤ eta) : BlockMatLoewnerLE H (blockScale (2 * ↑d * eta) F)

Entrywise bounds give a Loewner bound. A doubled block whose entries are bounded by η is dominated by 2dη times any reference block that dominates the identity form.

The block-level deviation estimate

theorem HCPolySupport.HighContrast.Quenched.measureReal_not_blockMatLoewnerLE_le {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsFiniteMeasure P] {H : CoeffSpace d → BlockMat d} {F : BlockMat d} {eta p : ℝ} (heta : 0 ≤ eta) (hF : ∀ (X : BlockVec d), ∑ α : BlockCoord d, toFullBlockVec X α * toFullBlockVec X α ≤ blockVecDot X (blockMatVecMul F X)) (hent : ∀ (α β : BlockCoord d), P.real {a : CoeffSpace d | eta < |blockMatEntry (H a) α β|} ≤ p) : P.real {a : CoeffSpace d | ¬BlockMatLoewnerLE (H a) (blockScale (2 * ↑d * eta) F)} ≤ (2 * ↑d) ^ 2 * p

The reassembly. If every entry of a block-valued observable stays below η outside an event of probability p, the block itself stays below 2dη times the reference block outside an event of probability 4d²p.

theorem HCPolySupport.HighContrast.Quenched.measureReal_not_blockMatLoewnerLE_average_le_frGauge {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (hP : IsUnitRangeLaw P) {k : ℤ} (hk : 0 ≤ k) {X : BlockCoord d → BlockCoord d → (Fin d → ℤ) → CoeffSpace d → ℝ} (hXloc : ∀ (α β : BlockCoord d) (w : Fin d → ℤ), Measurable (X α β w)) (hXbd : ∀ (α β : BlockCoord d) (w : Fin d → ℤ), ∀ᵐ (a : CoeffSpace d) ∂P, |X α β w a| ≤ 1) (hXmean : ∀ (α β : BlockCoord d) (w : Fin d → ℤ), ∫ (a : CoeffSpace d), X α β w a ∂P = 0) {Z : Finset (Fin d → ℤ)} (hZ : Z.Nonempty) {H : CoeffSpace d → BlockMat d} (hH : ∀ (a : CoeffSpace d) (α β : BlockCoord d), blockMatEntry (H a) α β = (↑Z.card)⁻¹ * ∑ w ∈ Z, X α β w a) {F : BlockMat d} (hF : ∀ (Y : BlockVec d), ∑ α : BlockCoord d, toFullBlockVec Y α * toFullBlockVec Y α ≤ blockVecDot Y (blockMatVecMul F Y)) {t : ℝ} (ht : 1 ≤ t) : P.real {a : CoeffSpace d | ¬BlockMatLoewnerLE (H a) (blockScale (2 * ↑d * (frThreshold d * t * (√↑Z.card)⁻¹)) F)} ≤ (2 * ↑d) ^ 2 * (frGauge d t)⁻¹

The block-level concentration estimate. A block-valued observable whose entries are the averages of centred local readouts bounded by one obeys the finite-range Gaussian tail in the Loewner order, at the fluctuation scale N^{-1/2} and with the factor 2d of the reassembly.