High-contrast homogenization: Provider.PortableHistory.MajorizationSize

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

The scalar size of a centered block, read spectrally

The centered history e.scale.selection.fluctuation.history measures a centered doubled block A_j^q(z) - E_j^q against a positive reference block, so the scalar size that enters it is the two-sided one: the least t ≥ 0 with -tF ≤ H ≤ tF. The identification of that infimum with the spectral norm of the normalized block is the only fact about it the majorization argument needs, and this file proves it.

The one new ingredient is the two-sided companion of norm_le_iff_le_smul_one: a symmetric matrix caught between ∓tI has spectral norm at most t. Its proof is the factorization

t²I - X² = (tI - X)(tI + X) = √(tI+X) (tI - X) √(tI+X),

which is legitimate because the square root of tI + X commutes with tI - X = 2tI - (tI + X); the C⋆ identity ‖X‖² = ‖X*X‖ then reads the norm off the square.

Three consequences follow at once, and they are exactly the three steps the proof of p.fixed.geometry.one.grid.propagation takes with the centered maximum: the size is attained, so a change of the reference block costs the relative size of the two references; the size is dominated by the Schatten size of the same pair, which is how the centered moments v_j^q enter; and the size is a continuous function of the entries of the block, so the centered maximum is a measurable statistic.

The two-sided spectral characterization

theorem HCPolySupport.HighContrast.PortableHistory.norm_le_of_sandwich {n : Type u_1} [Fintype n] [DecidableEq n] {X : Matrix n n ℝ} (hX : X.conjTranspose = X) {t : ℝ} (ht : 0 ≤ t) (hup : X ≤ t • 1) (hlo : -t • 1 ≤ X) : ‖X‖ ≤ t

A symmetric matrix caught between ∓tI has spectral norm at most t. The two-sided companion of norm_le_iff_le_smul_one.

theorem HCPolySupport.HighContrast.PortableHistory.sandwich_of_norm_le {n : Type u_1} [Fintype n] [DecidableEq n] {X : Matrix n n ℝ} (hX : X.conjTranspose = X) {t : ℝ} (h : ‖X‖ ≤ t) : X ≤ t • 1 ∧ -t • 1 ≤ X

A matrix of spectral norm at most t is caught between ∓tI.

The scalar size is the spectral norm of the normalized block

theorem HCPolySupport.HighContrast.PortableHistory.neg_smul_le_iff_normalize {d : ℕ} {H F : BlockMat d} (hF : Matrix.PosDef (toFullBlockMat F)) (t : ℝ) : -t • toFullBlockMat F ≤ toFullBlockMat H ↔ -t • 1 ≤ toFullBlockMat (normalizedBlock H F)

The lower Loewner constraint of a scalar size, read on the normalized block.

theorem HCPolySupport.HighContrast.PortableHistory.blockSize_eq_norm {d : ℕ} {H F : BlockMat d} (hH : IsSymmetricBlockMat H) (hF : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) : blockSize H F = ‖toFullBlockMat (normalizedBlock H F)‖

The scalar size is the spectral norm of the normalized block. On a symmetric numerator and a positive reference the defining set of blockSize is the closed half-line above ‖F^{-1/2}HF^{-1/2}‖.

theorem HCPolySupport.HighContrast.PortableHistory.blockSize_nonneg {d : ℕ} {H F : BlockMat d} (hH : IsSymmetricBlockMat H) (hF : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) : 0 ≤ blockSize H F

The scalar size is nonnegative.

theorem HCPolySupport.HighContrast.PortableHistory.blockSize_sandwich {d : ℕ} {H F : BlockMat d} (hH : IsSymmetricBlockMat H) (hF : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) : toFullBlockMat H ≤ blockSize H F • toFullBlockMat F ∧ -blockSize H F • toFullBlockMat F ≤ toFullBlockMat H

The scalar size realizes its own bound.

theorem HCPolySupport.HighContrast.PortableHistory.blockSize_le_of_sandwich {d : ℕ} {H F : BlockMat d} (hH : IsSymmetricBlockMat H) (hF : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) {t : ℝ} (ht : 0 ≤ t) (hup : toFullBlockMat H ≤ t • toFullBlockMat F) (hlo : -t • toFullBlockMat F ≤ toFullBlockMat H) : blockSize H F ≤ t

A nonnegative two-sided Loewner bound dominates the scalar size.

theorem HCPolySupport.HighContrast.PortableHistory.blockSize_le_mul_blockSize {d : ℕ} {H Fb Ft : BlockMat d} (hH : IsSymmetricBlockMat H) (hFb : IsSymmetricBlockMat Fb) (hFbpd : Book.Ch02.BlockPosDef Fb) (hFt : IsSymmetricBlockMat Ft) (hFtpd : Book.Ch02.BlockPosDef Ft) {lam : ℝ} (hlam : 0 ≤ lam) (hle : toFullBlockMat Fb ≤ lam • toFullBlockMat Ft) : blockSize H Ft ≤ lam * blockSize H Fb

Changing the reference block costs its relative size. This is the step of p.fixed.geometry.one.grid.propagation that replaces the normalization E_b^q of the centered maximum by E_T^q.

theorem HCPolySupport.HighContrast.PortableHistory.blockSize_le_schattenSize {d : ℕ} {H F : BlockMat d} (hH : IsSymmetricBlockMat H) (hF : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) {Q : ℝ} (hQ : 0 < Q) : blockSize H F ≤ schattenSize Q H F

The scalar size is dominated by the Schatten size of the same pair. The centered maximum of e.scale.selection.fluctuation.history is therefore controlled by the centered moments v_j^q.

The scalar size of a centered response is a measurable statistic

theorem HCPolySupport.HighContrast.PortableHistory.aemeasurable_blockSize_coarseBlock_sub {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {U : Set (Vec d)} (hmeas : HasMeasurableCoarseBlock P U) {E F : BlockMat d} (hE : IsSymmetricBlockMat E) (hF : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) : AEMeasurable (fun (a : CoeffSpace d) => blockSize (blockSub (coarseBlock U a) E) F) P

The centered scalar size is measurable. Its value is the spectral norm of a fixed continuous function of the entries of the response, so the measurability of the variational coarse block is all it needs.