High-contrast homogenization: Entry.Annealed.TransportMeans

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

Mean comparison for the two-grid transport

This module proves the mean comparison of p.two.grid.transport on the rounded grid: the boundary mean-row weight sums that concentrate the coarse-block weight on the deepest scale, the Whitney mean bound that decomposes the mean penalty into its bulk, boundary and fine-tail parts, and the geometric-series, generation-fiber and weighted power-sum estimates that keep the two decay powers of the fine amplitude separate. It also records the parent-center shift identifying a child fluctuation with a translated one and the weighted history bound for its moment.

theorem HCPolySupport.HighContrast.Annealed.transport_source_two_powers (Q : ℕ) (hQ : 1 ≤ Q) {A B z : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hz : 0 ≤ z) : A * B * z + (A * B * z) ^ Q ≤ (A + A ^ Q) * B ^ Q * (z + z ^ Q)

A geometric source amplitude at least one absorbs both the linear and Q-th-power scalar errors without changing their distinct decay powers.

theorem HCPolySupport.HighContrast.Annealed.transport_boundary_mean_row_weights {γ Cw : ℝ} (hγ : 0 ≤ γ) (hCw : 0 ≤ Cw) (J cap j : ℤ) (hJ : J ≤ cap) (hcap : cap ≤ j) (lam M : ℤ → ℝ) (hlam : ∀ r ∈ Finset.Icc J cap, 0 ≤ lam r) (hM : ∀ r ∈ Finset.Icc J cap, 0 ≤ M r) (hmass : ∑ r ∈ Finset.Icc J cap, lam r ≤ 1) (hrow : ∀ r ∈ Finset.Icc J (cap - 1), lam r ≤ Cw * 3 ^ (↑r - ↑j)) : ∑ r ∈ Finset.Icc J cap, lam r * M r ≤ (1 + Cw) * (M cap + ∑ r ∈ Finset.Icc J (cap - 1), 3 ^ (-(1 - γ) * (↑j - ↑r)) * M r)

The cap has mass at most one; only the smaller rows use the boundary mass estimate. Weakening 3^(r−j) preserves the printed (1−γ)-decay.

theorem HCPolySupport.HighContrast.Annealed.transport_whitney_mean_bound (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (Q : ℕ) (hQ : 1 ≤ Q) (Cfine Cw : ℝ) (hCfine : 0 ≤ Cfine) (hCw : 0 ≤ Cw) : ∃ (C : ℝ), 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 → ∀ (m mPlus : Mat d), Matrix.PosDef m → Matrix.PosDef mPlus → ∀ (oldEnd newEnd j cap : ℤ), ↑jStar ≤ cap → cap ≤ oldEnd → cap ≤ j → ∀ (W : Set (Vec d)) (hfin : ∀ r ≤ cap, (maximalAdaptedCellCenters W (Geometry.explicitRoundedGrid jStar m) cap r).Finite) (B : ℝ), 1 ≤ B → ∀ (X : CoeffSpace d → ℝ), MeasureTheory.Integrable X P → ∫ (a : CoeffSpace d), X a ∂P ≤ 2 → ∀ δ ∈ 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 (r : ℤ) => if hr : r ≤ cap then ⋯.toFinset else ∅; have lam := fun (r : ℤ) => ∑ _z ∈ Z r, (MeasureTheory.volume (adaptedCell q r)).toReal / (MeasureTheory.volume W).toReal; 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 MG := ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (G a) α β ∂P); have decay := 3 ^ (-(1 - γ) * (↑j - ↑jStar)); BlockMatLoewnerLE (blockScale (1 - δ) F) H → BlockMatLoewnerLE H (blockScale (1 + δ) F) → SchattenMemLp P (↑Q) G → SchattenMemLp P (↑Q) 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 (Cfine * B * decay * X a) (Book.Ch02.blockIdentity d))) → BlockMatLoewnerLE (Book.Ch02.blockIdentity d) MG → ∑ r ∈ Finset.Icc (↑jStar) cap, lam r ≤ 1 → (∀ r ∈ Finset.Icc (↑jStar) (cap - 1), lam r ≤ Cw * 3 ^ (↑r - ↑j)) → meanPenalty Q MG ≤ C * ⋯

