High-contrast homogenization: Provider.Quenched.SmallContrastAnnealedEnvelope

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

The annealed scaled envelope

Integrating the pathwise scale-adapted source envelope over the law bounds every annealed aligned cell by the reference block with the deterministic factor C(K) · boundaryConst · 3^{g(t+G−k)}: the random burn overshoot has a first moment bounded by the crude-moment constant. This is the deterministic envelope that makes the deep legs of the hatted rows summable against the 3^{(3/2)(k−s)} weights.

noncomputable def HCPolySupport.HighContrast.Quenched.sourceMomentOne (K : ℝ) : ℝ

The crude-moment constant of order one.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.Quenched.one_le_sourceMomentOne {K : ℝ} : 1 ≤ sourceMomentOne K

theorem HCPolySupport.HighContrast.Quenched.integral_normalizedSourceScale_le {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) {sK : ℤ} (hsK : growthBar K ≤ 3 ^ sK) : ∫ (a : CoeffSpace d), normalizedSourceScale S sK a ∂P ≤ sourceMomentOne K

The first moment of the normalized source scale.

theorem HCPolySupport.HighContrast.Quenched.integrable_normalizedSourceScale {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) {sK : ℤ} (hsK : growthBar K ≤ 3 ^ sK) : MeasureTheory.Integrable (normalizedSourceScale S sK) P

The normalized source scale is integrable.

theorem HCPolySupport.HighContrast.Quenched.annealedBlock_adaptedCell_le_scaled {d : ℕ} [NeZero d] (hd : 2 ≤ d) {g : ℝ} (hg : g ∈ Set.Ico 0 1) {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) {l : ℤ} (hl : ↑(kZero d) ≤ l) {Cd : ℝ} (hCd : max 1 (12 * ↑d * √↑d) ≤ Cd) {n : Mat d} (hn : Matrix.PosDef n) {sK : ℤ} (hsK : growthBar K ≤ 3 ^ sK) {k : ℤ} {w : Fin d → ℤ} (t : ℤ) {G : ℕ} (hDelta : 0 ≤ t + ↑G - 1 - sK) (hsub : adaptedCellAt (roundedGrid l n) k w ⊆ centeredCube d (t + ↑G)) (hint : HasIntegrableCoarseBlock P (adaptedCellAt (roundedGrid l n) k w)) : BlockMatLoewnerLE (annealedBlock P (adaptedCellAt (roundedGrid l n) k w)) (blockScale (sourceMomentOne K * boundaryConst Cd g n * 3 ^ (g * (↑(t + ↑G) - ↑k))) E)

The annealed scaled envelope: every annealed aligned cell contained in the generation cube is dominated by the reference with the deterministic scale-adapted factor.