High-contrast homogenization: Entry.Annealed.TransportReduction

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

Two-grid transport reduction

This module proves the block arithmetic underlying the two-grid transport estimate p.two.grid.transport. It establishes the scale-monotonicity of the doubled identity and the trace excess of subtracting that identity, the comparison of normalized blocks at Schatten order one, and the uniform bound on the normalization loss over the window δ ∈ [0, 1/4]. It then records the deterministic weighted gap inequality and the finite and centred mean-split identities that decompose a normalized Whitney sum into its row means plus one integrable tail, the splitting of the actual sum into a bulk row, boundary rows and the fine subseries, the convexity, scaling and addition estimates for the source and mean-penalty powers, and the pointwise comparison of a normalized row taken before any maximum over rows or target cells.

theorem HCPolySupport.HighContrast.Annealed.transport_identity_scale_mono {d : ℕ} {x y : ℝ} (hxy : x ≤ y) : BlockMatLoewnerLE (blockScale x (Book.Ch02.blockIdentity d)) (blockScale y (Book.Ch02.blockIdentity d))

Scalar order on the doubled identity, including zero coefficients.

theorem HCPolySupport.HighContrast.Annealed.transport_trace_excess {d : ℕ} (A : BlockMat d) : blockTrace (blockSub A (Book.Ch02.blockIdentity d)) = blockTrace A - 2 * ↑d

theorem HCPolySupport.HighContrast.Annealed.transport_trace_normalizer_comparison {d : ℕ} {F H X : BlockMat d} (hF : Matrix.PosDef (toFullBlockMat F)) (hH : Matrix.PosDef (toFullBlockMat H)) (hX : Matrix.PosSemidef (toFullBlockMat X)) {δ : ℝ} (hδ : δ ∈ Set.Icc 0 (1 / 4)) (hlow : BlockMatLoewnerLE (blockScale (1 - δ) F) H) (hup : BlockMatLoewnerLE H (blockScale (1 + δ) F)) : blockTrace (blockSub (normalizedBlock X H) (Book.Ch02.blockIdentity d)) ≤ (1 - δ)⁻¹ * blockTrace (blockSub (normalizedBlock X F) (Book.Ch02.blockIdentity d)) + 2 * ↑d * δ / (1 - δ)

The additive Cδ error comes from subtracting the doubled identity after the norm change.

theorem HCPolySupport.HighContrast.Annealed.transport_delta_bounds (d : ℕ) {δ : ℝ} (hδ : δ ∈ Set.Icc 0 (1 / 4)) : (1 - δ)⁻¹ ≤ 4 / 3 ∧ 2 * ↑d * δ / (1 - δ) ≤ 8 / 3 * ↑d * δ

The fixed δ-window makes both normalization losses uniformly bounded.

theorem HCPolySupport.HighContrast.Annealed.transport_weighted_gap_mean {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (Q : ℕ) (hQ : 2 ≤ Q) {ι : Type u_1} (I : Finset ι) (hI : I.Nonempty) (w : ι → ℝ) (hw : ∀ (i : ι), 0 ≤ w i) (F G : ι → CoeffSpace d → BlockMat d) (hF : ∀ i ∈ I, SchattenMemLp P (↑Q) (F i)) (hG : ∀ i ∈ I, SchattenMemLp P (↑Q) (G i)) (hFpos : ∀ i ∈ I, ∀ᵐ (a : CoeffSpace d) ∂P, BlockMatLoewnerLE (ofFullBlockMat 0) (F i a)) (hFG : ∀ i ∈ I, ∀ᵐ (a : CoeffSpace d) ∂P, BlockMatLoewnerLE (F i a) (G i a)) (hmean : ∀ i ∈ I, BlockMatLoewnerLE (Book.Ch02.blockIdentity d) (ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (F i a) α β ∂P))) : have MF := fun (i : ι) => ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (F i a) α β ∂P); have MG := fun (i : ι) => ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (G i a) α β ∂P); ∫ (a : CoeffSpace d), (⨆ i ∈ ↑I, w i * blockOpNorm (blockSub (F i a) (MF i))) ^ ↑Q ∂P ≤ 2 ^ (↑Q - 1) * (1 + (2 * ↑d) ^ (↑Q)⁻¹) ^ ↑Q * ∫ (a : CoeffSpace d), (⨆ i ∈ ↑I, w i * absSchattenNorm (↑Q) (blockSub (G i a) (MG i))) ^ ↑Q ∂P + 2 ^ (2 * ↑Q - 1) * (1 + ↑d ^ (1 - (↑Q)⁻¹)) ^ ↑Q * ∑ i ∈ I, w i ^ ↑Q * meanPenalty Q (MG i)

