High-contrast homogenization: Entry.Annealed.ReferenceNormalization

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

Annealed reference normalization

Under the standing stationary dagger law this module proves the annealed reference order, the two-grid reference normalization of adaptedMean, and the initialization sandwich on the source window. The reference order comes from the dagger at one sample and a sufficiently large standard cell through the two-sign characterization, so no standing-law conclusion needs a separate reference-order premise, and the normalization constants depend only on the dimension and the coarse exponent. These results serve p.global.selection, e.two.grid.source.normalization and p.initial.fixed.grid.scale.

The initialization conclusions retain the window restriction j ≤ 2 * jStar; the unrestricted range would require repeating the source construction at the larger window.

theorem HCPolySupport.HighContrast.Annealed.refBlock_reference_order {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {γ : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P γ E Ψ K S) : BlockMatLoewnerLE (ofFullBlockMat (toFullBlockMat (blockSwap d) * (toFullBlockMat E)⁻¹ * toFullBlockMat (blockSwap d))) E

Reference order from the dagger alone (p.global.selection). The probability measure supplies a sample in the coarse-bound event.

theorem HCPolySupport.HighContrast.Annealed.refBlock_le_six_aspectRatio_smul_swapConj {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {γ : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P γ E Ψ K S) : BlockMatLoewnerLE E (blockScale (6 * aspectRatio E) (ofFullBlockMat (toFullBlockMat (blockSwap d) * (toFullBlockMat E)⁻¹ * toFullBlockMat (blockSwap d))))

Standing-dagger corollary of the deterministic reference comparison.

theorem HCPolySupport.HighContrast.Annealed.aspectRatio_pos_and_three_le {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {γ : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P γ E Ψ K S) : 0 < aspectRatio E ∧ 3 ≤ 2 + aspectRatio E

Standing-dagger corollary of the deterministic reference comparison.

theorem HCPolySupport.HighContrast.Annealed.source_envelope_integral_le_two (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (X : CoeffSpace d → ℝ) (hX0 : ∀ (a : CoeffSpace d), 0 ≤ X a) (hlp : MeasureTheory.MemLp X (ENNReal.ofReal ↑(bigQ d γ)) P) (hnorm : MeasureTheory.eLpNorm X (ENNReal.ofReal ↑(bigQ d γ)) P ≤ ENNReal.ofReal 2) : ∫ (a : CoeffSpace d), X a ∂P ≤ 2

The envelope has expectation at most two on a probability space.

theorem HCPolySupport.HighContrast.Annealed.adaptedMean_refBlock_normalization (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (Csrc : ℝ) (C : ℝ), 0 < Csrc ∧ 0 < C ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ), IsStationaryLaw P → CoarseEllipticityDagger P γ E Ψ K S → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar → ∀ (m : Mat d), Matrix.PosDef m → ∀ (s : ℤ), ↑jStar ≤ s → adaptedCell (Geometry.explicitRoundedGrid jStar m) s ⊆ centeredCube d (2 * ↑jStar) → BlockMatLoewnerLE (adaptedMean P (Geometry.explicitRoundedGrid jStar m) s) (blockScale (C * √(‖m‖ * ‖m⁻¹‖)) E) ∧ BlockMatLoewnerLE E (blockScale (C * aspectRatio E * √(‖m‖ * ‖m⁻¹‖)) (adaptedMean P (Geometry.explicitRoundedGrid jStar m) s))

The two-grid annealed reference normalization, near e.two.grid.source.normalization. Both constants depend only on dimension and the coarse exponent.

theorem HCPolySupport.HighContrast.Annealed.initial_source_bounds (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (Csrc : ℝ), 0 < Csrc ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ), IsStationaryLaw P → CoarseEllipticityDagger P γ E Ψ K S → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar → ∀ (j : ℤ), ↑jStar ≤ j → j ≤ 2 * ↑jStar → BlockMatLoewnerLE (blockScale (1 / 2) (ofFullBlockMat (toFullBlockMat (blockSwap d) * (toFullBlockMat E)⁻¹ * toFullBlockMat (blockSwap d)))) (adaptedMean P 1 j) ∧ BlockMatLoewnerLE (adaptedMean P 1 j) (blockScale 2 E)

The exact initialization sandwich on the source window, p.initial.fixed.grid.scale. The printed uniform range is restricted to j ≤ 2 * jStar; a larger window requires repeating the multiplier construction.