High-contrast homogenization: Entry.Annealed.TransportFluctuations

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

Fluctuation bounds for the two-grid transport

The fluctuation and Whitney estimates consumed by the two-grid transport p.two.grid.transport. Stationarity pays only the number of scale-k parents for their joint history maximum; the averaged lattice row and the two Whitney row shapes are bounded as Schatten moments, with the operator-norm, weighted-moment and finite-row inequalities that let a single nonnegative envelope dominate every old-history generation. The old bulk family, the boundary rows above k and the root of the weighted moment are then paid by the profile, after canceling the exact parent-cardinality and dimension factors, so the whole old-history contribution keeps the printed terminal decay.

theorem HCPolySupport.HighContrast.Annealed.transport_parent_history_max (d : ℕ) (hd : 2 ≤ d) (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (γ : ℝ) (_hγ : γ ∈ Set.Ico 0 1) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ) (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P γ E Ψ K S) (jStar : ℕ) (hj : 2 * d ≤ 3 ^ jStar) (m : Mat d) (hm : Matrix.PosDef m) (k : ℤ) (hk : ↑jStar ≤ k) {ι : Type u_1} (Z : Finset ι) (hZ : Z.Nonempty) (p : ι → Fin d → ℤ) : have q := Geometry.explicitRoundedGrid jStar m; have H := fun (a : CoeffSpace d) => ⨆ j ∈ Set.Icc (↑jStar) k, 3 ^ (-↑(bigQ d γ) * rhoMax d γ * (↑k - ↑j)) * ⨆ y ∈ adaptedLatticeAtScale q j ∩ adaptedCell q k, blockOpNorm (normalizedFluctuation P q j k y a) ^ bigQ d γ; (∀ (a : CoeffSpace d), 0 ≤ H a) ∧ MeasureTheory.Integrable (fun (a : CoeffSpace d) => ⨆ z ∈ ↑Z, H (translateCoeff (p z) a)) P ∧ ∫ (a : CoeffSpace d), ⨆ z ∈ ↑Z, H (translateCoeff (p z) a) ∂P ≤ ↑Z.card * fluctuationHistory P γ q jStar k

Stationarity pays only the number of scale-k parents for their joint history maximum. Every parent keeps the same translation across all child generations.

