High-contrast homogenization: Entry.Annealed.MatrixAveraging

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

Finite-range matrix averaging

l.fixed.geometry.matrix.averaging. Positive homogeneity and finite-sum Minkowski turn the exact independent matrix sum estimate into the class-average bound. The original average is a convex combination of these class averages; Cauchy–Schwarz over the residue palette gives 3^(d/2). Empty classes have weight zero and are handled before any inverse cancellation. The full endpoint derives all moments, centering, and stationarity transport from the standing law, and certifies the positive definite inverse square root of the deterministic normalizer before using its congruence form.

Deterministic positive homogeneity

theorem HCPolySupport.HighContrast.Annealed.absSchattenNorm_smul {d : ℕ} {H : BlockMat d} (hH : Matrix.IsHermitian (toFullBlockMat H)) {N : ℝ} (hN : 1 ≤ N) (c : ℝ) : absSchattenNorm N (ofFullBlockMat (c • toFullBlockMat H)) = |c| * absSchattenNorm N H

Deterministic positive homogeneity. |c • H|_{S_N} = |c| |H|_{S_N} for a symmetric H and real N ≥ 1.

theorem HCPolySupport.HighContrast.Annealed.absSchattenNorm_ofFullBlockMat_zero {d : ℕ} {N : ℝ} (hN : 1 ≤ N) : absSchattenNorm N (ofFullBlockMat 0) = 0

|0|_{S_N} = 0; the c = 0 instance of absSchattenNorm_smul.

Law-level positive homogeneity

theorem HCPolySupport.HighContrast.Annealed.lqSchattenNorm_smul {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {N : ℝ} (hN : 1 ≤ N) {H : CoeffSpace d → BlockMat d} (hH : SchattenMemLp P N H) (c : ℝ) : (lqSchattenNorm P N fun (a : CoeffSpace d) => ofFullBlockMat (c • toFullBlockMat (H a))) = |c| * lqSchattenNorm P N H

Positive homogeneity for the mixed norm (group 5 item 1).

Finite-sum Minkowski

theorem HCPolySupport.HighContrast.Annealed.lqSchattenNorm_finset_sum_le {d : ℕ} {ι : Type u_1} {P : MeasureTheory.Measure (CoeffSpace d)} {N : ℝ} (hN : 1 ≤ N) (t : Finset ι) (H : ι → CoeffSpace d → BlockMat d) (hH : ∀ i ∈ t, SchattenMemLp P N (H i)) : (lqSchattenNorm P N fun (a : CoeffSpace d) => ofFullBlockMat (∑ i ∈ t, toFullBlockMat (H i a))) ≤ ∑ i ∈ t, lqSchattenNorm P N (H i)

Finite-sum Minkowski for the mixed norm (group 5 item 2). Induction on the finset, exactly as Analysis.lqSchattenNorm_sub_le does for two terms. The empty sum gives 0 ≤ 0; no nonemptiness premise is added.

theorem HCPolySupport.HighContrast.Annealed.lqSchattenNorm_class_average_le {d : ℕ} {ι : Type u_1} (P : MeasureTheory.Measure (CoeffSpace d)) (hP : MeasureTheory.IsProbabilityMeasure P) {N : ℕ} (hN : 2 ≤ N) (hNeven : Even N) (C : Finset ι) (hC : C.Nonempty) (Y : ι → CoeffSpace d → BlockMat d) (hmem : ∀ i ∈ C, SchattenMemLp P (↑N) (Y i)) (hcent : ∀ i ∈ C, ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (Y i a) α β ∂P) = ofFullBlockMat 0) (hindep : ProbabilityTheory.iIndepFun (fun (i : ↥C) (a : CoeffSpace d) => toFullBlockMat (Y (↑i) a)) P) (u : ℝ) (hu : 0 ≤ u) (hnorm : ∀ i ∈ C, lqSchattenNorm P (↑N) (Y i) = u) : (lqSchattenNorm P ↑N fun (a : CoeffSpace d) => ofFullBlockMat ((↑C.card)⁻¹ • ∑ i ∈ C, toFullBlockMat (Y i a))) ≤ ↑N / ↑C.card ^ (1 / 2) * u

A nonempty independent class with a common single-cell norm has the printed average bound.