The deterministic term in the joint gap is a sum of mean penalties. The centered term remains under the joint maximum.

theorem HCPolySupport.HighContrast.Annealed.transport_mean_finite_split {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsFiniteMeasure P] {N : ℝ} (hN : 1 ≤ N) {ι : Type u_1} (s : Finset ι) (F : ι → CoeffSpace d → BlockMat d) (G T : CoeffSpace d → BlockMat d) (hF : ∀ i ∈ s, SchattenMemLp P N (F i)) (hT : SchattenMemLp P N T) (hsplit : ∀ᵐ (a : CoeffSpace d) ∂P, toFullBlockMat (G a) = ∑ i ∈ s, toFullBlockMat (F i a) + toFullBlockMat (T a)) : have MF := fun (i : ι) => ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (F i a) α β ∂P); have MG := ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (G a) α β ∂P); have MT := ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (T a) α β ∂P); toFullBlockMat MG = ∑ i ∈ s, toFullBlockMat (MF i) + toFullBlockMat MT

Expectation respects an a.e. finite decomposition with one integrable tail.

theorem HCPolySupport.HighContrast.Annealed.transport_centered_finite_split {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {N : ℝ} (hN : 1 ≤ N) {ι : Type u_1} (s : Finset ι) (F : ι → CoeffSpace d → BlockMat d) (G T : CoeffSpace d → BlockMat d) (hF : ∀ i ∈ s, SchattenMemLp P N (F i)) (hG : SchattenMemLp P N G) (hT : SchattenMemLp P N T) (hsplit : ∀ᵐ (a : CoeffSpace d) ∂P, toFullBlockMat (G a) = ∑ i ∈ s, toFullBlockMat (F i a) + toFullBlockMat (T a)) : have MF := fun (i : ι) => ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (F i a) α β ∂P); have MG := ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (G a) α β ∂P); have MT := ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (T a) α β ∂P); ∀ᵐ (a : CoeffSpace d) ∂P, absSchattenNorm N (blockSub (G a) MG) ≤ (2 * ↑d) ^ N⁻¹ * (∑ i ∈ s, absSchattenNorm N (blockSub (F i a) (MF i)) + absSchattenNorm N (blockSub (T a) MT))

Centering commutes with a finite row decomposition plus one integrable tail. The triangle estimate has no factor for the number of rows.

theorem HCPolySupport.HighContrast.Annealed.transport_centered_tail_envelope {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {N : ℝ} (hN : 1 ≤ N) (T : CoeffSpace d → BlockMat d) (hT : SchattenMemLp P N T) (X : CoeffSpace d → ℝ) (hX : MeasureTheory.Integrable X P) (hEX : ∫ (a : CoeffSpace d), X a ∂P ≤ 2) (c : ℝ) (hc : 0 ≤ c) (hpos : ∀ᵐ (a : CoeffSpace d) ∂P, BlockMatLoewnerLE (ofFullBlockMat 0) (T a)) (hbound : ∀ᵐ (a : CoeffSpace d) ∂P, BlockMatLoewnerLE (T a) (blockScale (c * X a) (Book.Ch02.blockIdentity d))) : have MT := ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (T a) α β ∂P); blockTrace MT ≤ 2 * ↑d * c * 2 ∧ ∀ᵐ (a : CoeffSpace d) ∂P, absSchattenNorm N (blockSub (T a) MT) ≤ 2 * ↑d * c * (X a + 2)

