High-contrast homogenization: Provider.Quenched.SmallContrastBootstrapTilt

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

The bootstrap tilt bridge

The tilt scalarization reads a one-sided Loewner adapter error against the reference block as a multiplicative comparison of intrinsic contrasts. The bootstrap consumes it in the Euclidean direction: the adapted mean on the selection grid at generation n is compared with the annealed block of a centered cube at a strictly earlier scale k, the cube being presented as the adapted cell of the Euclidean rounded grid.

Two scalar inputs enter: the absorbed adapter size η = c·|𝐄 : 𝐀(□_k)| and the Euclidean hatted defect x = d(hatΘ_k − 1). The output is the same degree-two polynomial the scalarization produces, evaluated at any upper bounds for those two — the hatted carrier of the adapted mean sits below its intrinsic contrast, so the polynomial bounds the hatted defect on the selection grid as well.

noncomputable def HCPolySupport.HighContrast.Quenched.bootstrapTiltPolynomial (sigma x : ℝ) : ℝ

The bootstrap tilt polynomial (1+σ)²(1 + (5/4)x + (1/4)x²) − 1: the scalarized adapter comparison at absorbed size σ and Euclidean hatted defect x.

Equations

• HCPolySupport.HighContrast.Quenched.bootstrapTiltPolynomial sigma x = (1 + sigma) ^ 2 * (1 + 5 / 4 * x + 1 / 4 * x ^ 2) - 1

theorem HCPolySupport.HighContrast.Quenched.bootstrapTiltPolynomial_le {s t x y : ℝ} (hs : 0 ≤ s) (hst : s ≤ t) (hx : 0 ≤ x) (hxy : x ≤ y) : bootstrapTiltPolynomial s x ≤ bootstrapTiltPolynomial t y

The tilt polynomial is monotone in both arguments on the nonnegative quadrant.

theorem HCPolySupport.HighContrast.Quenched.adaptedHattedContrast_sub_one_le_of_euclidean_adapter {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {E : BlockMat d} (hEsymm : IsSymmetricBlockMat E) (hEpos : Book.Ch02.BlockPosDef E) {lq : ℤ} {q : Mat d} (hq : IsRoundedGrid lq q) {k n : ℤ} (hfinq : HasFiniteAdaptedMean P q n) (hfin1 : HasFiniteAdaptedMean P 1 k) {c : ℝ} (hc : 0 ≤ c) (hsub : BlockMatLoewnerLE (blockSub (adaptedMean P q n) (annealedBlock P (centeredCube d k))) (blockScale c E)) {sigma x : ℝ} (heta : c * blockSize E (adaptedMean P 1 k) ≤ sigma) (hx : ↑d * (adaptedHattedContrast P 1 k - 1) ≤ x) : ↑d * (adaptedHattedContrast P q n - 1) ≤ ↑d * bootstrapTiltPolynomial sigma x

The bootstrap tilt bridge. A one-sided adapter error against the reference block, from the adapted mean at generation n down to the annealed block of the centered cube at scale k, bounds the hatted defect of the adapted mean by the tilt polynomial at any upper bounds σ for the absorbed adapter size and x for the Euclidean hatted defect.