High-contrast homogenization: Provider.Quenched.SmallContrastSingleCellVarianceAbstract #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The single-cell variance at abstract envelopes #
The single-cell reference variance with both envelope inputs abstract:
the pathwise coarse-block envelope cPt·NSS^g·E and the mean envelope
c1·E, at an arbitrary normalized source variable and scale. The
burn-split (dimensional) constants instantiate directly: no boundary
constant, no grid-norm exponent in the statement.
theorem
HCPolySupport.HighContrast.Quenched.scaleVariance_le_of_envelopes
{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)
{n : Mat d}
(hn : Matrix.PosDef n)
(k : ℤ)
(hintk : HasFiniteAdaptedMean P (roundedGrid l n) k)
(F : BlockMat d)
(hFsym : IsSymmetricBlockMat F)
(hFpd : Book.Ch02.BlockPosDef F)
{S' : CoeffSpace d → ℝ}
(w : ℤ)
{cPt : ℝ}
(hcPt0 : 0 ≤ cPt)
(hpt' :
∀ᵐ (a : CoeffSpace d) ∂P, BlockMatLoewnerLE (coarseBlock (adaptedCell (roundedGrid l n) k) a)
(blockScale (cPt * normalizedSourceScale S' w a ^ g) E))
{c1 mu2 : ℝ}
(hc1Pt : cPt ≤ c1)
(hmu20 : 0 ≤ mu2)
(hmean : BlockMatLoewnerLE (adaptedMean P (roundedGrid l n) k) (blockScale c1 E))
(hmom : ∫⁻ (a : CoeffSpace d), ENNReal.ofReal (normalizedSourceScale S' w a ^ ↑2) ∂P ≤ ENNReal.ofReal mu2)
:
scaleVariance P (roundedGrid l n) F k ≤ ENNReal.ofReal ((2 * ↑d) ^ 2⁻¹ * blockSize E F * (2 * c1) * √mu2)
The single-cell variance at abstract envelopes.