High-contrast homogenization: Entry.Annealed.BridgeBoundarySum

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

The boundary sum, drift advance, and normalization sandwich

p.successful.short.bridge. The boundary estimate retains 1-(1-γ)/8 through a separate maximum-weight inequality. Empty integer intervals are allowed. Every inverse normalization uses a positive definite actual annealed mean.

theorem HCPolySupport.HighContrast.Annealed.bridge_boundary_weight_split {a L t : ℝ} (ha : a ∈ Set.Icc 0 1) : 3 ^ (-max L t) ≤ 3 ^ (-(1 - a) * L) * 3 ^ (-a * t)

Both branches of the maximum split retain the printed boundary exponent.

theorem HCPolySupport.HighContrast.Annealed.bridge_unnormalize_order {d : ℕ} {A B F : BlockMat d} (hA : Matrix.IsHermitian (toFullBlockMat A)) (hB : Matrix.IsHermitian (toFullBlockMat B)) (hF : Matrix.PosDef (toFullBlockMat F)) (h : BlockMatLoewnerLE (normalizedBlock A F) (normalizedBlock B F)) : BlockMatLoewnerLE A B

Removing a positive definite normalization preserves the quadratic order. The inverse is used only after its nonsingularity has been established.

theorem HCPolySupport.HighContrast.Annealed.bridge_increment_trace_bound {d : ℕ} (H F : BlockMat d) (hH : Matrix.PosSemidef (toFullBlockMat H)) (hF : Matrix.PosDef (toFullBlockMat F)) : 0 ≤ blockTrace (normalizedBlock H F) ∧ BlockMatLoewnerLE H (blockScale (blockTrace (normalizedBlock H F)) F)

A positive increment is bounded by the trace of its normalization, times the normalizer. This is the full matrix increment used in the boundary sum.

theorem HCPolySupport.HighContrast.Annealed.bridge_boundary_sum (d : ℕ) (hd : 2 ≤ d) (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ) (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P γ E Ψ K S) (jStar : ℕ) (hj : 2 * d ≤ 3 ^ jStar) (m : Mat d) (hm : Matrix.PosDef m) (j : ℤ) (L : ℕ) : BlockMatLoewnerLE (ofFullBlockMat (∑ r ∈ Finset.Icc (↑jStar) (j - ↑L), 3 ^ (↑r - ↑j) • toFullBlockMat (adaptedMean P (Geometry.explicitRoundedGrid jStar m) r))) (blockScale (3 / 2 * (3 ^ (-↑L) + 3 ^ (-(1 - (1 - γ) / 8) * ↑L) * determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar j)) (adaptedMean P (Geometry.explicitRoundedGrid jStar m) j))

e.bridge.boundary.sum, with an explicit universal geometric constant. This holds also for an empty generation interval and for L=0.

theorem HCPolySupport.HighContrast.Annealed.bridge_determinantDrift_nonneg (d : ℕ) (hd : 2 ≤ d) (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (γ : ℝ) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ) (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P γ E Ψ K S) (jStar : ℕ) (hj : 2 * d ≤ 3 ^ jStar) (m : Mat d) (hm : Matrix.PosDef m) (n : ℤ) : 0 ≤ determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar n

The actual determinant drift is nonnegative; positivity of its normalized increments is proved before reading the real sum. Empty ranges need no exception.

theorem HCPolySupport.HighContrast.Annealed.bridge_drift_advance_pair (d : ℕ) (hd : 2 ≤ d) (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ) (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P γ E Ψ K S) (jStar : ℕ) (hj : 2 * d ≤ 3 ^ jStar) (m : Mat d) (hm : Matrix.PosDef m) (n : ℤ) (hn : ↑jStar ≤ n) (L : ℕ) (hL : 1 ≤ L) (ε : ℝ) (hε : ε ∈ Set.Icc 0 1) (hD : determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar n ≤ ε) (hΔ : detIncrement P (Geometry.explicitRoundedGrid jStar m) n (n + 2 * ↑L) ≤ ε) : have Δ := detIncrement P (Geometry.explicitRoundedGrid jStar m) n (n + 2 * ↑L); have δ := Real.exp ((↑d)⁻¹ * Δ) - 1; δ ∈ Set.Icc 0 1 ∧ δ ≤ 2 * ε ∧ (1 + δ) ^ d = Real.exp Δ ∧ Real.exp Δ - 1 ≤ 2 * ε ∧ determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar (n + ↑L) + determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar (n + 2 * ↑L) ≤ 10 * ε

The printed drift advance is applied at both lengths, with the intermediate loss controlled using nonnegative loss on [n+L,n+2L]. All constants are numerical.

theorem HCPolySupport.HighContrast.Annealed.bridge_mean_sandwich (d : ℕ) (hd : 2 ≤ d) (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (γ : ℝ) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ) (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P γ E Ψ K S) (jStar : ℕ) (hj : 2 * d ≤ 3 ^ jStar) (m : Mat d) (hm : Matrix.PosDef m) (n : ℤ) (hn : ↑jStar ≤ n) (L : ℕ) : have q := Geometry.explicitRoundedGrid jStar m; have F := adaptedMean P q (n + 2 * ↑L); BlockMatLoewnerLE F (adaptedMean P q (n + ↑L)) ∧ BlockMatLoewnerLE (adaptedMean P q (n + ↑L)) (adaptedMean P q n) ∧ BlockMatLoewnerLE (adaptedMean P q n) (blockScale (Real.exp (detIncrement P q n (n + 2 * ↑L))) F)

The three means in the old grid share the terminal normalizer. The upper factor is the exponential of the unscaled log-determinant loss.

theorem HCPolySupport.HighContrast.Annealed.bridge_endpoint_errors (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (K₀ : ℝ) (hK₀ : 1 ≤ K₀) : ∃ (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 mPlus : Mat d), Matrix.PosDef m → Matrix.PosDef mPlus → gridRatio (Geometry.explicitRoundedGrid jStar m) (Geometry.explicitRoundedGrid jStar mPlus) ≤ K₀ → ∀ (n : ℤ) (L : ℕ), ↑jStar ≤ n → 1 ≤ L → adaptedCell (Geometry.explicitRoundedGrid jStar m) (n + 2 * ↑L) ∪ adaptedCell (Geometry.explicitRoundedGrid jStar mPlus) (n + ↑L) ⊆ centeredCube d (2 * ↑jStar) → ∀ ε ∈ Set.Icc 0 1, determinantDrift P γ (Geometry.explicitRoundedGrid jStar m) jStar n ≤ ε → detIncrement P (Geometry.explicitRoundedGrid jStar m) n (n + 2 * ↑L) ≤ ε → have F := adaptedMean P (Geometry.explicitRoundedGrid jStar m) (n + 2 * ↑L); have H := adaptedMean P (Geometry.explicitRoundedGrid jStar mPlus) (n + ↑L); have T := (1 + aspectRatio E * (√(‖m‖ * ‖m⁻¹‖) + √(‖mPlus‖ * ‖mPlus⁻¹‖)) ^ 2) * (1 + ↑n + ↑L - ↑jStar) * 3 ^ (-((1 - γ) / 8) * (↑n - ↑jStar)); BlockMatLoewnerLE (blockSub H F) (blockScale (C * ε + C * K₀ * 3 ^ (-↑L) + C * T) F) ∧ BlockMatLoewnerLE (blockSub F H) (blockScale (C * ε + C * K₀ * 3 ^ (-↑L) + C * T) F)

Both actual Whitney errors relative to the terminal old-grid mean. The boundary decay retains 1-(1-γ)/8; the source tail is enlarged only after the three-generation sandwich and the two drift advances have been established.