High-contrast homogenization: Provider.Response.ProfileRowOscillationSum

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

The scale sum of the cutoff-oscillation row

The cutoff-oscillation contribution to a cutoff-defect mean row is a sum over scales of a normalized cell average of a product: a cell energy root against a cell Schur load. Cauchy-Schwarz in the cell index and then in the scale index, with the geometric weight split between the two factors, converts that sum into the energy root times the root of the all-earlier Schur row.

The scale weights are split as 3^{k-s} = 3^{(k-s)/4}·3^{3(k-s)/4}, so the energy side collects a convergent geometric factor and the load side collects exactly the row weight 3^{3(k-s)/2}.

Cauchy-Schwarz for the normalized cell average

theorem HCPolySupport.HighContrast.Response.avsum_mul_le_sqrt_mul_sqrt {ι : Type u_1} (Z : Finset ι) (f g : ι → ℝ) : (avsum Z fun (z : ι) => f z * g z) ≤ √(avsum Z fun (z : ι) => f z ^ 2) * √(avsum Z fun (z : ι) => g z ^ 2)

The normalized cell average of a product is at most the product of the normalized quadratic means.

The geometric scale factor

theorem HCPolySupport.HighContrast.Response.sum_geom_half_Icc_le (Klo s : ℤ) : ∑ k ∈ Finset.Icc Klo s, 3 ^ (1 / 2 * (↑k - ↑s)) ≤ 1 / (1 - 3 ^ (-(1 / 2)))

The half-power scale weights of an all-earlier row sum to a convergent geometric total.

The weighted scale sum

theorem HCPolySupport.HighContrast.Response.sum_scaleWeighted_mul_le {Klo s : ℤ} {A B : ℤ → ℝ} {SE : ℝ} (hSE : 0 ≤ SE) (hB : ∀ k ∈ Finset.Icc Klo s, 0 ≤ B k) (hAE : ∀ k ∈ Finset.Icc Klo s, A k ≤ SE) : ∑ k ∈ Finset.Icc Klo s, 3 ^ (↑k - ↑s) * (A k * B k) ≤ √(1 / (1 - 3 ^ (-(1 / 2)))) * SE * √(∑ k ∈ Finset.Icc Klo s, profileRowWeight k s * B k ^ 2)

The weighted scale sum. A geometrically weighted sum of products, with the first factor uniformly bounded, is controlled by that bound times the root of the row-weighted sum of the second factor's squares.

The flux half of the row

theorem HCPolySupport.HighContrast.Response.profileRowWeight_pos (k s : ℤ) : 0 < profileRowWeight k s

theorem HCPolySupport.HighContrast.Response.sq_profileSchurLoadFlux_le_profileSchurLoad {d : ℕ} (H : BlockMat d) (Pcen Qcen : Vec d) : profileSchurLoadFlux H Qcen ^ 2 ≤ profileSchurLoad H Pcen Qcen

The square of the flux half of the Schur load is at most the load.

