High-contrast homogenization: Provider.Quenched.AnnealedContrastAntitone #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Monotonicity of the annealed contrast #
The intrinsic contrast decreases when a symmetric positive doubled block decreases in Loewner order. Applied to the annealed coarse blocks, this gives the generation monotonicity used when a law is rebased at a later triadic scale.
theorem
HCPolySupport.HighContrast.Quenched.blockContrast_le_of_blockMatLoewnerLE
{d : ℕ}
{A E : BlockMat d}
(hAsymm : IsSymmetricBlockMat A)
(hApos : Book.Ch02.BlockPosDef A)
(hEsymm : IsSymmetricBlockMat E)
(hEpos : Book.Ch02.BlockPosDef E)
(hle : BlockMatLoewnerLE A E)
:
The intrinsic contrast is monotone for the quadratic-form order on symmetric positive doubled blocks.
theorem
HCPolySupport.HighContrast.Quenched.annealedContrast_le_of_nonneg_of_le
{d : ℕ}
[NeZero d]
{P : MeasureTheory.Measure (CoeffSpace d)}
[MeasureTheory.IsProbabilityMeasure P]
{g : ℝ}
{E : BlockMat d}
{Ψ : ℝ → ℝ}
{K : ℝ}
{S : CoeffSpace d → ℝ}
(hstat : IsStationaryLaw P)
(hdag : CoarseEllipticityDagger P g E Ψ K S)
{j p : ℤ}
(hj : 0 ≤ j)
(hjp : j ≤ p)
:
The annealed intrinsic contrast decreases between nonnegative Euclidean generations.
theorem
HCPolySupport.HighContrast.Quenched.annealedContrast_antitone
{d : ℕ}
[NeZero d]
{P : MeasureTheory.Measure (CoeffSpace d)}
[MeasureTheory.IsProbabilityMeasure P]
{g : ℝ}
{E : BlockMat d}
{Ψ : ℝ → ℝ}
{K : ℝ}
{S : CoeffSpace d → ℝ}
(hstat : IsStationaryLaw P)
(hdag : CoarseEllipticityDagger P g E Ψ K S)
:
Antitone fun (n : ℕ) => annealedContrast P ↑n
The annealed intrinsic contrast is antitone along the natural-number generations.
theorem
HCPolySupport.HighContrast.Quenched.annealedContrast_triadicRebasedLaw_zero_sub_one_le_of_le
{d : ℕ}
[NeZero d]
{P : MeasureTheory.Measure (CoeffSpace d)}
[MeasureTheory.IsProbabilityMeasure P]
{g : ℝ}
{E : BlockMat d}
{Ψ : ℝ → ℝ}
{K : ℝ}
{S : CoeffSpace d → ℝ}
(hstat : IsStationaryLaw P)
(hdag : CoarseEllipticityDagger P g E Ψ K S)
{mEnt nBase : ℕ}
(hmn : mEnt ≤ nBase)
{cStar : ℝ}
(hsmall : annealedContrast P ↑mEnt - 1 ≤ cStar)
:
Small contrast at an entry generation remains valid at generation zero of a law rebased at any later generation.