p.two.grid.transport, expanded to include its actual premises and derivation. Cfine and Cw are the law-independent source and Whitney constants. The fine amplitude B is geometric; its two decay powers remain separate. Total mass, boundary row mass and the fine-tail hypotheses are exactly the corresponding outputs of the Whitney and source constructions.

theorem HCPolySupport.HighContrast.Annealed.transport_bulk_generation_fiber (k : ℤ) (L : ℕ) (r : ℤ) : {j : ℤ | (j - if j ≤ k + ↑L then 1 else ↑L) = r} ⊆ {r + 1, r + ↑L}

Every source generation occurs for at most the two targets r+1 and r+L.

theorem HCPolySupport.HighContrast.Annealed.transport_profile_components (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 t : ℤ) (hk : ↑jStar ≤ k) (hkt : k ≤ t) : have q := Geometry.explicitRoundedGrid jStar m; have A := 3 ^ (-((1 - γ) / 4) * (↑t - ↑k)) * (1 + meanPenalty (bigQ d γ) (relMean P q k t)); A * fluctuationHistory P γ q jStar k ≤ profile P γ q jStar k t ∧ A * history P γ q jStar k ≤ profile P γ q jStar k t ∧ meanHistory P γ q k t ≤ profile P γ q jStar k t ∧ ∑ r ∈ Finset.Icc (k + 1) t, 3 ^ (-((1 - γ) / 4) * (↑t - ↑r)) * Real.exp (↑(bigQ d γ) * detIncrement P q r t) * ∫ (a : CoeffSpace d), absSchattenNorm (↑(bigQ d γ)) (normalizedFluctuationSelf P q r a) ^ bigQ d γ ∂P ≤ profile P γ q jStar k t

The profile pays for each of its three nonnegative components. Its first component pays for the fluctuation history while retaining the mean history.

theorem HCPolySupport.HighContrast.Annealed.transport_geometric_Icc (a : ℝ) (ha : 0 < a) (J cap : ℤ) : 0 < 1 - 3 ^ (-a) ∧ ∑ r ∈ Finset.Icc J cap, 3 ^ (-a * (↑cap - ↑r)) ≤ 1 / (1 - 3 ^ (-a))

Reverse integer geometric weights are bounded uniformly in both endpoints, including an empty interval. The denominator is recorded with its positivity.

theorem HCPolySupport.HighContrast.Annealed.transport_bulk_generation_sum (k : ℤ) (L : ℕ) (S T : Finset ℤ) (f : ℤ → ℝ) (hf : ∀ r ∈ T, 0 ≤ f r) (hmap : ∀ j ∈ S, (j - if j ≤ k + ↑L then 1 else ↑L) ∈ T) : ∑ j ∈ S, f (j - if j ≤ k + ↑L then 1 else ↑L) ≤ 2 * ∑ r ∈ T, f r

The actual bulk generation map charges each old summand at most twice. This remains valid when either finite range is empty.

theorem HCPolySupport.HighContrast.Annealed.transport_weighted_power_sum {ι : Type u_1} (Q : ℕ) (hQ : 0 < Q) (s : Finset ι) (w x : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) (hx : ∀ i ∈ s, 0 ≤ x i) {M : ℝ} (hM : 1 ≤ M) (hs : ∑ i ∈ s, w i ≤ M) : (∑ i ∈ s, w i * x i) ^ Q ≤ M ^ Q * ∑ i ∈ s, w i * x i ^ Q

Weighted convexity uses a bound on total weight, without charging the number of summands. The missing weight is placed at zero.

theorem HCPolySupport.HighContrast.Annealed.transport_weighted_moment_sum {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] {P : MeasureTheory.Measure α} (Q : ℕ) (hQ : 0 < Q) (s : Finset ι) (w : ι → ℝ) (hw : ∀ i ∈ s, 0 < w i) (f : ι → α → ℝ) (hf0 : ∀ i ∈ s, ∀ᵐ (a : α) ∂P, 0 ≤ f i a) (hf : ∀ i ∈ s, MeasureTheory.MemLp (f i) (ENNReal.ofReal ↑Q) P) {M : ℝ} (hM : 1 ≤ M) (hs : ∑ i ∈ s, w i ≤ M) : MeasureTheory.Integrable (fun (a : α) => (∑ i ∈ s, f i a) ^ Q) P ∧ ∫ (a : α), (∑ i ∈ s, f i a) ^ Q ∂P ≤ M ^ Q * ∑ i ∈ s, w i * (w i)⁻¹ ^ Q * ∫ (a : α), f i a ^ Q ∂P

