High-contrast homogenization: Provider.Quenched.SmallContrastWeakCellVariance

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

The recent cell sums by per-scale variances

The weighted recent cell sum of the weak-norm split is bounded in L²(P) by the per-scale single-cell fluctuation carriers — the same lqSchattenSize-carriers as the aligned-subdivision concentration — plus the deterministic mean drops, with the geometric weights of the sum. This is the first (variance) group of the printed display HC (3.68), with no window multiplier and no history.

noncomputable def HCPolySupport.HighContrast.Quenched.scaleVariance {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (q : Mat d) (F : BlockMat d) (k : ℤ) : ENNReal

The per-scale single-cell fluctuation carrier in normalization F.

Equations

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

theorem HCPolySupport.HighContrast.Quenched.le_of_sq_le_sq {a b : ENNReal} (h : a ^ 2 ≤ b ^ 2) : a ≤ b

Squares compare iff the values compare.

theorem HCPolySupport.HighContrast.Quenched.eLpNorm_two_real_sq {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {f : CoeffSpace d → ℝ} (hf : ∀ (a : CoeffSpace d), 0 ≤ f a) (hfm : MeasureTheory.AEStronglyMeasurable f P) : MeasureTheory.eLpNorm f 2 P ^ 2 = ∫⁻ (a : CoeffSpace d), ENNReal.ofReal (f a ^ 2) ∂P

The square of the two-norm of a nonnegative statistic.

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

Minkowski on the normalized finite average.

theorem HCPolySupport.HighContrast.Quenched.eLpNorm_schattenTwo_adaptedCellAt_eq {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} (hstat : IsStationaryLaw P) {l : ℤ} {q : Mat d} (hq : IsRoundedGrid l q) {j : ℤ} (hlj : l ≤ j) (E F : BlockMat d) (hE : IsSymmetricBlockMat E) (w : Fin d → ℤ) : MeasureTheory.eLpNorm (fun (a : CoeffSpace d) => schattenSize 2 (blockSub (coarseBlock (adaptedCellAt q j w) a) E) F) 2 P = MeasureTheory.eLpNorm (fun (a : CoeffSpace d) => schattenSize 2 (blockSub (coarseBlock (adaptedCell q j) a) E) F) 2 P

Stationarity transport of the centred aligned-cell carrier (clone of the aligned-subdivision transport).

theorem HCPolySupport.HighContrast.Quenched.eLpNorm_diagonalWeakCellDefect_le {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (hstat : IsStationaryLaw P) {l : ℤ} {q : Mat d} (hgrid : IsRoundedGrid l q) {k t : ℤ} (hlk : l ≤ k) {F : BlockMat d} (hFsym : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) : MeasureTheory.eLpNorm (fun (a : CoeffSpace d) => Response.diagonalWeakCellDefect q k t F a) 2 P ≤ scaleVariance P q F k + scaleVariance P q F t + ENNReal.ofReal (blockSize (blockSub (adaptedMean P q k) (adaptedMean P q t)) F)

The per-scale cell defect in L². The recent-cell defect at scale k is bounded by the two single-cell fluctuation carriers plus the deterministic mean drop.

theorem HCPolySupport.HighContrast.Quenched.eLpNorm_diagonalWeakCellSum_le_variance {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (hstat : IsStationaryLaw P) {l : ℤ} {q : Mat d} (hgrid : IsRoundedGrid l q) {t : ℤ} (H : ℕ) (hstart : l ≤ t - ↑H) {F : BlockMat d} (hFsym : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) : MeasureTheory.eLpNorm (fun (a : CoeffSpace d) => Response.diagonalWeakCellSum q t H (1 / 2) F a) 2 P ≤ ∑ j ∈ Finset.range (H + 1), ENNReal.ofReal (3 ^ (-(1 / 2) * ↑j)) * (scaleVariance P q F (t - ↑j) + scaleVariance P q F t + ENNReal.ofReal (blockSize (blockSub (adaptedMean P q (t - ↑j)) (adaptedMean P q t)) F))

The recent cell sum in L². The weighted recent cell sum is bounded by the weighted per-scale variance carriers and mean drops.