High-contrast homogenization: Provider.Recurrence.Scalarization

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

Scalarization of the mixed norm

l.fixed.geometry.matrix.averaging proves a matrix estimate by proving 4d² scalar ones, and the passage between the two runs through the two displays recorded here.

Downwards, the mixed norm of a random symmetric doubled block is controlled by the L^Q norms of its entries, ‖H‖_{L^Q(S_Q)} ≤ (Σ_{a,b}‖H_{ab}‖_{L^Q}²)^{1/2}. The proof is the printed one: the Hilbert–Schmidt comparison |H|_{S_Q} ≤ (Σ_{a,b}H_{ab}²)^{1/2} pointwise, then Minkowski's inequality in L^{Q/2} for the sum of the 4d² squares — the exponent Q/2 is at least 1 exactly because Q ≥ 2.

Upwards, each entry is controlled by the mixed norm, ‖H_{ab}‖_{L^Q} ≤ ‖H‖_{L^Q(S_Q)}, which is the entrywise spectral bound integrated. The two together are what let the scalar independent-sum estimate be applied entry by entry and reassembled.

The normalized form is the one the fixed-grid moments are written in: the centered moment v_r^q is a mixed norm of a normalized block, and the normalization of a symmetric block is symmetric with no hypothesis.

The entry is dominated by the mixed norm

theorem HCPolySupport.HighContrast.Recurrence.lqNorm_le_eLpNorm_schattenNorm {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) {Q : ℝ} (hQ : 0 < Q) {H : CoeffSpace d → BlockMat d} (hH : ∀ (a : CoeffSpace d), IsSymmetricBlockMat (H a)) (α β : BlockCoord d) (hmeas : MeasureTheory.AEStronglyMeasurable (fun (a : CoeffSpace d) => toFullBlockMat (H a) α β) P) : (lqNorm P Q fun (a : CoeffSpace d) => toFullBlockMat (H a) α β) ≤ MeasureTheory.eLpNorm (fun (a : CoeffSpace d) => schattenNorm Q (H a)) (ENNReal.ofReal Q) P

‖H_{ab}‖_{L^Q} ≤ ‖H‖_{L^Q(S_Q)}. The entrywise spectral bound of a symmetric matrix holds pointwise, so it holds after taking L^Q norms.

The mixed norm is dominated by the entries

theorem HCPolySupport.HighContrast.Recurrence.eLpNorm_schattenNorm_le {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) {Q : ℝ} (hQ : 2 ≤ Q) {H : CoeffSpace d → BlockMat d} (hH : ∀ (a : CoeffSpace d), IsSymmetricBlockMat (H a)) (hmeas : ∀ (α β : BlockCoord d), MeasureTheory.AEStronglyMeasurable (fun (a : CoeffSpace d) => toFullBlockMat (H a) α β) P) : MeasureTheory.eLpNorm (fun (a : CoeffSpace d) => schattenNorm Q (H a)) (ENNReal.ofReal Q) P ≤ (∑ α : BlockCoord d, ∑ β : BlockCoord d, (lqNorm P Q fun (a : CoeffSpace d) => toFullBlockMat (H a) α β) ^ 2) ^ 2⁻¹

The scalarization display of l.fixed.geometry.matrix.averaging, ‖H‖_{L^Q(S_Q)} ≤ (Σ_{a,b}‖H_{ab}‖_{L^Q}²)^{1/2}, for a random symmetric doubled block with measurable entries. The Hilbert–Schmidt comparison is applied pointwise and Minkowski's inequality is applied in L^{Q/2} to the 4d² squared entries.

The normalized form

theorem HCPolySupport.HighContrast.Recurrence.lqSchattenSize_le {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) {Q : ℝ} (hQ : 2 ≤ Q) {A : CoeffSpace d → BlockMat d} (F : BlockMat d) (hA : ∀ (a : CoeffSpace d), IsSymmetricBlockMat (A a)) (hmeas : ∀ (α β : BlockCoord d), MeasureTheory.AEStronglyMeasurable (fun (a : CoeffSpace d) => toFullBlockMat (normalizedBlock (A a) F) α β) P) : lqSchattenSize P Q A F ≤ (∑ α : BlockCoord d, ∑ β : BlockCoord d, (lqNorm P Q fun (a : CoeffSpace d) => toFullBlockMat (normalizedBlock (A a) F) α β) ^ 2) ^ 2⁻¹

The scalarization display in the normalized carrier of the fixed-grid estimates. The mixed norm ‖F^{-1/2}·F^{-1/2}‖_{L^Q(S_Q)} of a random symmetric block is bounded by the L^Q norms of the entries of the normalized block; the normalization of a symmetric block is symmetric whatever the normalizing block, so no extra symmetry is assumed of it.