High-contrast homogenization: Entry.Annealed.BridgeComparisonsOneSided

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

The two one-sided Whitney comparisons

p.successful.short.bridge. Countable subadditivity uses response quadratics on the open parent and its open cells. A single locally elliptic representative serves the entire partition. The null remainder is never an argument of coarseBlock.

The companion module BridgeComparisons holds the shared partition-comparison machinery. Here the two comparisons themselves are proved: the forward comparison bounds the Loewner difference of the new and old adapted means by the old-grid quadratic sum together with a locally elliptic term, and the reverse comparison is the matching bound in the opposite direction, with the packed new cells at n + L and the old boundary rows running up to that cap. The cap-row mass bound gives the summability of the boundary row masses on which the countable subadditivity argument rests. The quadratic identities bridge_enlarge_quadratic_smul and bridge_enlarge_quadratic_add record the scaling and additivity of the response quadratic.

theorem HCPolySupport.HighContrast.Annealed.bridge_whitney_cap_mass_le_one {d : ℕ} [NeZero d] (W : Set (Vec d)) (q : Mat d) (hq : IsUnit q) (cap : ℤ) (hW : MeasureTheory.volume W ≠ ⊤) (hfin : ∀ r ≤ cap, (maximalAdaptedCellCenters W q cap r).Finite) (hwt : ∑' (r : { r : ℤ // r ≤ cap }), ∑ _z ∈ ⋯.toFinset, (MeasureTheory.volume (adaptedCell q ↑r)).toReal / (MeasureTheory.volume W).toReal = 1) : ∑ _z ∈ ⋯.toFinset, (MeasureTheory.volume (adaptedCell q cap)).toReal / (MeasureTheory.volume W).toReal ≤ 1

The forward cap row has mass at most one. Summability is obtained from finite volume before the full mass identity is used.

theorem HCPolySupport.HighContrast.Annealed.bridge_upper_comparison (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) → BlockMatLoewnerLE (blockSub (adaptedMean P (Geometry.explicitRoundedGrid jStar mPlus) (n + ↑L)) (adaptedMean P (Geometry.explicitRoundedGrid jStar m) n)) (ofFullBlockMat (toFullBlockMat (blockScale (C * K₀) (ofFullBlockMat (∑ r ∈ Finset.Icc (↑jStar) n, 3 ^ (↑r - ↑n - ↑L) • toFullBlockMat (adaptedMean P (Geometry.explicitRoundedGrid jStar m) r)))) + toFullBlockMat (blockScale (C * (1 + aspectRatio E * (√(‖m‖ * ‖m⁻¹‖) + √(‖mPlus‖ * ‖mPlus⁻¹‖)) ^ 2) * 3 ^ (-(1 - γ) * (↑n + ↑L - ↑jStar))) (adaptedMean P (Geometry.explicitRoundedGrid jStar m) (n + 2 * ↑L)))))

The forward Whitney comparison, e.bridge.upper.comparison. The old-grid sum ends at n; its parent is the new cell at n+L.

theorem HCPolySupport.HighContrast.Annealed.bridge_lower_comparison (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) → BlockMatLoewnerLE (blockSub (adaptedMean P (Geometry.explicitRoundedGrid jStar m) (n + 2 * ↑L)) (adaptedMean P (Geometry.explicitRoundedGrid jStar mPlus) (n + ↑L))) (ofFullBlockMat (toFullBlockMat (blockScale (C * K₀) (ofFullBlockMat (∑ r ∈ Finset.Icc (↑jStar) (n + ↑L), 3 ^ (↑r - ↑n - 2 * ↑L) • toFullBlockMat (adaptedMean P (Geometry.explicitRoundedGrid jStar m) r)))) + toFullBlockMat (blockScale (C * (1 + aspectRatio E * (√(‖m‖ * ‖m⁻¹‖) + √(‖mPlus‖ * ‖mPlus⁻¹‖)) ^ 2) * 3 ^ (-(1 - γ) * (↑n + 2 * ↑L - ↑jStar))) (adaptedMean P (Geometry.explicitRoundedGrid jStar m) (n + 2 * ↑L)))))

The reverse Whitney comparison, e.bridge.lower.comparison. The packed new cells are at n+L; the old boundary rows include that cap.