High-contrast homogenization: Provider.Transport.CenteredSplit

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

The fresh/inherited decomposition of the centred filling

The combined bound for the transported fluctuations charges the centred response of one target cell of the new grid to two different objects: the sources strictly above the checkpoint are summed by discrete Young convolution against the centred moments v_r^q, giving the contribution of the fluctuations at the new scales, while the sources at or below it are not restarted — they are grouped by their scale-b ancestor and read off the single statistic X_B that stationarity compares with the centred history at the checkpoint (e.two.grid.old.history.factor).

The per-target-cell estimate Transport.cell_moment_le_of_gap produces one real number: the mixed L^Q(S_Q) size of the whole centred filling. This file splits that number along the two regimes, in the carriers the two downstream estimates consume.

The triangle inequality. The Schatten size is a norm, but the repository carries it only through its spectrum, so the triangle inequality is taken in the crude dimensional form the transport can afford: the Hilbert–Schmidt comparison |H|_{S_Q} ≤ (Σ_{αβ}H_{αβ}²)^{1/2} of l.fixed.geometry.matrix.averaging and the entrywise bound |H_{αβ}| ≤ |H|_{S_Q} give |A + B|_{S_Q} ≤ 2d(|A|_{S_Q} + |B|_{S_Q}), and Minkowski in L^Q carries it to the mixed norm. The dimensional factor is a C(d,Q), which is what the printed constants are.

The inherited leg. Below the checkpoint the estimate leaves the Schatten dialect at once: the return route PortableHistory.schattenSize_le_blockSize puts the sum back on the scalar size, which is subadditive because it is the spectral norm of the normalized block. Each cell is then renormalized from the checkpoint at the cost 3^{ρ_max(b-r)} and dominated by the statistic of its own scale-b ancestor; the passage back to the Q-th power is the printed max-to-sum, taken here through sup ≤ (Σ (·)^Q)^{1/Q}, so the ancestor count enters at the first power exactly as e.two.grid.old.history.factor binds it.

The normalization bridge. The fresh half is estimated at the old terminal normalization E_t^q and read at the new one E_n^{q'}; the same two spectral comparisons exchange the two, and the scale factor they cost is exactly the lower bridge clause (1-η_x)E_t^q ≤ E_n^{q'} of p.two.grid.transport.

The grouping map itself is not produced here: it is data of the filling, and the consumer supplies it together with the weight budget of the row sum inside an ancestor at the checkpoint generation.

The Schatten triangle inequality with the dimensional constant

theorem HCPolySupport.HighContrast.Transport.schattenNorm_add_le {d : ℕ} {Q : ℝ} (hQ : 2 ≤ Q) {A B C : BlockMat d} (hA : IsSymmetricBlockMat A) (hB : IsSymmetricBlockMat B) (hC : IsSymmetricBlockMat C) (hsum : toFullBlockMat C = toFullBlockMat A + toFullBlockMat B) : schattenNorm Q C ≤ 2 * ↑d * (schattenNorm Q A + schattenNorm Q B)

The Schatten size is subadditive up to 2d. The Hilbert–Schmidt comparison bounds the size of the sum by its Frobenius norm, and each of the 4d² entries of the sum is at most the sum of the two sizes.

theorem HCPolySupport.HighContrast.Transport.schattenSize_add_le {d : ℕ} {Q : ℝ} (hQ : 2 ≤ Q) {A B C F : BlockMat d} (hA : IsSymmetricBlockMat A) (hB : IsSymmetricBlockMat B) (hC : IsSymmetricBlockMat C) (hsum : toFullBlockMat C = toFullBlockMat A + toFullBlockMat B) : schattenSize Q C F ≤ 2 * ↑d * (schattenSize Q A F + schattenSize Q B F)

The same at a fixed normalization: normalization is real-linear, so the Schatten size inherits the dimensional triangle inequality.

The mixed norm of a sum

