High-contrast homogenization: Entry.Annealed.BridgeComparisons

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

The common partition comparison

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. This file assembles bridge_partition_comparison, the shared machinery behind the two one-sided Whitney comparisons, which BridgeComparisonsOneSided carries as bridge_upper_comparison and bridge_lower_comparison.

The supporting estimates are inherited through BridgeSourceTail.

theorem HCPolySupport.HighContrast.Annealed.bridge_quadratic_sum {d : ℕ} {ι : Type u_1} (s : Finset ι) (F : ι → FullBlockMat d) (v : BlockVec d) : 1 / 2 * blockVecDot v (blockMatVecMul (ofFullBlockMat (∑ i ∈ s, F i)) v) = ∑ i ∈ s, 1 / 2 * blockVecDot v (blockMatVecMul (ofFullBlockMat (F i)) v)

Quadratic evaluation distributes over a finite sum of full blocks.

theorem HCPolySupport.HighContrast.Annealed.bridge_annealed_partition_bound {d : ℕ} [NeZero d] {ι : Type u_1} {s : Set ι} (hs : s.Countable) (P : MeasureTheory.Measure (CoeffSpace d)) (q : Mat d) (hq : IsUnit q) (j : ℤ) (y : Vec d) (qi : ι → Mat d) (hqi : ∀ i ∈ s, IsUnit (qi i)) (ji : ι → ℤ) (yi : ι → Vec d) (B : BlockMat d) : have W := adaptedCellTranslate q j y; have U := fun (i : ι) => adaptedCellTranslate (qi i) (ji i) (yi i); (∀ i ∈ s, U i ⊆ W) → s.PairwiseDisjoint U → MeasureTheory.volume (W \ ⋃ i ∈ s, U i) = 0 → HasIntegrableCoarseBlock P W → (∀ i ∈ s, HasIntegrableCoarseBlock P (U i)) → (∀ (F : Finset ↑s), BlockMatLoewnerLE (ofFullBlockMat (∑ i ∈ F, ((MeasureTheory.volume (U ↑i)).toReal / (MeasureTheory.volume W).toReal) • toFullBlockMat (annealedBlock P (U ↑i)))) B) → BlockMatLoewnerLE (annealedBlock P W) B

A countable adapted partition inherits every finite upper bound on its annealed weighted sums. Positivity and bounded finite expected quadratics justify summation under expectation; qualitative ellipticity is only used pathwise.

theorem HCPolySupport.HighContrast.Annealed.bridge_maximal_row_mass {d : ℕ} (W : Set (Vec d)) (q : Mat d) (hq : IsUnit q) (cap t : ℤ) (hfin : (maximalAdaptedCellCenters W q cap t).Finite) (V : ℝ) : let I := { p : ℤ × (Fin d → ℤ) // IsMaximalAdaptedCellIn W q cap p.1 p.2 }; (Summable fun (i : { i : I // (↑i).1 = t }) => (MeasureTheory.volume (adaptedCellAtCenter q (↑↑i).1 (↑↑i).2)).toReal / V) ∧ ∑' (i : { i : I // (↑i).1 = t }), (MeasureTheory.volume (adaptedCellAtCenter q (↑↑i).1 (↑↑i).2)).toReal / V = ∑ _z ∈ hfin.toFinset, (MeasureTheory.volume (adaptedCell q t)).toReal / V

The finite center-row mass is the mass of the corresponding fiber of the pair index. This preserves the inclusive reverse cap row.

theorem HCPolySupport.HighContrast.Annealed.bridge_partition_comparison (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 mBase mParent : Mat d), Matrix.PosDef m → Matrix.PosDef mBase → Matrix.PosDef mParent → ∀ (cap b j terminal : ℤ), ↑jStar ≤ cap → ↑jStar ≤ b → ↑jStar ≤ terminal → adaptedCell (Geometry.explicitRoundedGrid jStar mParent) j ⊆ centeredCube d (2 * ↑jStar) → adaptedCell (Geometry.explicitRoundedGrid jStar m) terminal ⊆ centeredCube d (2 * ↑jStar) → ∀ (ι : Type) [Countable ι] (I : Set ι) (qi : ι → Mat d), (∀ i ∈ I, IsUnit (qi i)) → ∀ (ji : ι → ℤ) (yi : ι → Vec d) (old : ι → Prop) (r : ι → ℤ) (z : ι → Fin d → ℤ), have W := adaptedCell (Geometry.explicitRoundedGrid jStar mParent) j; have U := fun (i : ι) => adaptedCellTranslate (qi i) (ji i) (yi i); (∀ i ∈ I, U i ⊆ W) → I.PairwiseDisjoint U → MeasureTheory.volume (W \ ⋃ i ∈ I, U i) = 0 → (∀ i ∈ I, old i → U i = adaptedCellAtCenter (Geometry.explicitRoundedGrid jStar m) (r i) (z i)) → (∀ i ∈ I, ¬old i → U i = adaptedCellAtCenter (Geometry.explicitRoundedGrid jStar mBase) b (z i)) → (∀ i ∈ I, old i → r i ≤ cap) → ∀ (Cw : ℝ), 0 ≤ Cw → (∀ t ≤ cap, ∑' (i : Subtype ⋯), ⋯ / ⋯ ≤ Cw * 3 ^ (↑t - ↑j)) → BlockMatLoewnerLE (blockSub (adaptedMean P (Geometry.explicitRoundedGrid jStar mParent) j) (adaptedMean P (Geometry.explicitRoundedGrid jStar mBase) b)) (ofFullBlockMat (toFullBlockMat (blockScale Cw ⋯) + toFullBlockMat (blockScale ⋯ (adaptedMean P (Geometry.explicitRoundedGrid jStar m) terminal))))

The common partition comparison, before harmless enlargement of its fine coefficient. The old-grid normalization is obtained inside the proof; all constants precede the law. The two constructions discharge the geometric premises separately below.