High-contrast homogenization: Provider.Quenched.SmallContrastEntryEnvelope

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

The entry-collapsed annealed envelope

Past the source burn-in — once the generation cube exceeds the burn scale by the logarithm of the second source moment — the annealed envelope's gauge cost collapses to a factor 2: the good event contributes the deterministic dagger envelope, and the bad event's first moment is dominated by the second moment divided by the (geometrically large) threshold. This is the formalized counterpart of the printed entry step (HC (4.18) and the mesoscale choice h' ~ log Π): every excess-multiplying constant of the recursion becomes dimensional after a polynomial entry delay, while the source-moment constants retreat into decaying terms and the delay itself.

theorem HCPolySupport.HighContrast.Quenched.integral_sq_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 ^ 2 ∂P ≤ sourceMomentTwo K

The second moment of the normalized source scale.

theorem HCPolySupport.HighContrast.Quenched.integrable_sq_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 (fun (a : CoeffSpace d) => normalizedSourceScale S sK a ^ 2) P

The square of the normalized source scale is integrable.

theorem HCPolySupport.HighContrast.Quenched.annealedBlock_adaptedCell_le_scaled_entry {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) (hentry : sourceMomentTwo K ≤ 3 ^ (t + ↑G - 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 (2 * boundaryConst Cd g n * 3 ^ (g * (↑(t + ↑G) - ↑k))) E)

The entry-collapsed annealed envelope: past the burn-in by the logarithm of the second source moment, the annealed aligned cell is dominated by the reference with the deterministic scale-adapted factor and the absolute constant 2.