High-contrast homogenization: Annealed.SourceIntegrability #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The source scale has a first moment #
The gauge tail bound of e.coarse.ellipticity together with the growth
witness t Ψ(t) ≤ Ψ(K t) forces the gauge to outgrow every polynomial, so the
source scale is integrable over the law. This is the probabilistic half of the
argument that makes the annealed block an honest expectation at every scale.
theorem
HCPolySupport.HighContrast.hasPsiGrowth_mono
{Ψ : ℝ → ℝ}
{K K' : ℝ}
(hadm : IndependentSums.AdmissiblePsi Ψ)
(hK : 1 ≤ K)
(hKK' : K ≤ K')
(hgrow : IndependentSums.HasPsiGrowth Ψ K)
:
The growth witness of a gauge may be enlarged.
theorem
HCPolySupport.HighContrast.integrable_source_of_coarseEllipticityDagger
{d : ℕ}
{P : MeasureTheory.Measure (CoeffSpace d)}
[MeasureTheory.IsProbabilityMeasure P]
{g : ℝ}
{E : BlockMat d}
{Ψ : ℝ → ℝ}
{K : ℝ}
{S : CoeffSpace d → ℝ}
(hdag : CoarseEllipticityDagger P g E Ψ K S)
:
The source scale is integrable. The gauge tail bound of
e.coarse.ellipticity together with the growth witness makes the tail of the
source integrable.