High-contrast homogenization: Entry.Response.Direct.DescendantEnvelopeBound

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

The increment envelope of the descendant sum, and its summable bound against the source load

The generation increments of the descendant sum are flat averages, over one generation's cells, of a cutoff weight of size K 3^{-n} against the crossed pairing of the dual variable with the cell average of the optimizer state; Cauchy-Schwarz bounds such an increment by K 3^{-n} times the square root of the annealed mean of the squared head, giving a nonnegative envelope whose series of annealed means is summable because the source load bounds the head and the terminal energy bounds the cell energy. Shifting the generation index up by one, to meet the layer below the scale-s cells, costs only the fixed factor 3^{3/2}, since every summand and the dropped head are nonnegative and the weighted square roots this step consumes are themselves summable by the arithmetic-geometric mean inequality. Summing the resulting bound over the descendant generations, each weighted by 3^{3(k-s)/2}, closes the descendant sum of the cutoff-oscillation pairings against the source load. This is the summability and domination input that the response transfer p.response.transfer consumes for its descendant sum.

A nonnegative series with summable annealed means

The increment envelope of the descendant sum of p.response.transfer is built generation by generation, and what the carriers control is the annealed mean of each generation: the layer load bounds the head and the terminal energy bounds the cell energy, so the series of annealed means is summable. Monotone convergence turns that single fact into the two hypotheses the descendant limit consumes: the series converges along almost every sample, and its sum is P-integrable.

Nothing here is specific to the response transfer; the statement is the Beppo Levi theorem for a nonnegative family of integrable functions indexed by the generations.