theorem HCPolySupport.HighContrast.Annealed.average_eq_sum_class_averages {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [Fintype κ] [DecidableEq κ] [AddCommGroup M] [Module ℝ M] (Z : Finset ι) (col : ι → κ) (Y : ι → M) : (↑Z.card)⁻¹ • ∑ z ∈ Z, Y z = ∑ c : κ, (↑{z ∈ Z | col z = c}.card / ↑Z.card) • (↑{z ∈ Z | col z = c}.card)⁻¹ • ∑ z ∈ Z with col z = c, Y z

A finite average is the sum of its class averages weighted by relative class size. Empty classes contribute zero; no inverse cancellation is used on them.

theorem HCPolySupport.HighContrast.Annealed.class_average_weights {ι : Type u_1} {κ : Type u_2} [Fintype κ] [DecidableEq κ] (Z : Finset ι) (hZ : Z.Nonempty) (col : ι → κ) : (∀ (c : κ), 0 ≤ ↑{z ∈ Z | col z = c}.card / ↑Z.card) ∧ ∑ c : κ, ↑{z ∈ Z | col z = c}.card / ↑Z.card = 1

The class weights are nonnegative and sum to one when the original set is nonempty.

theorem HCPolySupport.HighContrast.Annealed.memLqSchatten_smul {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {N : ℝ} (hN : 1 ≤ N) {H : CoeffSpace d → BlockMat d} (hH : SchattenMemLp P N H) (c : ℝ) : SchattenMemLp P N fun (a : CoeffSpace d) => ofFullBlockMat (c • toFullBlockMat (H a))

Scalar multiplication preserves finite mixed moments.

theorem HCPolySupport.HighContrast.Annealed.lqSchattenNorm_coloured_average_le {d : ℕ} {ι : Type u_1} {κ : Type u_2} [Fintype κ] [DecidableEq κ] (P : MeasureTheory.Measure (CoeffSpace d)) (hP : MeasureTheory.IsProbabilityMeasure P) {N : ℕ} (hN : 2 ≤ N) (hNeven : Even N) (Z : Finset ι) (hZ : Z.Nonempty) (col : ι → κ) (Y : ι → CoeffSpace d → BlockMat d) (hmem : ∀ i ∈ Z, SchattenMemLp P (↑N) (Y i)) (hcent : ∀ i ∈ Z, ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (Y i a) α β ∂P) = ofFullBlockMat 0) (hindep : ∀ (c : κ), ProbabilityTheory.iIndepFun (fun (i : ↥({z ∈ Z | col z = c})) (a : CoeffSpace d) => toFullBlockMat (Y (↑i) a)) P) (u : ℝ) (hu : 0 ≤ u) (hnorm : ∀ i ∈ Z, lqSchattenNorm P (↑N) (Y i) = u) : (lqSchattenNorm P ↑N fun (a : CoeffSpace d) => ofFullBlockMat ((↑Z.card)⁻¹ • ∑ i ∈ Z, toFullBlockMat (Y i a))) ≤ ↑N * ↑(Fintype.card κ) ^ (1 / 2) / ↑Z.card ^ (1 / 2) * u

Convex recombination of independent class averages gives the square root of the palette size.

theorem HCPolySupport.HighContrast.Annealed.matrix_averaging_roundedGrid (d : ℕ) (hd : 2 ≤ d) (P : MeasureTheory.Measure (CoeffSpace d)) (hP : MeasureTheory.IsProbabilityMeasure P) (γ : ℝ) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ) (hstat : IsStationaryLaw P) (hunit : IsUnitRangeLaw P) (hdag : CoarseEllipticityDagger P γ E Ψ K S) (N : ℕ) (hN : 2 ≤ N) (hNeven : Even N) (jStar : ℕ) (hj : 2 * d ≤ 3 ^ jStar) (m : Mat d) (hm : Matrix.PosDef m) (j : ℤ) (hjgen : ↑jStar ≤ j) (Z : Finset (Vec d)) (hZne : Z.Nonempty) (hZ : ↑Z ⊆ adaptedLatticeAtScale (Geometry.explicitRoundedGrid jStar m) j) (R : BlockMat d) (hRsymm : IsSymmetricBlockMat R) (hRpos : Book.Ch02.BlockPosDef R) : (lqSchattenNorm P ↑N fun (a : CoeffSpace d) => ofFullBlockMat ((↑Z.card)⁻¹ • ∑ z ∈ Z, toFullBlockMat (normalizedBlock (blockSub (coarseBlock (adaptedCellTranslate (Geometry.explicitRoundedGrid jStar m) j z) a) (adaptedMean P (Geometry.explicitRoundedGrid jStar m) j)) R))) ≤ ↑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 ordinary-support endpoint of finite-range matrix averaging, with the printed constant. The inverse square root is certified positive definite before the normalized variables are identified with a Hermitian congruence. All moment receipts come from the standing law.