The weighted power estimate for integrable random moments, including empty generation ranges. Positivity and finite moments are explicit guards.

theorem HCPolySupport.HighContrast.Annealed.transport_geometric_forward (a : ℝ) (ha : 0 < a) (J cap : ℤ) : ∑ r ∈ Finset.Icc J cap, 3 ^ (-a * (↑r - ↑J)) ≤ 1 / (1 - 3 ^ (-a))

Forward geometric weights have the same endpoint-independent sum bound.

theorem HCPolySupport.HighContrast.Annealed.transport_geometric_convolution (a : ℝ) (ha : 0 < a) (S U : Finset ℤ) (T : ℤ → Finset ℤ) (t : ℤ) (hst : ∀ j ∈ S, j ≤ t) (hTU : ∀ j ∈ S, T j ⊆ U) (hTj : ∀ j ∈ S, ∀ r ∈ T j, r ≤ j) (F : ℤ → ℝ) (hF : ∀ r ∈ U, 0 ≤ F r) : ∑ j ∈ S, ∑ r ∈ T j, 3 ^ (-a * (↑j - ↑r)) * F r ≤ 1 / (1 - 3 ^ (-a)) * ∑ r ∈ U, F r

Interchanging the finite target/source sums costs only one geometric mass, even when the generation ranges depend on the target generation.

theorem HCPolySupport.HighContrast.Annealed.transport_target_fiber_card {d : ℕ} (I : Finset (ℤ × (Fin d → ℤ))) (t : ℤ) (hgen : ∀ i ∈ I, i.1 ≤ t) (hcenter : ∀ i ∈ I, standardCellCenter i.1 i.2 ∈ centeredCube d t) (j : ℤ) (hj : j ∈ Finset.image Prod.fst I) : ↑{i ∈ I | i.1 = j}.card ≤ 3 ^ (↑d * (↑t - ↑j))

Any selected target family has the actual aligned target-count bound.

theorem HCPolySupport.HighContrast.Annealed.transport_maximal_centers_subset {d : ℕ} (W : Set (Vec d)) (q : Mat d) (cap r : ℤ) : maximalAdaptedCellCenters W q cap r ⊆ adaptedLatticeAtScale q r ∩ W

An actual maximal cell center lies in its target and in the old lattice.

theorem HCPolySupport.HighContrast.Annealed.transport_joint_sum_moment {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] {P : MeasureTheory.Measure α} (Q : ℕ) (hQ : 0 < Q) (I : Finset ι) (hI : I.Nonempty) (f g : ι → α → ℝ) (hf0 : ∀ i ∈ I, ∀ᵐ (a : α) ∂P, 0 ≤ f i a) (hg0 : ∀ i ∈ I, ∀ᵐ (a : α) ∂P, 0 ≤ g i a) (hf : ∀ i ∈ I, MeasureTheory.MemLp (f i) (ENNReal.ofReal ↑Q) P) (hg : ∀ i ∈ I, MeasureTheory.MemLp (g i) (ENNReal.ofReal ↑Q) P) : ∫ (a : α), (⨆ i ∈ ↑I, f i a + g i a) ^ ↑Q ∂P ≤ 2 ^ Q * (∫ (a : α), (⨆ i ∈ ↑I, f i a) ^ ↑Q ∂P + ∫ (a : α), (⨆ i ∈ ↑I, g i a) ^ ↑Q ∂P)

Two nonnegative random families can be combined under the same joint maximum, paying only the fixed power constant.

theorem HCPolySupport.HighContrast.Annealed.transport_joint_union_moment {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] [DecidableEq ι] {P : MeasureTheory.Measure α} (Q : ℕ) (hQ : 0 < Q) (I J : Finset ι) (f : ι → α → ℝ) (hf0 : ∀ i ∈ I ∪ J, ∀ᵐ (a : α) ∂P, 0 ≤ f i a) (hf : ∀ i ∈ I ∪ J, MeasureTheory.MemLp (f i) (ENNReal.ofReal ↑Q) P) : ∫ (a : α), (⨆ i ∈ ↑(I ∪ J), f i a) ^ ↑Q ∂P ≤ ∫ (a : α), (⨆ i ∈ ↑I, f i a) ^ ↑Q ∂P + ∫ (a : α), (⨆ i ∈ ↑J, f i a) ^ ↑Q ∂P