theorem HCPolySupport.HighContrast.Annealed.exists_transport_averaged_fluctuation (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (Csrc : ℝ), 0 < Csrc ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P γ E Ψ K S → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar → ∀ (m : Mat d), Matrix.PosDef m → ∀ (r t : ℤ), ↑jStar ≤ r → r ≤ t → ∀ (Z : Finset (Vec d)), ↑Z ⊆ adaptedLatticeAtScale (Geometry.explicitRoundedGrid jStar m) r → ∀ (v : ℝ), 0 ≤ v → (lqSchattenNorm P ↑(bigQ d γ) fun (a : CoeffSpace d) => ofFullBlockMat (∑ z ∈ Z, v • toFullBlockMat (normalizedFluctuation P (Geometry.explicitRoundedGrid jStar m) r t z a))) ≤ ↑(bigQ d γ) * 3 ^ (↑d / 2) * (√↑Z.card * v) * Real.exp (detIncrement P (Geometry.explicitRoundedGrid jStar m) r t) * lqSchattenNorm P (↑(bigQ d γ)) (normalizedFluctuationSelf P (Geometry.explicitRoundedGrid jStar m) r)

Averaging at the even moment bigQ, with the actual terminal mean as R, then transport from the self normalization. Both the row-average bound and log-det loss are consumed; the row may be empty.

theorem HCPolySupport.HighContrast.Annealed.exists_transport_whitney_coefficients (d : ℕ) (hd : 2 ≤ d) (K₀ : ℝ) (hK₀ : 1 ≤ K₀) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (Csrc : ℝ), 0 < Csrc ∧ ∃ (C : ℝ), 0 < C ∧ ∀ (K : ℝ), 1 < K → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar → ∀ (m mPlus : Mat d), Matrix.PosDef m → Matrix.PosDef mPlus → gridRatio (Geometry.explicitRoundedGrid jStar m) (Geometry.explicitRoundedGrid jStar mPlus) ≤ K₀ → ∀ (j : ℤ) (ell : ℕ), 1 ≤ ell → ∀ y ∈ adaptedLatticeAtScale (Geometry.explicitRoundedGrid jStar mPlus) j, let W := adaptedCellTranslate (Geometry.explicitRoundedGrid jStar mPlus) j y; let q := Geometry.explicitRoundedGrid jStar m; let cap := j - ↑ell; ∃ (hfin : ∀ r ≤ cap, (maximalAdaptedCellCenters W q cap r).Finite), have v := fun (r : ℤ) => (MeasureTheory.volume (adaptedCell q r)).toReal / (MeasureTheory.volume W).toReal; ∑' (r : { r : ℤ // r ≤ cap }), ∑ _z ∈ ⋯.toFinset, v ↑r = 1 ∧ (∑ _z ∈ ⋯.toFinset, v cap ^ 2) ^ (1 / 2) ≤ C * 3 ^ (-↑d / 2 * ↑ell) ∧ ∀ (r : ℤ) (hr : r < cap), (∑ _z ∈ ⋯.toFinset, v r ^ 2) ^ (1 / 2) ≤ C * 3 ^ (-(↑d + 1) / 2 * (↑j - ↑r)) ∧ ∑ _z ∈ ⋯.toFinset, v r ≤ C * 3 ^ (↑r - ↑j)

The Whitney two-grid bound supplies both square-sum coefficients and the actual infinite mass identity. All constants are chosen before the grids and target.

theorem HCPolySupport.HighContrast.Annealed.transport_opNorm_normalizer {d : ℕ} {A B : BlockMat d} (hA : Matrix.PosDef (toFullBlockMat A)) (hB : Matrix.PosDef (toFullBlockMat B)) (X : BlockMat d) : blockOpNorm (normalizedBlock X B) ≤ blockOpNorm (normalizedBlock A B) * blockOpNorm (normalizedBlock X A)

Operator-norm transport is pointwise, so it can be used before any random maximum.

theorem HCPolySupport.HighContrast.Annealed.transport_finite_row_bound {ι : Type u_1} {d : ℕ} (Z : Finset ι) {N A : ℝ} (hN : 1 ≤ N) (w : ι → ℝ) (hw : ∀ z ∈ Z, 0 ≤ w z) (X : ι → BlockMat d) (hX : ∀ z ∈ Z, Matrix.IsHermitian (toFullBlockMat (X z))) (hbound : ∀ z ∈ Z, blockOpNorm (X z) ≤ A) : absSchattenNorm N (ofFullBlockMat (∑ z ∈ Z, w z • toFullBlockMat (X z))) ≤ ((2 * ↑d) ^ N⁻¹ * ∑ z ∈ Z, w z) * A

A positive finite row mass multiplies the maximum of its entry norms. Only the fixed dimension converts its final operator norm to Schatten norm.

theorem HCPolySupport.HighContrast.Annealed.transport_weighted_moment_root (Q : ℕ) (hQ : 0 < Q) {x H b : ℝ} (hx : 0 ≤ x) (hH : 0 ≤ H) (h : 3 ^ (-↑Q * b) * x ^ Q ≤ H) : x ≤ 3 ^ b * H ^ (↑Q)⁻¹

Removing a positive geometric moment weight gives its reciprocal root. This is used on each child before taking the parent maximum.

theorem HCPolySupport.HighContrast.Annealed.transport_old_history_envelope (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 : ℕ) (hj : 2 * d ≤ 3 ^ jStar) (m : Mat d) (hm : Matrix.PosDef m) (qPlus : Mat d) (k t : ℤ) (hk : ↑jStar ≤ k) (hkt : k ≤ t) (h : ℕ) (hcover : adaptedCell qPlus t ⊆ adaptedCell (Geometry.explicitRoundedGrid jStar m) (t + ↑h)) : ∃ (X : CoeffSpace d → ℝ), (∀ (a : CoeffSpace d), 0 ≤ X a) ∧ MeasureTheory.MemLp X (ENNReal.ofReal ↑(bigQ d γ)) P ∧ ∫ (a : CoeffSpace d), X a ^ bigQ d γ ∂P ≤ 3 ^ (d * ((t - k).toNat + h)) * fluctuationHistory P γ (Geometry.explicitRoundedGrid jStar m) jStar k ∧ ∀ r ∈ Set.Icc (↑jStar) k, ∀ (w : Fin d → ℤ), adaptedCellCenter (Geometry.explicitRoundedGrid jStar m) r w ∈ adaptedCell qPlus t → ∀ (a : CoeffSpace d), blockOpNorm (normalizedFluctuation P (Geometry.explicitRoundedGrid jStar m) r k (adaptedCellCenter (Geometry.explicitRoundedGrid jStar m) r w) a) ≤ 3 ^ (rhoMax d γ * (↑k - ↑r)) * X a

A single random envelope controls all old-history generations in the new target. Its moment pays only the finite family of scale-k parents.

theorem HCPolySupport.HighContrast.Annealed.transport_old_history_moment_factor (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (M : BlockMat d) (hM : Matrix.IsHermitian (toFullBlockMat M)) (hIM : BlockMatLoewnerLE (Book.Ch02.blockIdentity d) M) (n k : ℤ) (hnk : k ≤ n) (L : ℕ) : 3 ^ (-↑(bigQ d γ) * rhoMax d γ * (↑n + ↑L - ↑k)) * 3 ^ (↑d * (↑n + ↑L - ↑k)) * blockOpNorm M ^ bigQ d γ ≤ 3 ^ ((1 - γ) / 4 * ↑L) * 3 ^ (-((1 - γ) / 4) * (↑n + 2 * ↑L - ↑k)) * (1 + meanPenalty (bigQ d γ) M)

The old-history norm comparison after taking the Q-th power, including the exact d-dimensional parent-count exponent.

theorem HCPolySupport.HighContrast.Annealed.transport_bulk_high_weight (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (n j : ℤ) (L ell : ℕ) (hjt : j ≤ n + ↑L) : 3 ^ (-↑(bigQ d γ) * rhoMax d γ * (↑n + ↑L - ↑j)) * 3 ^ (↑d * (↑n + ↑L - ↑j)) * (3 ^ (-↑d / 2 * ↑ell)) ^ bigQ d γ ≤ 3 ^ ((1 - γ) / 4 * ↑L) * 3 ^ (-((1 - γ) / 4) * (↑n + 2 * ↑L - (↑j - ↑ell)))

Above k, target counting and averaging leave precisely the old profile weight. Nonnegative gamma and the positive bulk decay exponent pay the rest.

theorem HCPolySupport.HighContrast.Annealed.transport_boundary_high_weight (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (n j r : ℤ) (L : ℕ) (hjt : j ≤ n + ↑L) : have β := (↑d + 1) / 2 - (1 - γ) / (4 * ↑(bigQ d γ)); 3 ^ (-↑(bigQ d γ) * rhoMax d γ * (↑n + ↑L - ↑j)) * 3 ^ (↑d * (↑n + ↑L - ↑j)) * (3 ^ (-(↑d + 1) / 2 * (↑j - ↑r))) ^ bigQ d γ ≤ 3 ^ ((1 - γ) / 4 * ↑L) * (3 ^ (-β * (↑j - ↑r))) ^ bigQ d γ * 3 ^ (-((1 - γ) / 4) * (↑n + 2 * ↑L - ↑r))

Boundary averaging preserves a summable coefficient in the separation of the target and source generations, after the exact target-count loss.

theorem HCPolySupport.HighContrast.Annealed.transport_lq_moment {d Q : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} (hQ : 0 < Q) (H : CoeffSpace d → BlockMat d) (hH : SchattenMemLp P (↑Q) H) : lqSchattenNorm P (↑Q) H ^ Q = ∫ (a : CoeffSpace d), absSchattenNorm (↑Q) (H a) ^ Q ∂P

The mixed norm at the fixed natural moment has the printed Bochner moment. Membership records that this is an integrable random moment.

theorem HCPolySupport.HighContrast.Annealed.exists_transport_lattice_row_moment (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (Csrc : ℝ), 0 < Csrc ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P γ E Ψ K S → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar → ∀ (m : Mat d), Matrix.PosDef m → ∀ (r t : ℤ), ↑jStar ≤ r → r ≤ t → ∀ (Z : Finset (Vec d)), ↑Z ⊆ adaptedLatticeAtScale (Geometry.explicitRoundedGrid jStar m) r → ∀ (v : ℝ), 0 ≤ v → ∀ (A : ℝ), (∑ _z ∈ Z, v ^ 2) ^ (1 / 2) ≤ A → ∫ (a : CoeffSpace d), absSchattenNorm (↑(bigQ d γ)) (ofFullBlockMat (∑ z ∈ Z, v • toFullBlockMat (normalizedFluctuation P (Geometry.explicitRoundedGrid jStar m) r t z a))) ^ bigQ d γ ∂P ≤ (↑(bigQ d γ) * 3 ^ (↑d / 2) * A) ^ bigQ d γ * Real.exp (↑(bigQ d γ) * detIncrement P (Geometry.explicitRoundedGrid jStar m) r t) * ∫ (a : CoeffSpace d), absSchattenNorm (↑(bigQ d γ)) (normalizedFluctuationSelf P (Geometry.explicitRoundedGrid jStar m) r a) ^ bigQ d γ ∂P

The averaging estimate gives the actual row moment, for both Whitney row shapes.

theorem HCPolySupport.HighContrast.Annealed.transport_old_bulk_raw (d : ℕ) (hd : 2 ≤ d) (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ) (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P γ E Ψ K S) (jStar : ℕ) (hj : 2 * d ≤ 3 ^ jStar) (m : Mat d) (hm : Matrix.PosDef m) (qPlus : Mat d) (k n : ℤ) (hk : ↑jStar ≤ k) (hkn : k ≤ n) (L h : ℕ) (hcover : adaptedCell qPlus (n + ↑L) ⊆ adaptedCell (Geometry.explicitRoundedGrid jStar m) (n + ↑L + ↑h)) {ι : Type u_1} (I : Finset ι) (hI : I.Nonempty) (j : ι → ℤ) (Z : ι → Finset (Vec d)) (v : ι → ℝ) (hjgen : ∀ i ∈ I, j i - 1 ∈ Set.Icc (↑jStar) k) (hZ : ∀ i ∈ I, ↑(Z i) ⊆ adaptedLatticeAtScale (Geometry.explicitRoundedGrid jStar m) (j i - 1) ∩ adaptedCell qPlus (n + ↑L)) (hv : ∀ i ∈ I, 0 ≤ v i) (hmass : ∀ i ∈ I, ∑ _z ∈ Z i, v i ≤ 1) : have q := Geometry.explicitRoundedGrid jStar m; have Q := bigQ d γ; have M := relMean P q k (n + 2 * ↑L); have B := (2 * ↑d) ^ (↑Q)⁻¹ * 3 ^ rhoMax d γ * 3 ^ (-rhoMax d γ * (↑n + ↑L - ↑k)) * blockOpNorm M; ∫ (a : CoeffSpace d), (⨆ i ∈ ↑I, 3 ^ (-rhoMax d γ * (↑n + ↑L - ↑(j i))) * absSchattenNorm (↑Q) (ofFullBlockMat (∑ z ∈ Z i, v i • toFullBlockMat (normalizedFluctuation P q (j i - 1) (n + 2 * ↑L) z a)))) ^ ↑Q ∂P ≤ B ^ Q * (3 ^ (d * ((n + ↑L - k).toNat + h)) * fluctuationHistory P γ q jStar k)

The old-history half of the bulk family retains one common envelope under the joint maximum. Its exact coefficient is recorded before absorption.

theorem HCPolySupport.HighContrast.Annealed.transport_old_bulk_mass_factor (d Q : ℕ) (hQ : 0 < Q) (ρ : ℝ) (s : ℤ) (hs : 0 ≤ s) (h : ℕ) (x : ℝ) : ((2 * ↑d) ^ (↑Q)⁻¹ * 3 ^ ρ * 3 ^ (-ρ * ↑s) * x) ^ Q * 3 ^ (d * (s.toNat + h)) = 2 * ↑d * 3 ^ (↑Q * ρ + ↑d * ↑h) * (3 ^ (-↑Q * ρ * ↑s) * 3 ^ (↑d * ↑s) * x ^ Q)

Exact cancellation of the root dimension factor and parent cardinality against the old-history weight. The enlargement contributes only 3^(d*h).

theorem HCPolySupport.HighContrast.Annealed.transport_old_history_profile_payment (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 : ℕ) (hj : 2 * d ≤ 3 ^ jStar) (m : Mat d) (hm : Matrix.PosDef m) (k n : ℤ) (hk : ↑jStar ≤ k) (hkn : k ≤ n) (L h : ℕ) : have q := Geometry.explicitRoundedGrid jStar m; have Q := bigQ d γ; have M := relMean P q k (n + 2 * ↑L); have B := (2 * ↑d) ^ (↑Q)⁻¹ * 3 ^ rhoMax d γ * 3 ^ (-rhoMax d γ * (↑n + ↑L - ↑k)) * blockOpNorm M; B ^ Q * (3 ^ (d * ((n + ↑L - k).toNat + h)) * fluctuationHistory P γ q jStar k) ≤ 2 * ↑d * 3 ^ (↑Q * rhoMax d γ + ↑d * ↑h) * 3 ^ ((1 - γ) / 4 * ↑L) * profile P γ q jStar k (n + 2 * ↑L)

The powered old-history factor is paid by the first profile component. The constant records the fixed enlargement of the parent family.

theorem HCPolySupport.HighContrast.Annealed.transport_old_bulk_profile_bound (d : ℕ) (hd : 2 ≤ d) (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ) (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P γ E Ψ K S) (jStar : ℕ) (hj : 2 * d ≤ 3 ^ jStar) (m : Mat d) (hm : Matrix.PosDef m) (qPlus : Mat d) (k n : ℤ) (hk : ↑jStar ≤ k) (hkn : k ≤ n) (L h : ℕ) (hcover : adaptedCell qPlus (n + ↑L) ⊆ adaptedCell (Geometry.explicitRoundedGrid jStar m) (n + ↑L + ↑h)) {ι : Type u_1} (I : Finset ι) (hI : I.Nonempty) (j : ι → ℤ) (Z : ι → Finset (Vec d)) (v : ι → ℝ) (hjgen : ∀ i ∈ I, j i - 1 ∈ Set.Icc (↑jStar) k) (hZ : ∀ i ∈ I, ↑(Z i) ⊆ adaptedLatticeAtScale (Geometry.explicitRoundedGrid jStar m) (j i - 1) ∩ adaptedCell qPlus (n + ↑L)) (hv : ∀ i ∈ I, 0 ≤ v i) (hmass : ∀ i ∈ I, ∑ _z ∈ Z i, v i ≤ 1) : have q := Geometry.explicitRoundedGrid jStar m; have Q := bigQ d γ; ∫ (a : CoeffSpace d), (⨆ i ∈ ↑I, 3 ^ (-rhoMax d γ * (↑n + ↑L - ↑(j i))) * absSchattenNorm (↑Q) (ofFullBlockMat (∑ z ∈ Z i, v i • toFullBlockMat (normalizedFluctuation P q (j i - 1) (n + 2 * ↑L) z a)))) ^ ↑Q ∂P ≤ 2 * ↑d * 3 ^ (↑Q * rhoMax d γ + ↑d * ↑h) * 3 ^ ((1 - γ) / 4 * ↑L) * profile P γ q jStar k (n + 2 * ↑L)

The old bulk family is paid by the first summand of the actual profile.

theorem HCPolySupport.HighContrast.Annealed.exists_transport_high_boundary_profile (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (Csrc : ℝ), 0 < Csrc ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P γ E Ψ K S → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar → ∀ (m : Mat d), Matrix.PosDef m → ∀ (k n : ℤ), ↑jStar ≤ k → k ≤ n → ∀ (L : ℕ) (D : ℝ), 0 ≤ D → have q := Geometry.explicitRoundedGrid jStar m; have Q := bigQ d γ; have β := (↑d + 1) / 2 - (1 - γ) / (4 * ↑Q); have M := 1 + 1 / (1 - 3 ^ (-β)); ∀ (I : Finset (ℤ × (Fin d → ℤ))), I.Nonempty → ∀ (T : ℤ → Finset ℤ) (Z : ℤ × (Fin d → ℤ) → ℤ → Finset (Vec d)) (v : ℤ × (Fin d → ℤ) → ℤ → ℝ), (∀ j ∈ Finset.image Prod.fst I, T j ⊆ Finset.Icc (k + 1) j) → (∀ i ∈ I, i.1 ≤ n + ↑L) → (∀ j ∈ Finset.image Prod.fst I, ↑{i ∈ I | i.1 = j}.card ≤ 3 ^ (↑d * (↑n + ↑L - ↑j))) → (∀ i ∈ I, ∀ r ∈ T i.1, ↑(Z i r) ⊆ adaptedLatticeAtScale q r) → (∀ i ∈ I, ∀ r ∈ T i.1, 0 ≤ v i r) → (∀ i ∈ I, ∀ r ∈ T i.1, (∑ _z ∈ Z i r, v i r ^ 2) ^ (1 / 2) ≤ D * 3 ^ (-(↑d + 1) / 2 * (↑i.1 - ↑r))) → ∫ (a : CoeffSpace d), (⨆ i ∈ ↑I, 3 ^ (-rhoMax d γ * (↑n + ↑L - ↑i.1)) * ∑ r ∈ T i.1, absSchattenNorm (↑Q) (ofFullBlockMat (∑ z ∈ Z i r, v i r • toFullBlockMat (normalizedFluctuation P q r (n + 2 * ↑L) z a)))) ^ ↑Q ∂P ≤ M ^ (Q + 1) * (↑Q * 3 ^ (↑d / 2) * D) ^ Q * 3 ^ ((1 - γ) / 4 * ↑L) * profile P γ q jStar k (n + 2 * ↑L)

The boundary rows above k are paid by the final profile sum. Weighted convexity is applied before exchanging the target and source generations.