High-contrast homogenization: Entry.Analysis.MatrixMomentSum

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

The independent centered symmetric matrix sum estimate

l.fixed.geometry.matrix.averaging:

Expanding the power gives tr E[(∑_{i ∈ I} Y_i)^N] = ∑_{i_1,…,i_N ∈ I} tr E[Y_{i_1} ⋯ Y_{i_N}].

• pow_sum_eq_sum_prod_ofFn — the underlying algebraic identity in an arbitrary (in general noncommutative) ring: (∑ i ∈ s, M i)^N = ∑_{f : Fin N → s} (List.ofFn (M ∘ f)).prod. The factors are kept in an ordered List.ofFn … |>.prod; a Finset.prod of matrices is not available and inventing a commutative structure would be a false statement. Commutativity is not used anywhere in the proof, which is a bare induction on N through Fin.consEquiv.
• The same identity after Matrix.trace, in the shape the printed display uses: the trace of the power expands as the sum of the traces of the ordered words. The operator-norm entry bound in SchattenNormIntegrability is public and is used in the product-integrability bridge. The proof uses grouped independence to cancel singleton words, exact trace Hölder from K1, Hölder in probability, and at most N^N singleton-free equality patterns. Taking the even N-th root gives exactly the printed coefficient N, without a dimension loss.

theorem HCPolySupport.HighContrast.Analysis.abs_blockMatEntry_le_absSchattenNorm {d : ℕ} (H : BlockMat d) (hH : Matrix.IsHermitian (toFullBlockMat H)) {N : ℝ} (hN : 1 ≤ N) (α β : BlockCoord d) : |blockMatEntry H α β| ≤ absSchattenNorm N H

Each entry of a Hermitian block is bounded by its Schatten norm, for real index at least one.

The ordered expansion of a power of a finite sum

theorem HCPolySupport.HighContrast.Analysis.pow_sum_eq_sum_prod_ofFn {R : Type u_1} [Ring R] {ι : Type u_2} (s : Finset ι) (M : ι → R) (N : ℕ) : (∑ i ∈ s, M i) ^ N = ∑ f : Fin N → ↥s, (List.ofFn fun (k : Fin N) => M ↑(f k)).prod

The noncommutative multinomial expansion. In any ring, (∑ i ∈ s, M i) ^ N = ∑_{f : Fin N → s} (M (f 0) * M (f 1) * ⋯ * M (f (N-1))), the factors taken in the order of Fin N.

Commutativity is nowhere used: the right-hand side is an ordered List.ofFn … |>.prod, and the induction step splits Fin (N+1) into its head and tail through Fin.consEquiv.

theorem HCPolySupport.HighContrast.Analysis.trace_pow_sum_toFullBlockMat {d : ℕ} {ι : Type u_1} (s : Finset ι) (Y : ι → BlockMat d) (N : ℕ) : Matrix.trace ((∑ i ∈ s, toFullBlockMat (Y i)) ^ N) = ∑ f : Fin N → ↥s, Matrix.trace (List.ofFn fun (k : Fin N) => toFullBlockMat (Y ↑(f k))).prod

The trace expansion for doubled blocks, in the toFullBlockMat picture.

theorem HCPolySupport.HighContrast.Analysis.memLp_list_prod {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [NormedRing E] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {p : ENNReal} (l : List ι) (f : ι → Ω → E) (hf : ∀ i ∈ l, MeasureTheory.MemLp (f i) p μ) : MeasureTheory.MemLp (fun (a : Ω) => (List.map (fun (i : ι) => f i a) l).prod) (↑l.length * p⁻¹)⁻¹ μ

Hölder membership for an ordered product in a normed ring; the exponent is the reciprocal sum.

theorem HCPolySupport.HighContrast.Analysis.memLp_toFullBlockMat {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {N : ℝ} {H : CoeffSpace d → BlockMat d} (hH : SchattenMemLp P N H) (hN : 1 ≤ N) : MeasureTheory.MemLp (fun (a : CoeffSpace d) => toFullBlockMat (H a)) (ENNReal.ofReal N) P

A Schatten moment controls the full matrix operator-norm moment.

theorem HCPolySupport.HighContrast.Analysis.memLp_prod_entry {d : ℕ} {ι : Type u_1} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsFiniteMeasure P] {N : ℝ} (hN : 1 ≤ N) (l : List ι) (Y : ι → CoeffSpace d → BlockMat d) (hY : ∀ i ∈ l, SchattenMemLp P N (Y i)) (α β : BlockCoord d) : MeasureTheory.MemLp (fun (a : CoeffSpace d) => (List.map (fun (i : ι) => toFullBlockMat (Y i a)) l).prod α β) (↑l.length * (ENNReal.ofReal N)⁻¹)⁻¹ P

Each entry of an ordered matrix product has the Hölder exponent for its length.

theorem HCPolySupport.HighContrast.Analysis.integrable_prod_entry {d : ℕ} {ι : Type u_1} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsFiniteMeasure P] {N : ℕ} (hN : 1 ≤ N) (l : List ι) (hlen : l.length ≤ N) (Y : ι → CoeffSpace d → BlockMat d) (hY : ∀ i ∈ l, SchattenMemLp P (↑N) (Y i)) (α β : BlockCoord d) : MeasureTheory.Integrable (fun (a : CoeffSpace d) => (List.map (fun (i : ι) => toFullBlockMat (Y i a)) l).prod α β) P