A union of target families is paid by the sum of their moments. Either subfamily may be empty; no generation-count factor is introduced.

theorem HCPolySupport.HighContrast.Annealed.transport_uniform_row_average {ι : Type u_1} {d : ℕ} (Z : Finset ι) (hZ : Z.Nonempty) (v : ℝ) (F : ι → FullBlockMat d) : ∑ z ∈ Z, v • F z = (↑Z.card * v) • (↑Z.card)⁻¹ • ∑ z ∈ Z, F z

An equal-volume row is its relative mass times its unweighted average.

theorem HCPolySupport.HighContrast.Annealed.exists_transport_lattice_row_average (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 → ∀ (N : ℕ), 2 ≤ N → Even N → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar → ∀ (m : Mat d), Matrix.PosDef m → ∀ (j : ℤ), ↑jStar ≤ j → ∀ (Z : Finset (Vec d)), ↑Z ⊆ adaptedLatticeAtScale (Geometry.explicitRoundedGrid jStar m) j → ∀ (R : BlockMat d), IsSymmetricBlockMat R → Book.Ch02.BlockPosDef R → ∀ (v : ℝ), 0 ≤ v → (lqSchattenNorm P ↑N fun (a : CoeffSpace d) => ofFullBlockMat (∑ z ∈ Z, v • toFullBlockMat (normalizedBlock (blockSub (coarseBlock (adaptedCellTranslate (Geometry.explicitRoundedGrid jStar m) j z) a) (adaptedMean P (Geometry.explicitRoundedGrid jStar m) j)) R))) ≤ ↑Z.card * v * (↑N * 3 ^ (↑d / 2) / ↑Z.card ^ (1 / 2)) * lqSchattenNorm P ↑N fun (a : CoeffSpace d) => normalizedBlock (blockSub (coarseBlock (adaptedCell (Geometry.explicitRoundedGrid jStar m) j) a) (adaptedMean P (Geometry.explicitRoundedGrid jStar m) j)) R

The averaging estimate is instantiated at the actual lattice row (N,j,Z,R). The standing unit-range law is consumed here. The empty row has zero norm.

theorem HCPolySupport.HighContrast.Annealed.transport_row_square_sum_bound {ι : Type u_1} (Z : Finset ι) {C v a b : ℝ} (hC : 0 ≤ C) (hv : 0 ≤ v) (hcard : ↑Z.card ≤ C * 3 ^ b) (hvol : v ≤ C * 3 ^ (-a)) : (∑ _z ∈ Z, v ^ 2) ^ (1 / 2) ≤ C * √C * 3 ^ (b / 2 - a)

Count times equal cell volume gives the square-sum coefficient, with no nonempty-row assumption. Exponents b=d ell or b=(d-1)(j-r) give both rows.

theorem HCPolySupport.HighContrast.Annealed.transport_boundary_decay_pos (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : 0 < (↑d + 1) / 2 - (1 - γ) / (4 * ↑(bigQ d γ))

Boundary averaging has still more geometric decay than bulk averaging.

theorem HCPolySupport.HighContrast.Annealed.transport_old_history_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 ^ (-(rhoMax d γ - ↑d / ↑(bigQ d γ)) * (↑n + ↑L - ↑k)) * blockOpNorm M ≤ 3 ^ ((1 - γ) / (4 * ↑(bigQ d γ)) * ↑L) * 3 ^ (-(1 - γ) / (4 * ↑(bigQ d γ)) * (↑n + 2 * ↑L - ↑k)) * (1 + meanPenalty (bigQ d γ) M) ^ (↑(bigQ d γ))⁻¹

The old-history factor uses the trace penalty at scale k, with the d/Q loss from counting the old parents.

theorem HCPolySupport.HighContrast.Annealed.transport_target_count_weight (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (s : ℝ) : 3 ^ (-↑(bigQ d γ) * rhoMax d γ * s) * 3 ^ (↑d * s) = 3 ^ (-↑(bigQ d γ) * (γ + (1 - γ) / (4 * ↑(bigQ d γ))) * s)

The exact target count changes rho to rho-d/Q. This is the loss paid before applying the averaging estimate.

theorem HCPolySupport.HighContrast.Annealed.transport_boundary_history_sum {ρ : ℝ} (hρ : ρ < 1) (J cap k j : ℤ) : ∑ r ∈ Finset.Icc J cap, 3 ^ (↑r - ↑j) * 3 ^ (ρ * (↑k - ↑r)) ≤ 1 / (1 - 3 ^ (-(1 - ρ))) * 3 ^ (↑cap - ↑j + ρ * (↑k - ↑cap))

The boundary history convolution before choosing the branch j≥k or j<k.

theorem HCPolySupport.HighContrast.Annealed.transport_boundary_history_below {ρ : ℝ} (hρ : ρ < 1) (J cap k j : ℤ) (hcap : cap ≤ j) : ∑ r ∈ Finset.Icc J cap, 3 ^ (↑r - ↑j) * 3 ^ (ρ * (↑k - ↑r)) ≤ 1 / (1 - 3 ^ (-(1 - ρ))) * 3 ^ (ρ * (↑k - ↑j))

For j<k the boundary history coefficient has 3^(rho(k-j)) growth. The same bound applies to the first branch since rho<1.

theorem HCPolySupport.HighContrast.Annealed.transport_parent_center_shift {d : ℕ} (q : Mat d) (r k : ℤ) (hrk : r ≤ k) (w v : Fin d → ℤ) : ∃ (u : Fin d → ℤ), adaptedCellCenter q r u + adaptedCellCenter q k v = adaptedCellCenter q r w ∧ (adaptedCellCenter q r w ∈ adaptedCellAtCenter q k v → adaptedCellCenter q r u ∈ adaptedCell q k)

Subtracting a scale-k parent center leaves an aligned scale-r center. The child center then lies in the untranslated parent used by the history.

theorem HCPolySupport.HighContrast.Annealed.transport_parent_fluctuation_shift (d jStar : ℕ) (m : Mat d) (k : ℤ) (hk : ↑jStar ≤ k) (v : Fin d → ℤ) : ∃ (p : Fin d → ℤ), ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (r t : ℤ), r ≤ k → ∀ (w : Fin d → ℤ), adaptedCellCenter (Geometry.explicitRoundedGrid jStar m) r w ∈ adaptedCellAtCenter (Geometry.explicitRoundedGrid jStar m) k v → ∃ z ∈ adaptedLatticeAtScale (Geometry.explicitRoundedGrid jStar m) r ∩ adaptedCell (Geometry.explicitRoundedGrid jStar m) k, ∀ (a : CoeffSpace d), normalizedFluctuation P (Geometry.explicitRoundedGrid jStar m) r t (adaptedCellCenter (Geometry.explicitRoundedGrid jStar m) r w) a = normalizedFluctuation P (Geometry.explicitRoundedGrid jStar m) r t z (translateCoeff p a)

One parent translation works simultaneously for every child generation; this pointwise equality therefore survives the joint maximum.

theorem HCPolySupport.HighContrast.Annealed.transport_history_centers {d : ℕ} (q : Mat d) (hq : IsUnit q) (r k : ℤ) (hrk : r ≤ k) : (adaptedLatticeAtScale q r ∩ adaptedCell q k).Finite ∧ (adaptedLatticeAtScale q r ∩ adaptedCell q k).Nonempty

The history's actual center set is a finite nonempty image of an aligned integer box. This supplies the boundedness needed when using its real suprema.

theorem HCPolySupport.HighContrast.Annealed.transport_history_pointwise {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (γ : ℝ) (q : Mat d) (hq : IsUnit q) (jStar : ℕ) (k r : ℤ) (hr : r ∈ Set.Icc (↑jStar) k) (z : Vec d) (hz : z ∈ adaptedLatticeAtScale q r ∩ adaptedCell q k) (a : CoeffSpace d) : 3 ^ (-↑(bigQ d γ) * rhoMax d γ * (↑k - ↑r)) * blockOpNorm (normalizedFluctuation P q r k z a) ^ bigQ 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 chosen child moment is bounded by the single joint history integrand. No sum over source generations is introduced.