theorem HCPolySupport.HighContrast.Multiscale.aeSummable_and_integrable_tsum_of_summable_integral {α : Type u_1} [MeasurableSpace α] (P : MeasureTheory.Measure α) (g : ℕ → α → ℝ) (hg0 : ∀ (n : ℕ) (a : α), 0 ≤ g n a) (hgint : ∀ (n : ℕ), MeasureTheory.Integrable (g n) P) (hgS : Summable fun (n : ℕ) => ∫ (a : α), g n a ∂P) : (∀ᵐ (a : α) ∂P, Summable fun (n : ℕ) => g n a) ∧ MeasureTheory.Integrable (fun (a : α) => ∑' (n : ℕ), g n a) P

Beppo Levi for a nonnegative generation series. A nonnegative family of P-integrable functions whose annealed means form a summable series converges along almost every sample, and its sample sum is P-integrable.

This is the producer of the henvsum and henvI hypotheses of the descendant limit: the carriers supply a summable bound on ∫ env n alone.

The increment envelope of the descendant sum

The generation increments of the descendant sum of p.response.transfer are flat averages, over the cells of one generation, of a cutoff weight of size K 3^{-n} against the crossed pairing of the deterministic dual variable with the cell average of the optimizer state. Cauchy--Schwarz over the cells bounds such an increment by K 3^{-n} times the square root of the flat head energy times the square root of the flat cell energy, and Young's inequality with the weight 3^{-n/2} splits that product into

(K/2) (3^{-3n/2} · flat head energy + 3^{-n/2} · flat cell energy) ,

which is the envelope below. Its annealed mean is summable, because the head energy is summable against 3^{-3n/2} (that is the source load) and the cell energy is bounded by the terminal energy at every depth; monotone convergence then makes the envelope series converge along almost every sample with a P-integrable sum. Nothing here uses a moment of the coefficient field.

noncomputable def HCPolySupport.HighContrast.Multiscale.descendantEnvelope {iota : Type u_1} {alpha : Type u_2} (Z : ℕ → Finset iota) (G D : ℕ → iota → alpha → ℝ) (K : ℝ) (n : ℕ) (a : alpha) : ℝ

The increment envelope of the descendant sum: Young's splitting, with the weight 3^{-n/2}, of K 3^{-n} times the Cauchy--Schwarz product of the flat head energy and the flat cell energy of the generation-n cells.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.Multiscale.descendantEnvelope_nonneg {iota : Type u_1} {alpha : Type u_2} (Z : ℕ → Finset iota) (G D : ℕ → iota → alpha → ℝ) (K : ℝ) (hK : 0 ≤ K) (hD : ∀ (n : ℕ), ∀ W ∈ Z n, ∀ (a : alpha), 0 ≤ D n W a) (n : ℕ) (a : alpha) : 0 ≤ descendantEnvelope Z G D K n a

The envelope is nonnegative.

theorem HCPolySupport.HighContrast.Multiscale.mul_rpow_neg_sqrt_mul_sqrt_le {K X Y : ℝ} (hK : 0 ≤ K) (hX : 0 ≤ X) (hY : 0 ≤ Y) (n : ℕ) : K * 3 ^ (-↑n) * (√X * √Y) ≤ K / 2 * (3 ^ (-(3 / 2) * ↑n) * X + 3 ^ (-(1 / 2) * ↑n) * Y)

Young's splitting of the geometric Cauchy--Schwarz product. For nonnegative X, Y and K, the product K 3^{-n} √X √Y is at most (K/2)(3^{-3n/2} X + 3^{-n/2} Y).

theorem HCPolySupport.HighContrast.Multiscale.abs_flat_weighted_pairing_le_descendantEnvelope {iota : Type u_1} {alpha : Type u_2} (Z : ℕ → Finset iota) (θ : ℕ → iota → ℝ) (pairing G D : ℕ → iota → alpha → ℝ) (K : ℝ) (hK : 0 ≤ K) (hθ : ∀ (n : ℕ), ∀ W ∈ Z n, |θ n W| ≤ K * 3 ^ (-↑n)) (hG : ∀ (n : ℕ), ∀ W ∈ Z n, ∀ (a : alpha), 0 ≤ G n W a) (hD : ∀ (n : ℕ), ∀ W ∈ Z n, ∀ (a : alpha), 0 ≤ D n W a) (hbd : ∀ (n : ℕ), ∀ W ∈ Z n, ∀ (a : alpha), |pairing n W a| ≤ G n W a * √(2 * D n W a)) (n : ℕ) (a : alpha) : |(↑(Z n).card)⁻¹ * ∑ W ∈ Z n, θ n W * pairing n W a| ≤ descendantEnvelope Z G D K n a

The envelope dominates the generation increment. With cutoff weights of size K 3^{-n} and a crossed pairing bounded by the head times the square root of twice the cell energy, the flat average defining the generation-n increment is at most the envelope.

theorem HCPolySupport.HighContrast.Multiscale.aeSummable_and_integrable_tsum_descendantEnvelope {iota : Type u_1} {alpha : Type u_2} [MeasurableSpace alpha] (P : MeasureTheory.Measure alpha) (Z : ℕ → Finset iota) (G D : ℕ → iota → alpha → ℝ) (L : ℕ → ℝ) (K EJ : ℝ) (hK : 0 ≤ K) (hD : ∀ (n : ℕ), ∀ W ∈ Z n, ∀ (a : alpha), 0 ≤ D n W a) (hGsq : ∀ (n : ℕ), ∫ (a : alpha), (↑(Z n).card)⁻¹ * ∑ W ∈ Z n, G n W a ^ 2 ∂P ≤ L n) (hDval : ∀ (n : ℕ), ∫ (a : alpha), (↑(Z n).card)⁻¹ * ∑ W ∈ Z n, 2 * D n W a ∂P ≤ 2 * EJ) (hFint : ∀ (n : ℕ), MeasureTheory.Integrable (fun (a : alpha) => (↑(Z n).card)⁻¹ * ∑ W ∈ Z n, G n W a ^ 2) P) (hDint : ∀ (n : ℕ), MeasureTheory.Integrable (fun (a : alpha) => (↑(Z n).card)⁻¹ * ∑ W ∈ Z n, 2 * D n W a) P) (hsum : Summable fun (n : ℕ) => 3 ^ (-(3 / 2) * ↑n) * L n) : (∀ᵐ (a : alpha) ∂P, Summable fun (n : ℕ) => descendantEnvelope Z G D K n a) ∧ MeasureTheory.Integrable (fun (a : alpha) => ∑' (n : ℕ), descendantEnvelope Z G D K n a) P

The envelope series converges along almost every sample, with an integrable sum. The annealed mean of the generation-n envelope is at most (K/2)(3^{-3n/2} L n + 3^{-n/2} 2 E[J]), where L is the layer head energy of the source load and E[J] bounds the cell energy at every depth. That series is summable, so monotone convergence gives both hypotheses the descendant limit consumes.

The shifted descendant layers against the source load

The descendant sum of p.response.transfer meets the layer one generation below the scale-s cells. Shifting the generation index upward costs the single factor 3^{3/2}, since every summand is nonnegative and the dropped head is nonnegative; and the weighted square roots the descendant Cauchy--Schwarz consumes are summable by the arithmetic--geometric mean inequality.

theorem HCPolySupport.HighContrast.Multiscale.summable_rpow_neg_mul_sqrt_of_summable (L : ℕ → ℝ) (hL : ∀ (n : ℕ), 0 ≤ L n) (hsum : Summable fun (n : ℕ) => 3 ^ (-(3 / 2) * ↑n) * L n) : Summable fun (n : ℕ) => 3 ^ (-↑n) * √(L n)

Summability of the weighted square roots of the descendant layers. If the load family 3^{-3n/2} L n is summable and every layer is nonnegative, then the family 3^{-n} √(L n) that the descendant Cauchy--Schwarz consumes is summable, because 3^{-n} √(L n) ≤ ½ (3^{-n/2} + 3^{-3n/2} L n).

theorem HCPolySupport.HighContrast.Multiscale.tsum_succ_layer_le_respSourceLoad {d : ℕ} [NeZero d] (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (s : ℤ) (b : CoeffSpace d → CoeffField d) (Y : BlockVec d) (hsum : Summable fun (n : ℕ) => 3 ^ (-(3 / 2) * ↑n) * ((↑(triadicIndexBox d n).card)⁻¹ * ∑ z ∈ triadicIndexBox d n, (√(vecDot Y.1 (matVecMul (annealedBlockOf P (adaptedCellAtCenter (respGrid jStar F) (s - ↑n) z) b).upperLeft Y.1)) + √(vecDot Y.2 (matVecMul (annealedBlockOf P (adaptedCellAtCenter (respGrid jStar F) (s - ↑n) z) b).lowerRight Y.2))) ^ 2)) : ∑' (n : ℕ), 3 ^ (-(3 / 2) * ↑n) * ((↑(triadicIndexBox d (n + 1)).card)⁻¹ * ∑ z ∈ triadicIndexBox d (n + 1), (√(vecDot Y.1 (matVecMul (annealedBlockOf P (adaptedCellAtCenter (respGrid jStar F) (s - ↑(n + 1)) z) b).upperLeft Y.1)) + √(vecDot Y.2 (matVecMul (annealedBlockOf P (adaptedCellAtCenter (respGrid jStar F) (s - ↑(n + 1)) z) b).lowerRight Y.2))) ^ 2) ≤ 3 ^ (3 / 2) * respSourceLoad P jStar F s b Y

The shifted descendant layers are dominated by the source load. Summing the layers from depth one, with the weights of depth zero, costs at most the factor 3^{3/2} against the source load 𝓛_s of p.response.transfer.

The descendant sum of the cutoff-oscillation pairings

The second cutoff-mean row of p.response.transfer pairs the within-cell oscillations of the cutoff with the gradient and the flux, and then sums the descendants with weights 3^{3(k-s)/2}. At each descendant depth a finite family of cells carries a weight of size at most a fixed multiple of 3^{-n} and a pairing controlled pathwise by the source-load head G times the square root of twice the scalar deficit D. The depth-n row bounds the expectation of the weighted flat average, and summing over the depths after splitting 3^{-n} into a geometric factor and a load factor turns the descendant sum into the printed factor 3^{-H}(E[J_t]𝓛_s)^{1/2}.

The first declaration is the depth row with the normalisation of the weight made explicit; the second sums those rows over the depths.

theorem HCPolySupport.HighContrast.Multiscale.abs_integral_flat_weighted_pairing_le_of_bound {iota : Type u_1} {alpha : Type u_2} [MeasurableSpace alpha] (P : MeasureTheory.Measure alpha) (Z : Finset iota) (c : iota → ℝ) (M : ℝ) (hM : 0 ≤ M) (hc : ∀ w ∈ Z, |c w| ≤ M) (pairing G D : iota → alpha → ℝ) (Lhead tau : ℝ) (hG : ∀ w ∈ Z, ∀ (a : alpha), 0 ≤ G w a) (hD : ∀ w ∈ Z, ∀ (a : alpha), 0 ≤ D w a) (hbd : ∀ w ∈ Z, ∀ (a : alpha), |pairing w a| ≤ G w a * √(2 * D w a)) (hGsq : ∫ (a : alpha), (↑Z.card)⁻¹ * ∑ w ∈ Z, G w a ^ 2 ∂P ≤ Lhead) (hDval : ∫ (a : alpha), (↑Z.card)⁻¹ * ∑ w ∈ Z, 2 * D w a ∂P = 2 * tau) (hFint : MeasureTheory.Integrable (fun (a : alpha) => (↑Z.card)⁻¹ * ∑ w ∈ Z, G w a ^ 2) P) (hDint : MeasureTheory.Integrable (fun (a : alpha) => (↑Z.card)⁻¹ * ∑ w ∈ Z, 2 * D w a) P) (hMidint : MeasureTheory.Integrable (fun (a : alpha) => √((↑Z.card)⁻¹ * ∑ w ∈ Z, G w a ^ 2) * √((↑Z.card)⁻¹ * ∑ w ∈ Z, 2 * D w a)) P) (hPint : MeasureTheory.Integrable (fun (a : alpha) => (↑Z.card)⁻¹ * ∑ w ∈ Z, c w * (√(G w a ^ 2) * √(2 * D w a))) P) (hPint' : MeasureTheory.Integrable (fun (a : alpha) => (↑Z.card)⁻¹ * ∑ w ∈ Z, c w * pairing w a) P) : |∫ (a : alpha), (↑Z.card)⁻¹ * ∑ w ∈ Z, c w * pairing w a ∂P| ≤ M * (√Lhead * √(2 * tau))

The cell pairing row against a weight bounded by M. The weighted flat average of a full-dual pairing controlled pathwise by the source-load head G and the scalar deficit D, against weights of size at most M, has sample expectation at most M · √Lhead · √(2 tau). This is the cell pairing row of p.response.transfer with the normalisation of the weight made explicit.

theorem HCPolySupport.HighContrast.Multiscale.abs_sum_range_descendant_pairing_le {iota : Type u_1} {alpha : Type u_2} [MeasurableSpace alpha] (P : MeasureTheory.Measure alpha) (Nn : ℕ) (Z : ℕ → Finset iota) (θ : ℕ → iota → ℝ) (pairing G D : ℕ → iota → alpha → ℝ) (L : ℕ → ℝ) (K EJ : ℝ) (hK : 0 ≤ K) (hEJ : 0 ≤ EJ) (hL : ∀ (n : ℕ), 0 ≤ L n) (hθ : ∀ (n : ℕ), ∀ w ∈ Z n, |θ n w| ≤ K * 3 ^ (-↑n)) (hG : ∀ (n : ℕ), ∀ w ∈ Z n, ∀ (a : alpha), 0 ≤ G n w a) (hD : ∀ (n : ℕ), ∀ w ∈ Z n, ∀ (a : alpha), 0 ≤ D n w a) (hbd : ∀ (n : ℕ), ∀ w ∈ Z n, ∀ (a : alpha), |pairing n w a| ≤ G n w a * √(2 * D n w a)) (hGsq : ∀ (n : ℕ), ∫ (a : alpha), (↑(Z n).card)⁻¹ * ∑ w ∈ Z n, G n w a ^ 2 ∂P ≤ L n) (hDval : ∀ (n : ℕ), ∫ (a : alpha), (↑(Z n).card)⁻¹ * ∑ w ∈ Z n, 2 * D n w a ∂P ≤ 2 * EJ) (hFint : ∀ (n : ℕ), MeasureTheory.Integrable (fun (a : alpha) => (↑(Z n).card)⁻¹ * ∑ w ∈ Z n, G n w a ^ 2) P) (hDint : ∀ (n : ℕ), MeasureTheory.Integrable (fun (a : alpha) => (↑(Z n).card)⁻¹ * ∑ w ∈ Z n, 2 * D n w a) P) (hMidint : ∀ (n : ℕ), MeasureTheory.Integrable (fun (a : alpha) => √((↑(Z n).card)⁻¹ * ∑ w ∈ Z n, G n w a ^ 2) * √((↑(Z n).card)⁻¹ * ∑ w ∈ Z n, 2 * D n w a)) P) (hPint : ∀ (n : ℕ), MeasureTheory.Integrable (fun (a : alpha) => (↑(Z n).card)⁻¹ * ∑ w ∈ Z n, θ n w * (√(G n w a ^ 2) * √(2 * D n w a))) P) (hPint' : ∀ (n : ℕ), MeasureTheory.Integrable (fun (a : alpha) => (↑(Z n).card)⁻¹ * ∑ w ∈ Z n, θ n w * pairing n w a) P) (hsum : Summable fun (n : ℕ) => 3 ^ (-(3 / 2) * ↑n) * L n) (hsum' : Summable fun (n : ℕ) => 3 ^ (-↑n) * √(L n)) : |∑ n ∈ Finset.range Nn, ∫ (a : alpha), (↑(Z n).card)⁻¹ * ∑ w ∈ Z n, θ n w * pairing n w a ∂P| ≤ K * (√(∑' (n : ℕ), 3 ^ (-(↑n / 2))) * √(∑' (n : ℕ), 3 ^ (-(3 / 2) * ↑n) * L n)) * √(2 * EJ)

The descendant sum of the cutoff-oscillation pairings. At each depth n the weights θ n w are of size at most K · 3^{-n}, the pairings are controlled pathwise by the head G n w a and the deficit D n w a, the annealed flat average of G² is at most L n and the annealed flat average of 2 D is at most 2 EJ. Then every partial descendant sum is bounded by K · √(∑ 3^{-n/2}) · √(∑ 3^{-3n/2} L n) · √(2 EJ): this is the term 3^{-H}(E[J_t]𝓛_s)^{1/2} of p.response.transfer.