Products of at most N factors in L^N have integrable entries on a finite measure space.

theorem HCPolySupport.HighContrast.Analysis.measurable_list_prod {Ω : Type u_1} {ι : Type u_2} {M : Type u_3} [MeasurableSpace Ω] [Monoid M] [MeasurableSpace M] [MeasurableMul₂ M] (l : List ι) (f : ι → Ω → M) (hf : ∀ i ∈ l, Measurable (f i)) : Measurable fun (a : Ω) => (List.map (fun (i : ι) => f i a) l).prod

Measurable factors give a measurable ordered product.

theorem HCPolySupport.HighContrast.Analysis.indepFun_list_prod_of_notMem {Ω : Type u_1} {ι : Type u_2} {M : Type u_3} [MeasurableSpace Ω] [Monoid M] [MeasurableSpace M] [MeasurableMul₂ M] {μ : MeasureTheory.Measure Ω} {f : ι → Ω → M} (hindep : ProbabilityTheory.iIndepFun f μ) (hf : ∀ (i : ι), AEMeasurable (f i) μ) (i : ι) (l : List ι) (hi : i ∉ l) : ProbabilityTheory.IndepFun (f i) (fun (a : Ω) => (List.map (fun (j : ι) => f j a) l).prod) μ

A grouped tuple of other indices, and every ordered product of it, is independent of one index.

theorem HCPolySupport.HighContrast.Analysis.integral_trace_mul_prod_eq_zero {d : ℕ} {ι : Type u_1} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsFiniteMeasure P] {N : ℕ} (hN : 1 ≤ N) (Y : ι → CoeffSpace d → BlockMat d) (hY : ∀ (i : ι), SchattenMemLp P (↑N) (Y i)) (hindep : ProbabilityTheory.iIndepFun (fun (i : ι) (a : CoeffSpace d) => toFullBlockMat (Y i a)) P) (i : ι) (l : List ι) (hlen : l.length ≤ N) (hi : i ∉ l) (hcent : ∀ (α β : BlockCoord d), ∫ (a : CoeffSpace d), blockMatEntry (Y i a) α β ∂P = 0) : ∫ (a : CoeffSpace d), (toFullBlockMat (Y i a) * (List.map (fun (j : ι) => toFullBlockMat (Y j a)) l).prod).trace ∂P = 0

Centering annihilates the expected trace after a singleton factor is moved to the front.

theorem HCPolySupport.HighContrast.Analysis.integral_trace_prod_eq_zero_of_count_eq_one {d : ℕ} {ι : Type u_1} [DecidableEq ι] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsFiniteMeasure P] {N : ℕ} (hN : 1 ≤ N) (Y : ι → CoeffSpace d → BlockMat d) (hY : ∀ (i : ι), SchattenMemLp P (↑N) (Y i)) (hindep : ProbabilityTheory.iIndepFun (fun (i : ι) (a : CoeffSpace d) => toFullBlockMat (Y i a)) P) (l : List ι) (hlen : l.length ≤ N) (i : ι) (hi : List.count i l = 1) (hcent : ∀ (α β : BlockCoord d), ∫ (a : CoeffSpace d), blockMatEntry (Y i a) α β ∂P = 0) : ∫ (a : CoeffSpace d), Matrix.trace (List.map (fun (j : ι) => toFullBlockMat (Y j a)) l).prod ∂P = 0

A word with an index occurring exactly once has zero expected trace, by grouped independence and cyclicity.

theorem HCPolySupport.HighContrast.Analysis.count_ofFn_eq_card_fiber {ι : Type u_1} [DecidableEq ι] {N : ℕ} (f : Fin N → ι) (i : ι) : List.count i (List.ofFn f) = {k : Fin N | f k = i}.card

The occurrence count in an ordered finite word equals the cardinality of its equality fiber.

