High-contrast homogenization: Provider.Transport.AnnealedRows

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

The pathwise majorant of a target cell

e.two.grid.whitney.average is consumed against a majorant, not summed: its hypothesis is that a block dominates every finite partial double sum of the filling's rows. The printed majorant Σ_{r=j_*}^{n}Σ_{V∈𝒱_r}(|V|/|W|)𝐀(V) + G_W^{<j_*} is exhibited here with the below-start term in closed form, and the hypothesis is discharged.

The rows below the alignment are paid by one geometric series: the cross-grid row of e.two.grid.whitney.volumes weights a scale-r row by 3^{r-j}, the window multiplier's own cell bound carries the burn discount 3^{g(j_*-r)}, and the product is 3^{j_*-j}3^{-(1-g)(j_*-r)}, whose total over the scales below the alignment is 3^{j_*-j}ζ_g -- the same geometric series that the boundary constant B_{\mathbf q} already names. Nothing of the filling is discarded: the rows at or above the alignment are kept whole, as the printed right side keeps them.

Elementary transport of symmetry, positivity and quadratic forms

The two scalar steps of the below-start series

theorem HCPolySupport.HighContrast.Transport.zpow_mul_burnDiscount_eq {g : ℝ} {jStar r j : ℤ} (hr : r ≤ jStar) : 3 ^ (r - j) * burnDiscount g jStar r = 3 ^ (jStar - j) * 3 ^ (-(1 - g) * (↑jStar - ↑r))

The below-start weight in closed form. Below the alignment scale the cross-grid row weight 3^{r-j} and the burn discount 3^{g(j_*-r)} combine into 3^{j_*-j}3^{-(1-g)(j_*-r)}: the burn is paid by the part of the row decay that the exponent 1-g leaves over.

theorem HCPolySupport.HighContrast.Transport.sum_belowStart_weight_le {g : ℝ} (hg : g < 1) (jStar j J : ℤ) : ∑ r ∈ Finset.Ico J jStar, 3 ^ (r - j) * burnDiscount g jStar r ≤ 3 ^ (jStar - j) * zetaG g

The total below-start weight. The scales strictly below the alignment carry total weight at most 3^{j_*-j}ζ_g, the geometric series of ratio 3^{-(1-g)}.

The pathwise majorant

theorem HCPolySupport.HighContrast.Transport.coarseBlock_le_filling_rows_add_belowStart {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K Cd : ℝ} {jStar M : ℤ} {Y : CoeffSpace d → ℝ} [NeZero d] (hd : 1 ≤ d) (hCd : 0 ≤ Cd) (hg : g < 1) (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) (hY : IsWindowMultiplier P g E Ψ K Cd jStar M Y) {nu : Mat d} (hnu : Matrix.PosDef nu) (hq : IsRoundedGrid jStar (roundedGrid jStar nu)) {p : Mat d} (hp : Matrix.PosDef p) {Khop : ℝ} (hK : gridRatio (roundedGrid jStar nu) p ≤ Khop) {n j : ℤ} (hjn : jStar ≤ n) {y : Vec d} {Z : ℤ → Finset (Fin d → ℤ)} (hZ : ∀ (r : ℤ), ↑(Z r) = fillingIndex (roundedGrid jStar nu) n (adaptedCellTranslate p j y) r) (hcont : ∀ r < jStar, ∀ w ∈ Z r, adaptedCellAt (roundedGrid jStar nu) r w ⊆ centeredCube d M) : ∀ᵐ (a : CoeffSpace d) ∂P, toFullBlockMat (coarseBlock (adaptedCellTranslate p j y) a) ≤ ∑ r ∈ Finset.Icc jStar n, ∑ w ∈ Z r, ((MeasureTheory.volume (adaptedCellAt (roundedGrid jStar nu) r w)).toReal / (MeasureTheory.volume (adaptedCellTranslate p j y)).toReal) • toFullBlockMat (coarseBlock (adaptedCellAt (roundedGrid jStar nu) r w) a) + (6 * ↑d * √↑d * Khop * boundaryConst Cd g nu * zetaG g * 3 ^ (jStar - j) * Y a) • toFullBlockMat E

The pathwise majorant of e.two.grid.whitney.average, exhibited. The coarse response of a target cell of the new grid is below the weighted rows of the old grid's filling from the alignment scale up to the starting scale, plus the closed-form below-start term C_dK_{hop}B_{\mathbf q}ζ_g3^{j_*-j}Y_P𝐄.

Every partial double sum of the filling is split at the alignment: the rows at or above it form a subsum of the printed finite part, and the rows below it are paid by the geometric series of the previous display, each cell being controlled by the window multiplier's own cell bound.