theorem HCPolySupport.HighContrast.Transport.aestronglyMeasurable_schattenSize {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {A : CoeffSpace d → BlockMat d} {F : BlockMat d} {Q : ℕ} (hQeven : Even Q) (hA : ∀ (a : CoeffSpace d), IsSymmetricBlockMat (A a)) (hAm : ∀ (α β : BlockCoord d), MeasureTheory.AEStronglyMeasurable (fun (a : CoeffSpace d) => toFullBlockMat (A a) α β) P) : MeasureTheory.AEStronglyMeasurable (fun (a : CoeffSpace d) => schattenSize (↑Q) (A a) F) P

The Schatten size of a random block at a fixed normalization is a measurable statistic at an even exponent.

theorem HCPolySupport.HighContrast.Transport.lqSchattenSize_rpow_eq {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {Q : ℝ} (hQ : 0 < Q) {A : CoeffSpace d → BlockMat d} (hA : ∀ (a : CoeffSpace d), IsSymmetricBlockMat (A a)) (F : BlockMat d) (hAm : MeasureTheory.AEStronglyMeasurable (fun (a : CoeffSpace d) => schattenSize Q (A a) F) P) : lqSchattenSize P Q A F ^ Q = ∫⁻ (a : CoeffSpace d), ENNReal.ofReal (schattenSize Q (A a) F) ^ Q ∂P

The Q-th power of the mixed norm is the Q-th moment of the Schatten size.

The scalar size of a filling sum

theorem HCPolySupport.HighContrast.Transport.blockSize_filling_sum_le {d : ℕ} {F : BlockMat d} (hF : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) {R : Finset ℤ} {Z : ℤ → Finset (Fin d → ℤ)} {c : ℤ → ℝ} (hc : ∀ r ∈ R, 0 ≤ c r) {H : ℤ → (Fin d → ℤ) → BlockMat d} (hH : ∀ (r : ℤ) (w : Fin d → ℤ), IsSymmetricBlockMat (H r w)) : blockSize (ofFullBlockMat (∑ r ∈ R, ∑ w ∈ Z r, c r • toFullBlockMat (H r w))) F ≤ ∑ r ∈ R, ∑ w ∈ Z r, c r * blockSize (H r w) F

The scalar size of a filling sum is subadditive. The normalized block is real-linear in its argument and the scalar size is the spectral norm of the normalized block.

The inherited leg

The decomposition

The inherited leg at the centred history

The normalization bridge

theorem HCPolySupport.HighContrast.Transport.lqSchattenSize_le_of_smul_le {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {Ej Ep : BlockMat d} (hEjs : IsSymmetricBlockMat Ej) (hEjpd : Book.Ch02.BlockPosDef Ej) (hEps : IsSymmetricBlockMat Ep) (hEppd : Book.Ch02.BlockPosDef Ep) {lam : ℝ} (hlam : 0 ≤ lam) (hle : toFullBlockMat Ej ≤ lam • toFullBlockMat Ep) {W : CoeffSpace d → BlockMat d} (hW : ∀ (a : CoeffSpace d), IsSymmetricBlockMat (W a)) {Q : ℝ} (hQ : 0 < Q) (hWm : MeasureTheory.AEStronglyMeasurable (fun (a : CoeffSpace d) => schattenSize Q (W a) Ep) P) : lqSchattenSize P Q W Ep ≤ ENNReal.ofReal ((2 * ↑d) ^ Q⁻¹ * lam) * lqSchattenSize P Q W Ej

The normalization exchange at a scale factor. If the old reference block is below λ times the new one, then the mixed L^Q(S_Q) size at the new normalization is at most (2d)^{1/Q}λ times the size at the old one.

The Schatten dialect is left and re-entered through the two spectral comparisons PortableHistory.schattenSize_le_blockSize and PortableHistory.blockSize_le_schattenSize; in between the exchange is PortableHistory.blockSize_le_mul_blockSize, which is where the scale factor enters and is the only inequality that is not dimension-free.

theorem HCPolySupport.HighContrast.Transport.lqSchattenSize_bridge_le {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {q q' : Mat d} {t n : ℤ} {etaX : ℝ} (heta1 : etaX < 1) (hEts : IsSymmetricBlockMat (adaptedMean P q t)) (hEtpd : Book.Ch02.BlockPosDef (adaptedMean P q t)) (hEns : IsSymmetricBlockMat (adaptedMean P q' n)) (hEnpd : Book.Ch02.BlockPosDef (adaptedMean P q' n)) (hlo : BlockMatLoewnerLE (blockScale (1 - etaX) (adaptedMean P q t)) (adaptedMean P q' n)) {W : CoeffSpace d → BlockMat d} (hW : ∀ (a : CoeffSpace d), IsSymmetricBlockMat (W a)) {Q : ℝ} (hQ : 0 < Q) (hWm : MeasureTheory.AEStronglyMeasurable (fun (a : CoeffSpace d) => schattenSize Q (W a) (adaptedMean P q' n)) P) : lqSchattenSize P Q W (adaptedMean P q' n) ≤ ENNReal.ofReal ((2 * ↑d) ^ Q⁻¹ * (1 - etaX)⁻¹) * lqSchattenSize P Q W (adaptedMean P q t)

The bridge normalization exchange. The lower bridge clause (1-η_x)E_t^q ≤ E_n^{q'} of p.two.grid.transport transports the fresh centred rows from the old terminal normalization to the new one at the cost (2d)^{1/Q}(1-η_x)^{-1}, which on the printed box 0 ≤ η_x ≤ 1/4 is at most (2d)^{1/Q}·4/3.