theorem HCPolySupport.HighContrast.Response.profilePrimalHattedRowPartial_nonneg {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (q h : Mat d) (Klo s : ℤ) (Pcen Qcen : Vec d) : 0 ≤ profilePrimalHattedRowPartial P q h Klo s Pcen Qcen

The row bound in the mixed carrier

The generic closing form

theorem HCPolySupport.HighContrast.Response.sq_profileSchurLoadGradient_le_profileSchurLoad {d : ℕ} (H : BlockMat d) (Pcen Qcen : Vec d) : profileSchurLoadGradient H Pcen ^ 2 ≤ profileSchurLoad H Pcen Qcen

The square of the gradient half of the Schur load is at most the load.

theorem HCPolySupport.HighContrast.Response.sum_rowWeight_avsum_sq_le {d : ℕ} (q : Mat d) (Klo s : ℤ) (Pcen Qcen : Vec d) (blk : ℤ → (Fin d → ℤ) → BlockMat d) (load : ℤ → (Fin d → ℤ) → ℝ) (hsq : ∀ (k : ℤ) (w : Fin d → ℤ), load k w ^ 2 ≤ profileSchurLoad (blk k w) Pcen Qcen) : (∑ k ∈ Finset.Icc Klo s, profileRowWeight k s * avsum (alignedIndex q k s) fun (w : Fin d → ℤ) => load k w ^ 2) ≤ ∑ k ∈ Finset.Icc Klo s, profileRowWeight k s * avsum (alignedIndex q k s) fun (w : Fin d → ℤ) => profileSchurLoad (blk k w) Pcen Qcen

A row-weighted sum of squared cell loads is dominated by the corresponding row-weighted sum of Schur loads.

theorem HCPolySupport.HighContrast.Response.sum_rowWeight_avsum_profileSchurLoad_nonneg {d : ℕ} (q : Mat d) (Klo s : ℤ) (Pcen Qcen : Vec d) (blk : ℤ → (Fin d → ℤ) → BlockMat d) : 0 ≤ ∑ k ∈ Finset.Icc Klo s, profileRowWeight k s * avsum (alignedIndex q k s) fun (w : Fin d → ℤ) => profileSchurLoad (blk k w) Pcen Qcen

A row-weighted sum of Schur loads is nonnegative.

theorem HCPolySupport.HighContrast.Response.profileAdjointHattedRowPartial_nonneg {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (q h : Mat d) (Klo s : ℤ) (Pcen Qcen : Vec d) : 0 ≤ profileAdjointHattedRowPartial P q h Klo s Pcen Qcen

theorem HCPolySupport.HighContrast.Response.ofReal_abs_le_mul_row_rpow {row : ENNReal} {rowPartial T G : ℝ} (hG : 0 ≤ G) (hrowPartial : 0 ≤ rowPartial) (hrowLe : ENNReal.ofReal rowPartial ≤ row) (hT : |T| ≤ G * √rowPartial) : ENNReal.ofReal |T| ≤ ENNReal.ofReal G * row ^ (1 / 2)

A quantity dominated by a constant times the root of a lower-cutoff row is dominated, in the mixed carrier, by that constant against the root of any majorant of the row.

theorem HCPolySupport.HighContrast.Response.ofReal_abs_scaleSum_le_mul_row_rpow {d : ℕ} (q : Mat d) (Klo s : ℤ) (energy load : ℤ → (Fin d → ℤ) → ℝ) {row : ENNReal} {rowPartial SE Cd T : ℝ} (hSE : 0 ≤ SE) (hCd : 0 ≤ Cd) (hrowPartial : 0 ≤ rowPartial) (hrowSum : (∑ k ∈ Finset.Icc Klo s, profileRowWeight k s * avsum (alignedIndex q k s) fun (w : Fin d → ℤ) => load k w ^ 2) ≤ rowPartial) (hrowLe : ENNReal.ofReal rowPartial ≤ row) (hbound : ∀ k ∈ Finset.Icc Klo s, √(avsum (alignedIndex q k s) fun (w : Fin d → ℤ) => energy k w ^ 2) ≤ SE) (hT : |T| ≤ Cd * ∑ k ∈ Finset.Icc Klo s, 3 ^ (↑k - ↑s) * avsum (alignedIndex q k s) fun (w : Fin d → ℤ) => energy k w * load k w) : ENNReal.ofReal |T| ≤ ENNReal.ofReal (Cd * √(1 / (1 - 3 ^ (-(1 / 2)))) * SE) * row ^ (1 / 2)

The cutoff-oscillation contribution to a cutoff-defect mean row. The scale sum of cell products, with the cell energy roots uniformly bounded by the parent energy root, is dominated by the geometric constant times that energy root times the root of the row.

The four row instances

theorem HCPolySupport.HighContrast.Response.ofReal_abs_scaleSum_flux_le_mul_profilePrimalHattedEarlierRow_rpow {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (q h : Mat d) (Klo s : ℤ) (Pcen Qcen : Vec d) (energy : ℤ → (Fin d → ℤ) → ℝ) {SE Cd T : ℝ} (hSE : 0 ≤ SE) (hCd : 0 ≤ Cd) (hbound : ∀ k ∈ Finset.Icc Klo s, √(avsum (alignedIndex q k s) fun (w : Fin d → ℤ) => energy k w ^ 2) ≤ SE) (hT : |T| ≤ Cd * ∑ k ∈ Finset.Icc Klo s, 3 ^ (↑k - ↑s) * avsum (alignedIndex q k s) fun (w : Fin d → ℤ) => energy k w * profileSchurLoadFlux (profileHattedBlock h (annealedBlock P (adaptedCellAt q k w))) Qcen) : ENNReal.ofReal |T| ≤ ENNReal.ofReal (Cd * √(1 / (1 - 3 ^ (-(1 / 2)))) * SE) * profilePrimalHattedEarlierRow P q h s Pcen Qcen ^ (1 / 2)

The primal flux-half instance: the second term of the gradient-mean row estimate.

theorem HCPolySupport.HighContrast.Response.ofReal_abs_scaleSum_gradient_le_mul_profilePrimalHattedEarlierRow_rpow {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (q h : Mat d) (Klo s : ℤ) (Pcen Qcen : Vec d) (energy : ℤ → (Fin d → ℤ) → ℝ) {SE Cd T : ℝ} (hSE : 0 ≤ SE) (hCd : 0 ≤ Cd) (hbound : ∀ k ∈ Finset.Icc Klo s, √(avsum (alignedIndex q k s) fun (w : Fin d → ℤ) => energy k w ^ 2) ≤ SE) (hT : |T| ≤ Cd * ∑ k ∈ Finset.Icc Klo s, 3 ^ (↑k - ↑s) * avsum (alignedIndex q k s) fun (w : Fin d → ℤ) => energy k w * profileSchurLoadGradient (profileHattedBlock h (annealedBlock P (adaptedCellAt q k w))) Pcen) : ENNReal.ofReal |T| ≤ ENNReal.ofReal (Cd * √(1 / (1 - 3 ^ (-(1 / 2)))) * SE) * profilePrimalHattedEarlierRow P q h s Pcen Qcen ^ (1 / 2)

The primal gradient-half instance: the second term of the flux-mean row estimate.

theorem HCPolySupport.HighContrast.Response.ofReal_abs_scaleSum_flux_le_mul_profileAdjointHattedEarlierRow_rpow {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (q h : Mat d) (Klo s : ℤ) (Pcen Qcen : Vec d) (energy : ℤ → (Fin d → ℤ) → ℝ) {SE Cd T : ℝ} (hSE : 0 ≤ SE) (hCd : 0 ≤ Cd) (hbound : ∀ k ∈ Finset.Icc Klo s, √(avsum (alignedIndex q k s) fun (w : Fin d → ℤ) => energy k w ^ 2) ≤ SE) (hT : |T| ≤ Cd * ∑ k ∈ Finset.Icc Klo s, 3 ^ (↑k - ↑s) * avsum (alignedIndex q k s) fun (w : Fin d → ℤ) => energy k w * profileSchurLoadFlux (profileHattedAdjointBlock h (annealedBlock P (adaptedCellAt q k w))) Qcen) : ENNReal.ofReal |T| ≤ ENNReal.ofReal (Cd * √(1 / (1 - 3 ^ (-(1 / 2)))) * SE) * profileAdjointHattedEarlierRow P q h s Pcen Qcen ^ (1 / 2)

The coefficient-transpose flux-half instance.

theorem HCPolySupport.HighContrast.Response.ofReal_abs_scaleSum_gradient_le_mul_profileAdjointHattedEarlierRow_rpow {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (q h : Mat d) (Klo s : ℤ) (Pcen Qcen : Vec d) (energy : ℤ → (Fin d → ℤ) → ℝ) {SE Cd T : ℝ} (hSE : 0 ≤ SE) (hCd : 0 ≤ Cd) (hbound : ∀ k ∈ Finset.Icc Klo s, √(avsum (alignedIndex q k s) fun (w : Fin d → ℤ) => energy k w ^ 2) ≤ SE) (hT : |T| ≤ Cd * ∑ k ∈ Finset.Icc Klo s, 3 ^ (↑k - ↑s) * avsum (alignedIndex q k s) fun (w : Fin d → ℤ) => energy k w * profileSchurLoadGradient (profileHattedAdjointBlock h (annealedBlock P (adaptedCellAt q k w))) Pcen) : ENNReal.ofReal |T| ≤ ENNReal.ofReal (Cd * √(1 / (1 - 3 ^ (-(1 / 2)))) * SE) * profileAdjointHattedEarlierRow P q h s Pcen Qcen ^ (1 / 2)

The coefficient-transpose gradient-half instance.