theorem HCPolySupport.HighContrast.Analysis.integral_prod_le_prod_eLpNorm {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {N : ℕ} (hN : 0 < N) (f : Fin N → Ω → ℝ) (hmem : ∀ (k : Fin N), MeasureTheory.MemLp (f k) (ENNReal.ofReal ↑N) μ) (hnn : ∀ (k : Fin N), 0 ≤ᵐ[μ] f k) : ∫ (a : Ω), ∏ k : Fin N, f k a ∂μ ≤ ∏ k : Fin N, (MeasureTheory.eLpNorm (f k) (ENNReal.ofReal ↑N) μ).toReal

Hölder in probability for N nonnegative factors with finite N-th moments.

theorem HCPolySupport.HighContrast.Analysis.sum_prod_eqPattern_le {κ : Type u_1} {β : Type u_2} {ι : Type u_3} [Fintype κ] [Fintype ι] [DecidableEq κ] [DecidableEq β] [DecidableEq ι] (q : κ → β) (hq : Function.Surjective q) (hb : ∀ (b : β), 2 ≤ Fintype.card { k : κ // q k = b }) (u : ι → ℝ) (hu : ∀ (i : ι), 0 ≤ u i) : ∑ f : κ → ι with ∀ (k l : κ), f k = f l ↔ q k = q l, ∏ k : κ, u (f k) ≤ ((∑ i : ι, u i ^ 2) ^ (1 / 2)) ^ Fintype.card κ

A fixed equality partition without singleton blocks contributes at most the N-th power of the quadratic sum.

theorem HCPolySupport.HighContrast.Analysis.exists_equality_pattern {κ : Type u_1} {ι : Type u_2} (f : κ → ι) : ∃ (q : κ → κ), ∀ (k l : κ), q k = q l ↔ f k = f l

Each equality partition admits a representative map on its original index type.

theorem HCPolySupport.HighContrast.Analysis.sum_prod_noSingleton_le {N : ℕ} {ι : Type u_1} [Fintype ι] [DecidableEq ι] (u : ι → ℝ) (hu : ∀ (i : ι), 0 ≤ u i) : ∑ f : Fin N → ι with ∀ (i : ι), {k : Fin N | f k = i}.card ≠ 1, ∏ k : Fin N, u (f k) ≤ ↑N ^ N * ((∑ i : ι, u i ^ 2) ^ (1 / 2)) ^ N

There are at most N^N equality patterns; sum their singleton-free contributions.

theorem HCPolySupport.HighContrast.Analysis.integrable_trace_prod {d N : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsFiniteMeasure P] (hN : 1 ≤ N) (Y : Fin N → CoeffSpace d → BlockMat d) (hY : ∀ (k : Fin N), SchattenMemLp P (↑N) (Y k)) : MeasureTheory.Integrable (fun (a : CoeffSpace d) => Matrix.trace (List.ofFn fun (k : Fin N) => toFullBlockMat (Y k a)).prod) P

The trace of an N-fold ordered product is integrable.

theorem HCPolySupport.HighContrast.Analysis.abs_integral_trace_prod_le_prod_lqSchattenNorm {d N : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsFiniteMeasure P] (hN : 2 ≤ N) (Y : Fin N → CoeffSpace d → BlockMat d) (hY : ∀ (k : Fin N), SchattenMemLp P (↑N) (Y k)) : |∫ (a : CoeffSpace d), Matrix.trace (List.ofFn fun (k : Fin N) => toFullBlockMat (Y k a)).prod ∂P| ≤ ∏ k : Fin N, lqSchattenNorm P (↑N) (Y k)

Trace Hölder followed by Hölder in probability bounds each word.

theorem HCPolySupport.HighContrast.Analysis.lqSchattenNorm_pow_eq_integral_trace {d N : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} (hN : 2 ≤ N) (hNeven : Even N) {H : CoeffSpace d → BlockMat d} (hH : SchattenMemLp P (↑N) H) : lqSchattenNorm P (↑N) H ^ N = ∫ (a : CoeffSpace d), Matrix.trace (toFullBlockMat (H a) ^ N) ∂P

The even mixed moment is the expected trace power; membership rules out junk integrals.

theorem HCPolySupport.HighContrast.Analysis.lqSchattenNorm_finset_sum_le_of_iIndepFun {d : ℕ} {ι : Type u_1} (P : MeasureTheory.Measure (CoeffSpace d)) (hP : MeasureTheory.IsProbabilityMeasure P) {N : ℕ} (hN : 2 ≤ N) (hNeven : Even N) (s : Finset ι) (Y : ι → CoeffSpace d → BlockMat d) (hmem : ∀ i ∈ s, SchattenMemLp P (↑N) (Y i)) (hcent : ∀ i ∈ s, ofFullBlockMat (Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (Y i a) α β ∂P) = ofFullBlockMat 0) (hindep : ProbabilityTheory.iIndepFun (fun (i : ↥s) (a : CoeffSpace d) => toFullBlockMat (Y (↑i) a)) P) : (lqSchattenNorm P ↑N fun (a : CoeffSpace d) => ofFullBlockMat (∑ i ∈ s, toFullBlockMat (Y i a))) ≤ ↑N * (∑ i ∈ s, lqSchattenNorm P (↑N) (Y i) ^ 2) ^ (1 / 2)

The independent centered symmetric matrix sum bound with coefficient exactly N. The proof also covers the empty finset: its word sum is empty since N is positive.