A positive tail bounded by one scalar envelope stays bounded after centering. The same X is available to the later joint maximum.

theorem HCPolySupport.HighContrast.Annealed.transport_centered_lattice_row (d : ℕ) (hd : 2 ≤ d) (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (γ : ℝ) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ) (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P γ E Ψ K S) (jStar : ℕ) (hjStar : 2 * d ≤ 3 ^ jStar) (m : Mat d) (hm : Matrix.PosDef m) (j : ℤ) (hj : ↑jStar ≤ j) (Z : Finset (Vec d)) (hZ : ∀ z ∈ Z, z ∈ adaptedLatticeAtScale (Geometry.explicitRoundedGrid jStar m) j) (w : Vec d → ℝ) (R : BlockMat d) : have q := Geometry.explicitRoundedGrid jStar m; have A := fun (a : CoeffSpace d) => normalizedBlock (ofFullBlockMat (∑ z ∈ Z, w z • toFullBlockMat (coarseBlock (adaptedCellTranslate q j z) a))) R; have MA := ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (A a) α β ∂P); MA = blockScale (∑ z ∈ Z, w z) (normalizedBlock (adaptedMean P q j) R) ∧ ∀ (a : CoeffSpace d), blockSub (A a) MA = ofFullBlockMat (∑ z ∈ Z, w z • toFullBlockMat (normalizedBlock (blockSub (coarseBlock (adaptedCellTranslate q j z) a) (adaptedMean P q j)) R))

Stationarity identifies each centered cell in an actual finite Whitney row. The identity is pointwise and therefore remains valid under the joint maximum.

theorem HCPolySupport.HighContrast.Annealed.transport_mean_trace_split {d : ℕ} {ι : Type u_1} (s : Finset ι) (lam : ι → ℝ) (A : ι → BlockMat d) (F H G T : BlockMat d) (hF : Matrix.PosDef (toFullBlockMat F)) (hH : Matrix.PosDef (toFullBlockMat H)) {δ : ℝ} (hδ : δ ∈ Set.Icc 0 (1 / 4)) (hlow : BlockMatLoewnerLE (blockScale (1 - δ) F) H) (hup : BlockMatLoewnerLE H (blockScale (1 + δ) F)) (hlam : ∀ i ∈ s, 0 ≤ lam i) (hmass : ∑ i ∈ s, lam i ≤ 1) (hA : ∀ i ∈ s, Matrix.PosSemidef (toFullBlockMat (A i))) (ht : ∀ i ∈ s, 0 ≤ blockTrace (blockSub (normalizedBlock (A i) F) (Book.Ch02.blockIdentity d))) (hsplit : toFullBlockMat G = ∑ i ∈ s, lam i • toFullBlockMat (normalizedBlock (A i) H) + toFullBlockMat T) (u : ℝ) (hT : blockTrace T ≤ u) : blockTrace (blockSub G (Book.Ch02.blockIdentity d)) ≤ 4 / 3 * ∑ i ∈ s, lam i * blockTrace (blockSub (normalizedBlock (A i) F) (Book.Ch02.blockIdentity d)) + 8 / 3 * ↑d * δ + u

At the trace level, missing volume is filled by the identity. The finite part has mass at most one, so the normalization error is Cδ, independent of how many rows or cells occur.

