High-contrast homogenization: Entry.Annealed.BridgeSourceTail

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

The fine source tail for the two-grid bridge

Near e.two.grid.whitney.source, p.successful.short.bridge. The fine generations are indexed by their nonnegative deficit below jStar - 1; no generation is truncated away. The geometric ratio is 3 ^ (-(1-γ)), strictly below one for γ < 1.

The normalization has no reference-order premise.

theorem HCPolySupport.HighContrast.Annealed.bridge_fine_ratio_mem_Ico {γ : ℝ} (hγ : γ < 1) : 3 ^ (-(1 - γ)) ∈ Set.Ico 0 1

The exact fine geometric ratio is nonnegative and strictly less than one.

theorem HCPolySupport.HighContrast.Annealed.bridge_fine_weighted_sum {ι : Type u_1} (w : ι → ℝ) (r : ι → ℤ) (hw0 : ∀ (i : ι), 0 ≤ w i) (hw : Summable w) (J j : ℤ) (hr : ∀ (i : ι), r i < J) (C : ℝ) (hC : 0 ≤ C) (hrow : ∀ (t : ℤ), ∑' (i : { i : ι // r i = t }), w ↑i ≤ C * 3 ^ (↑t - ↑j)) (γ : ℝ) (hγ : γ < 1) : (Summable fun (i : ι) => w i * 3 ^ (γ * (↑J - ↑(r i)))) ∧ ∑' (i : ι), w i * 3 ^ (γ * (↑J - ↑(r i))) ≤ C / (1 - 3 ^ (-(1 - γ))) * 3 ^ (-(↑j - ↑J))

Any countable fine family with the Whitney row estimate has the summable source penalty. The summable unweighted masses come from disjointness in the finite-volume parent; the row estimate is supplied by the two-grid bridge.

theorem HCPolySupport.HighContrast.Annealed.bridge_block_tsum_bound {d : ℕ} {ι : Type u_1} (A : ι → BlockMat d) (E : BlockMat d) (w c : ι → ℝ) (hw0 : ∀ (i : ι), 0 ≤ w i) (hAs : ∀ (i : ι), IsSymmetricBlockMat (A i)) (hAp : ∀ (i : ι), Book.Ch02.BlockPosDef (A i)) (ho : ∀ (i : ι), BlockMatLoewnerLE (A i) (blockScale (c i) E)) (hc : Summable fun (i : ι) => w i * c i) : (Summable fun (i : ι) => w i • toFullBlockMat (A i)) ∧ BlockMatLoewnerLE (ofFullBlockMat (∑' (i : ι), w i • toFullBlockMat (A i))) (blockScale (∑' (i : ι), w i * c i) E)

A countable positive block family admits an actual weighted sum, with the same scalar order envelope. This uses full block coordinates throughout.

theorem HCPolySupport.HighContrast.Annealed.bridge_fine_source_tail (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 → ∃ (X : CoeffSpace d → ℝ), (∀ (a : CoeffSpace d), 0 ≤ X a) ∧ MeasureTheory.MemLp X (ENNReal.ofReal ↑(bigQ d γ)) P ∧ MeasureTheory.Integrable X P ∧ ∫ (a : CoeffSpace d), X a ∂P ≤ 2 ∧ ∀ (m : Mat d), Matrix.PosDef m → ∀ W ⊆ centeredCube d (2 * ↑jStar), ∀ (ι : Type) [Countable ι] (r : ι → ℤ) (y : ι → Vec d) (w : ι → ℝ), (∀ (i : ι), r i < ↑jStar) → (∀ (i : ι), 0 ≤ w i) → Summable w → (∀ (i : ι), adaptedCellTranslate (Geometry.explicitRoundedGrid jStar m) (r i) (y i) ⊆ W) → ∀ (j : ℤ) (Cw : ℝ), 0 ≤ Cw → (∀ (t : ℤ), ∑' (i : { i : ι // r i = t }), w ↑i ≤ Cw * 3 ^ (↑t - ↑j)) → have M := fun (a : CoeffSpace d) => ofFullBlockMat (∑' (i : ι), w i • toFullBlockMat (coarseBlock (adaptedCellTranslate (Geometry.explicitRoundedGrid jStar m) (r i) (y i)) a)); SchattenMemLp P (↑(bigQ d γ)) M ∧ (∀ᵐ (a : CoeffSpace d) ∂P, (Summable fun (i : ι) => w i • toFullBlockMat (coarseBlock (adaptedCellTranslate (Geometry.explicitRoundedGrid jStar m) (r i) (y i)) a)) ∧ BlockMatLoewnerLE (M a) (blockScale (C * √(‖m‖ * ‖m⁻¹‖) * X a * Cw * 3 ^ (-(↑j - ↑jStar))) E)) ∧ BlockMatLoewnerLE (ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (M a) α β ∂P)) (blockScale (2 * C * √(‖m‖ * ‖m⁻¹‖) * Cw * 3 ^ (-(↑j - ↑jStar))) E)

The actual fine source tail: one source envelope works simultaneously for all contained families. The geometric hypotheses are just nonnegative summable volume weights, the fine row bound, and containment through the parent window.

theorem HCPolySupport.HighContrast.Annealed.bridge_blockScale_mono {d : ℕ} {A B : BlockMat d} {c : ℝ} (hc : 0 ≤ c) (h : BlockMatLoewnerLE A B) : BlockMatLoewnerLE (blockScale c A) (blockScale c B)

Nonnegative scaling preserves the full quadratic block order.

theorem HCPolySupport.HighContrast.Annealed.bridge_normalize_source_tail (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) → ∀ (B : BlockMat d) (D : ℝ), 0 ≤ D → BlockMatLoewnerLE B (blockScale D E) → BlockMatLoewnerLE B (blockScale (D * C * aspectRatio E * √(‖m‖ * ‖m⁻¹‖)) (adaptedMean P (Geometry.explicitRoundedGrid jStar m) s))

Any source tail bounded by D E is converted into a comparison with the actual old-grid terminal mean. The source constant is selected before the law; the reference order is derived from the dagger law, never supplied as a premise here.

theorem HCPolySupport.HighContrast.Annealed.bridge_source_normalization_factor {Pi a b t γ : ℝ} (hPi : 0 ≤ Pi) (ha : 0 ≤ a) (hb : 0 ≤ b) (ht : 0 ≤ t) (hγ : 0 ≤ γ) : Pi * a ^ 2 * 3 ^ (-t) ≤ (1 + Pi * (a + b) ^ 2) * 3 ^ (-(1 - γ) * t)

The two old-grid eccentricity factors can be enlarged to the printed squared sum; the faster source decay can be weakened to the printed exponent. One factor comes from the source estimate and one from old-grid normalization in the proof of p.successful.short.bridge, near e.two.grid.source.normalization. The proof does not require normalization on the other grid.