High-contrast homogenization: Entry.Multiscale.Initial.Nonnegativity

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

Initialization: nonnegativity and order on the Euclidean grid

The profile, its fluctuation and mean histories, and the determinant drift are nonnegative at the Euclidean grid, and the normalized mean is antitone in its left generation. These are the order facts the crude bound of p.initial.fixed.grid.scale and the logarithmic decrement e.initial.log.decrement consume.

C. Nonnegativity and order on the Euclidean grid

theorem HCPolySupport.HighContrast.Multiscale.fluctuationHistory_nonneg {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (γ : ℝ) (q : Mat d) (jStar : ℕ) (m : ℤ) : 0 ≤ fluctuationHistory P γ q jStar m

C1. The fluctuation history is a nonnegative real.

theorem HCPolySupport.HighContrast.Multiscale.normalizedMean_one_antitone_left (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (_hγ : γ ∈ Set.Ico 0 1) (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (Src : CoeffSpace d → ℝ) : MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P γ E Ψ K Src → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ∀ (i j m : ℤ), ↑jStar ≤ i → i ≤ j → BlockMatLoewnerLE (relMean P 1 j m) (relMean P 1 i m)

C3. P^Id_{j,m} is antitone in the first index (congruence of the annealed order).

theorem HCPolySupport.HighContrast.Multiscale.determinantDrift_one_nonneg (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (_hγ : γ ∈ Set.Ico 0 1) (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (Src : CoeffSpace d → ℝ) : MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P γ E Ψ K Src → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ∀ (m : ℤ), 0 ≤ determinantDrift P γ 1 jStar m

C4. The Euclidean drift is nonnegative (p.initial.fixed.grid.scale).

theorem HCPolySupport.HighContrast.Multiscale.profile_one_nonneg (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (Src : CoeffSpace d → ℝ) : MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P γ E Ψ K Src → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ∀ (n m : ℤ), ↑jStar ≤ n → n ≤ m → 0 ≤ profile P γ 1 jStar n m

C5. The Euclidean profile is nonnegative.