theorem HCPolySupport.HighContrast.Annealed.transport_whitney_raw_split {d : ℕ} (q : Mat d) (hq : IsUnit q) (W : Set (Vec d)) (J cap : ℤ) (hJ : J ≤ cap) (hfin : ∀ t ≤ cap, (maximalAdaptedCellCenters W q cap t).Finite) (a : CoeffSpace d) (R : BlockMat d) : let I := { p : ℤ × (Fin d → ℤ) // IsMaximalAdaptedCellIn W q cap p.1 p.2 }; have f := fun (p : I) => ((MeasureTheory.volume (adaptedCellAtCenter q (↑p).1 (↑p).2)).toReal / (MeasureTheory.volume W).toReal) • toFullBlockMat (coarseBlock (adaptedCellAtCenter q (↑p).1 (↑p).2) a); have Z := fun (t : ℤ) => if ht : t ≤ cap then ⋯.toFinset else ∅; have row := fun (t : ℤ) => ofFullBlockMat (∑ z ∈ Z t, ((MeasureTheory.volume (adaptedCell q t)).toReal / (MeasureTheory.volume W).toReal) • toFullBlockMat (coarseBlock (adaptedCellTranslate q t z) a)); have fine := ofFullBlockMat (∑' (p : { p : I // (↑p).1 < J }), f ↑p); Summable f → toFullBlockMat (normalizedBlock (ofFullBlockMat (∑' (p : I), f p)) R) = toFullBlockMat (normalizedBlock (row cap) R) + ∑ t ∈ Finset.Icc J (cap - 1), toFullBlockMat (normalizedBlock (row t) R) + toFullBlockMat (normalizedBlock fine R)

The actual normalized Whitney sum has precisely a finite bulk row, finite boundary rows, and the fine subseries. Convergence is supplied by the source bounds; no coarse block is evaluated on the remainder of the partition.

theorem HCPolySupport.HighContrast.Annealed.transport_row_normalizer_comparison {d : ℕ} {ι : Type u_1} (s : Finset ι) (w : ι → ℝ) (X : ι → BlockMat d) (hX : ∀ i ∈ s, Matrix.IsHermitian (toFullBlockMat (X i))) {F H : BlockMat d} (hF : Matrix.PosDef (toFullBlockMat F)) (hH : Matrix.PosDef (toFullBlockMat H)) {N : ℝ} (hN : 1 ≤ N) {δ : ℝ} (hδ : δ ∈ Set.Icc 0 (1 / 4)) (hlow : BlockMatLoewnerLE (blockScale (1 - δ) F) H) (hup : BlockMatLoewnerLE H (blockScale (1 + δ) F)) : absSchattenNorm N (ofFullBlockMat (∑ i ∈ s, w i • toFullBlockMat (normalizedBlock (X i) H))) ≤ 4 / 3 * absSchattenNorm N (ofFullBlockMat (∑ i ∈ s, w i • toFullBlockMat (normalizedBlock (X i) F)))

The normalizer change is pointwise on the whole centered row, before any maximum over rows or target cells is taken.

theorem HCPolySupport.HighContrast.Annealed.transport_centered_whitney_bound (d : ℕ) (hd : 2 ≤ d) (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (γ : ℝ) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ) (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P γ E Ψ K S) (jStar : ℕ) (hjStar : 2 * d ≤ 3 ^ jStar) (m mPlus : Mat d) (hm : Matrix.PosDef m) (hmPlus : Matrix.PosDef mPlus) (oldEnd newEnd cap : ℤ) (hcap : ↑jStar ≤ cap) (W : Set (Vec d)) (hfin : ∀ t ≤ cap, (maximalAdaptedCellCenters W (Geometry.explicitRoundedGrid jStar m) cap t).Finite) (N : ℝ) (hN : 1 ≤ N) (X : CoeffSpace d → ℝ) (hX : MeasureTheory.Integrable X P) (hEX : ∫ (a : CoeffSpace d), X a ∂P ≤ 2) (c : ℝ) (hc : 0 ≤ c) (δ : ℝ) (hδ : δ ∈ Set.Icc 0 (1 / 4)) : have q := Geometry.explicitRoundedGrid jStar m; have F := adaptedMean P q oldEnd; have H := adaptedMean P (Geometry.explicitRoundedGrid jStar mPlus) newEnd; let I := { p : ℤ × (Fin d → ℤ) // IsMaximalAdaptedCellIn W q cap p.1 p.2 }; have f := fun (p : I) (a : CoeffSpace d) => ((MeasureTheory.volume (adaptedCellAtCenter q (↑p).1 (↑p).2)).toReal / (MeasureTheory.volume W).toReal) • toFullBlockMat (coarseBlock (adaptedCellAtCenter q (↑p).1 (↑p).2) a); have Z := fun (t : ℤ) => if ht : t ≤ cap then ⋯.toFinset else ∅; have G := fun (a : CoeffSpace d) => normalizedBlock (ofFullBlockMat (∑' (p : I), f p a)) H; have T := fun (a : CoeffSpace d) => normalizedBlock (ofFullBlockMat (∑' (p : { p : I // (↑p).1 < ↑jStar }), f (↑p) a)) H; have V := fun (t : ℤ) (a : CoeffSpace d) => ofFullBlockMat (∑ z ∈ Z t, ((MeasureTheory.volume (adaptedCell q t)).toReal / (MeasureTheory.volume W).toReal) • toFullBlockMat (normalizedBlock (blockSub (coarseBlock (adaptedCellTranslate q t z) a) (adaptedMean P q t)) F)); BlockMatLoewnerLE (blockScale (1 - δ) F) H → BlockMatLoewnerLE H (blockScale (1 + δ) F) → SchattenMemLp P N G → SchattenMemLp P N T → (∀ᵐ (a : CoeffSpace d) ∂P, Summable fun (p : I) => f p a) → (∀ᵐ (a : CoeffSpace d) ∂P, BlockMatLoewnerLE (ofFullBlockMat 0) (T a)) → (∀ᵐ (a : CoeffSpace d) ∂P, BlockMatLoewnerLE (T a) (blockScale (c * X a) (Book.Ch02.blockIdentity d))) → have MG := ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (G a) α β ∂P); ∀ᵐ (a : CoeffSpace d) ∂P, absSchattenNorm N (blockSub (G a) MG) ≤ 4 / 3 * (2 * ↑d) ^ N⁻¹ * (absSchattenNorm N (V cap a) + ∑ t ∈ Finset.Icc (↑jStar) (cap - 1), absSchattenNorm N (V t a)) + (2 * ↑d) ^ N⁻¹ * (2 * ↑d) * c * (X a + 2)

p.two.grid.transport, with the actual Whitney rows. The hypotheses on the fine part are the normalized conclusions of transport_fine_source_tail; the membership of the whole sum is furnished by exists_transport_whitney_ordered_data. One scalar X controls the tail for every subsequent target.

theorem HCPolySupport.HighContrast.Annealed.meanPenalty_convex_combination (Q : ℕ) {ι : Type u_1} (s : Finset ι) (lam t : ι → ℝ) (hlam : ∀ i ∈ s, 0 ≤ lam i) (ht : ∀ i ∈ s, 0 ≤ t i) (hsum : ∑ i ∈ s, lam i ≤ 1) : (1 + ∑ i ∈ s, lam i * t i) ^ Q - 1 ≤ ∑ i ∈ s, lam i * ((1 + t i) ^ Q - 1)

Insert the missing mass at trace excess zero before applying convexity.

theorem HCPolySupport.HighContrast.Annealed.transport_penalty_scale (Q : ℕ) {x c : ℝ} (hx : 0 ≤ x) (hc : 1 ≤ c) : (1 + c * x) ^ Q - 1 ≤ c ^ Q * ((1 + x) ^ Q - 1)

Scaling a nonnegative trace excess costs at most the Q-th power.

theorem HCPolySupport.HighContrast.Annealed.transport_penalty_linear_and_power (Q : ℕ) {x : ℝ} (hx : 0 ≤ x) : (1 + x) ^ Q - 1 ≤ 2 ^ Q * (x + x ^ Q)

The nonlinear source error retains its first and Q-th powers.

theorem HCPolySupport.HighContrast.Annealed.transport_penalty_add (Q : ℕ) {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) : (1 + (x + y)) ^ Q - 1 ≤ 2 ^ Q * ((1 + x) ^ Q - 1 + ((1 + y) ^ Q - 1))

Splitting a trace excess costs only a constant depending on Q.

theorem HCPolySupport.HighContrast.Annealed.transport_penalty_convex_error (Q : ℕ) (hQ : 1 ≤ Q) (D : ℝ) (hD : 0 ≤ D) : ∃ (C : ℝ), 0 < C ∧ ∀ (ι : Type u_1) (s : Finset ι) (lam x : ι → ℝ), (∀ i ∈ s, 0 ≤ lam i) → (∀ i ∈ s, 0 ≤ x i) → ∑ i ∈ s, lam i ≤ 1 → ∀ (δ u t : ℝ), δ ∈ Set.Icc 0 1 → 0 ≤ u → 0 ≤ t → t ≤ 4 / 3 * ∑ i ∈ s, lam i * x i + (D * δ + u) → (1 + t) ^ Q - 1 ≤ C * (∑ i ∈ s, lam i * ((1 + x i) ^ Q - 1) + δ + u + u ^ Q)

Insert the missing mass at zero trace excess, then separate the normalizer error and both powers of the source error. The constant precedes every weight.

theorem HCPolySupport.HighContrast.Annealed.transport_whitney_mean_identity (d : ℕ) (hd : 2 ≤ d) (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (γ : ℝ) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ) (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P γ E Ψ K S) (jStar : ℕ) (hjStar : 2 * d ≤ 3 ^ jStar) (m : Mat d) (hm : Matrix.PosDef m) (W : Set (Vec d)) (cap : ℤ) (hcap : ↑jStar ≤ cap) (hfin : ∀ t ≤ cap, (maximalAdaptedCellCenters W (Geometry.explicitRoundedGrid jStar m) cap t).Finite) (N : ℝ) (hN : 1 ≤ N) (R : BlockMat d) : have q := Geometry.explicitRoundedGrid jStar m; let I := { p : ℤ × (Fin d → ℤ) // IsMaximalAdaptedCellIn W q cap p.1 p.2 }; have f := fun (p : I) (a : CoeffSpace d) => ((MeasureTheory.volume (adaptedCellAtCenter q (↑p).1 (↑p).2)).toReal / (MeasureTheory.volume W).toReal) • toFullBlockMat (coarseBlock (adaptedCellAtCenter q (↑p).1 (↑p).2) a); have Z := fun (t : ℤ) => if ht : t ≤ cap then ⋯.toFinset else ∅; have lam := fun (t : ℤ) => ∑ _z ∈ Z t, (MeasureTheory.volume (adaptedCell q t)).toReal / (MeasureTheory.volume W).toReal; have G := fun (a : CoeffSpace d) => normalizedBlock (ofFullBlockMat (∑' (p : I), f p a)) R; have T := fun (a : CoeffSpace d) => normalizedBlock (ofFullBlockMat (∑' (p : { p : I // (↑p).1 < ↑jStar }), f (↑p) a)) R; SchattenMemLp P N T → (∀ᵐ (a : CoeffSpace d) ∂P, Summable fun (p : I) => f p a) → toFullBlockMat (ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (G a) α β ∂P)) = ∑ t ∈ Finset.Icc (↑jStar) cap, lam t • toFullBlockMat (normalizedBlock (adaptedMean P q t) R) + toFullBlockMat (ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (T a) α β ∂P))

The expectation of the actual Whitney sum is the finite weighted sum of stationary row means plus the expectation of the fine subseries.