High-contrast homogenization: Provider.Quenched.SmallContrastMomentCollapse #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The moment collapse past the burn-in #
The shared interface for the free-threshold wave: past the burn-in depth,
the deepened moment excess is at most one, so the deepened first moment is
at most 2 and the deepened second moment integrates to at most 2.
The burn-in condition transports monotonically to deeper anchors.
theorem
HCPolySupport.HighContrast.Quenched.burn_condition_mono
{K : ℝ}
{M : ℕ}
{sKw jb w : ℤ}
{Gacc : ℕ}
(hjw : jb ≤ w)
(hburn :
1 + 2 * ↑(2 + M) * (1 + Real.log (growthBar K)) * growthBar K ^ IndependentSums.natTriangular (2 + M) ≤ 3 ^ (↑M * ↑(jb + ↑(Gacc + 1) - 1 - sKw)))
:
The burn-in condition transports to any deeper anchor.
The crude moment constants are monotone in the order.
theorem
HCPolySupport.HighContrast.Quenched.deepened_excess_le_one
{K : ℝ}
{M : ℕ}
{sKw w : ℤ}
{Gacc : ℕ}
(hburnW :
1 + 2 * ↑(2 + M) * (1 + Real.log (growthBar K)) * growthBar K ^ IndependentSums.natTriangular (2 + M) ≤ 3 ^ (↑M * ↑(w + ↑(Gacc + 1) - 1 - sKw)))
:
Past the burn-in, the decayed excess at either order is at most one.
theorem
HCPolySupport.HighContrast.Quenched.lintegral_nss_sq_collapsed
{d : ℕ}
{g : ℝ}
{P : MeasureTheory.Measure (CoeffSpace d)}
[MeasureTheory.IsProbabilityMeasure P]
{E : BlockMat d}
{Ψ : ℝ → ℝ}
{K : ℝ}
{S : CoeffSpace d → ℝ}
(hdag : CoarseEllipticityDagger P g E Ψ K S)
{sKw : ℤ}
(hsKw : growthBar K ≤ 3 ^ sKw)
(w : ℤ)
{Gacc : ℕ}
(M : ℕ)
(hDw : 0 ≤ w + ↑(Gacc + 1) - 1 - sKw)
(hburnW :
1 + 2 * ↑(2 + M) * (1 + Real.log (growthBar K)) * growthBar K ^ IndependentSums.natTriangular (2 + M) ≤ 3 ^ (↑M * ↑(w + ↑(Gacc + 1) - 1 - sKw)))
:
∫⁻ (a : CoeffSpace d), ENNReal.ofReal (normalizedSourceScale S (w + ↑(Gacc + 1) - 1) a ^ ↑2) ∂P ≤ ENNReal.ofReal 2
The collapsed second moment: past the burn-in, the second moment of
the normalized source scale at the window top is at most 2.