High-contrast homogenization: Provider.Quenched.UnitRangeReferenceComparison

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

The reference block is dominated by the annealed block

The renormalization of ellipticity replaces the reference block of a coarse-ellipticity datum by the annealed block at an inner generation, and it converts the deviation it produces — which is measured against the reference block — into a deviation measured against the annealed one. That conversion is the comparison of the reference block with the annealed one.

The comparison has a short proof on this carrier. At its own generation the coarse-ellipticity datum puts the coarse block below the reference block on the event that the source has burnt in; the sharp map reverses that, and the pathwise block bounds put the sharp of a coarse block below the block itself, so the sharp of the reference block is below the coarse block on the same event. Averaging costs only the probability of that event, which the source tail keeps above one half, and the reference block is above its own sharp by the intrinsic reference ratio. Nothing in the argument sees a second generation, so no scale factor survives.

The annealed block as an average of quadratic forms

theorem HCPolySupport.HighContrast.Quenched.blockMatEntry_annealedBlock {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (U : Set (Vec d)) (α β : BlockCoord d) : blockMatEntry (annealedBlock P U) α β = ∫ (a : CoeffSpace d), blockMatEntry (coarseBlock U a) α β ∂P

The entries of the annealed block are the integrals of the entries.

theorem HCPolySupport.HighContrast.Quenched.integrable_blockVecDot_coarseBlock {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {U : Set (Vec d)} (hint : HasIntegrableCoarseBlock P U) (X : BlockVec d) : MeasureTheory.Integrable (fun (a : CoeffSpace d) => blockVecDot X (blockMatVecMul (coarseBlock U a) X)) P

The quadratic form of a coarse block is integrable as soon as its entries are.

theorem HCPolySupport.HighContrast.Quenched.blockVecDot_annealedBlock_eq_integral {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {U : Set (Vec d)} (hint : HasIntegrableCoarseBlock P U) (X : BlockVec d) : blockVecDot X (blockMatVecMul (annealedBlock P U) X) = ∫ (a : CoeffSpace d), blockVecDot X (blockMatVecMul (coarseBlock U a) X) ∂P

The quadratic form of the annealed block is the average of the quadratic forms.

Averaging a pathwise bound over an event

theorem HCPolySupport.HighContrast.Quenched.blockVecDot_nonneg_of_blockPosDef {d : ℕ} {H : BlockMat d} (hH : Book.Ch02.BlockPosDef H) (X : BlockVec d) : 0 ≤ blockVecDot X (blockMatVecMul H X)

The quadratic form of a positive block is nonnegative.

theorem HCPolySupport.HighContrast.Quenched.blockMatLoewnerLE_blockScale_annealedBlock_of_ae_on {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hvol : 0 < (MeasureTheory.volume U).toReal) (hint : HasIntegrableCoarseBlock P U) {B : BlockMat d} {G : Set (CoeffSpace d)} (hGmeas : MeasurableSet G) (hG : ∀ᵐ (a : CoeffSpace d) ∂P, a ∈ G → BlockMatLoewnerLE B (coarseBlock U a)) : BlockMatLoewnerLE (blockScale (P.real G) B) (annealedBlock P U)

A pathwise Loewner bound valid on an event survives averaging, at the cost of the probability of that event.

The comparison

theorem HCPolySupport.HighContrast.Quenched.blockMatLoewnerLE_blockScale_annealedBlock_reference {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Psi : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Psi K S) (l : ℤ) (hint : HasIntegrableCoarseBlock P (centeredCube d l)) (hhalf : (Psi (3 ^ l))⁻¹ ≤ 1 / 2) : BlockMatLoewnerLE E (blockScale (2 * kappaRef E) (annealedBlock P (centeredCube d l)))

The reference block is dominated by the annealed block. On the event that the source has burnt in at the generation l, the coarse-ellipticity datum puts the coarse block below the reference block; the sharp map reverses that and the pathwise block bounds close the loop, so the reference block is below twice its intrinsic reference ratio times the annealed block, as soon as the source tail at 3^l is at most one half.