High-contrast homogenization: Provider.PolynomialHomogenization.NormalizedRootCoefficient

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

Exact identity normalization of a coefficient sample

The symmetric part of the comparison coefficient is normalized by its exact projective square root. Before the affine pullback, the coefficient is recentered by the comparison skew part and multiplied by the scalar used in that square root. The resulting constant comparison matrix is exactly the identity; no rounded grid enters this identity.

theorem HCPolySupport.HighContrast.isEllipticMatrix_positive_smul {d : ℕ} {lam Lam c : ℝ} {A : Mat d} (hc : 0 < c) (hA : IsEllipticMatrix lam Lam A) : IsEllipticMatrix (c * lam) (c * Lam) (c • A)

noncomputable def HCPolySupport.HighContrast.CoeffSpace.positiveScale {d : ℕ} (c : ℝ) (hc : 0 < c) (a : CoeffSpace d) : CoeffSpace d

Positive scalar multiplication on the qualitative coefficient space.

Equations

• HCPolySupport.HighContrast.CoeffSpace.positiveScale c hc a = ⟨c • ↑a, ⋯⟩

theorem HCPolySupport.HighContrast.CoeffSpace.positiveScale_ae {d : ℕ} (c : ℝ) (hc : 0 < c) (a : CoeffSpace d) : ↑↑(positiveScale c hc a) =ᵐ[MeasureTheory.volume] fun (x : Vec d) => c • ↑↑a x

The positive scalar action has its expected pointwise representative.

theorem HCPolySupport.HighContrast.CoeffSpace.coeffOn_positiveScale_AEScaled {d : ℕ} (c : ℝ) (hc : 0 < c) (a : CoeffSpace d) (U : Book.Ch02.Domain d) : Book.Ch02.CoeffOn.AEScaled c (a.coeffOn U) ((positiveScale c hc a).coeffOn U)

Restriction to a Chapter 2 domain is an a.e. scalar rescaling.

theorem HCPolySupport.HighContrast.normalizedRootScale_pos {d : ℕ} [NeZero d] {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) : 0 < specBound (symmPart abar)⁻¹

The scalar used by the exact normalized root is positive in positive dimension.

theorem HCPolySupport.HighContrast.normalizedRoot_posDef_of_posDef {d : ℕ} [NeZero d] {m : Mat d} (hm : Matrix.PosDef m) : Matrix.PosDef (Selection.normalizedRoot m)

The exact normalized root is positive definite.

theorem HCPolySupport.HighContrast.normalizedRoot_mul_self {d : ℕ} {m : Mat d} (hm : Matrix.PosDef m) : Selection.normalizedRoot m * Selection.normalizedRoot m = specBound m⁻¹ • m

The exact normalized root squares to the scalar-normalized matrix.

theorem HCPolySupport.HighContrast.Selection.norm_normalizedRoot_eq_witnessEccentricity {d : ℕ} {m : Mat d} (hm : Matrix.PosDef m) : ‖normalizedRoot m‖ = witnessEccentricity m

The operator norm of the exact normalized root is its projective eccentricity.

theorem HCPolySupport.HighContrast.Selection.normalizedRoot_inv_norm_le_one {d : ℕ} [NeZero d] {m : Mat d} (hm : Matrix.PosDef m) : ‖(normalizedRoot m)⁻¹‖ ≤ 1

The inverse of the exact normalized root has operator norm at most one.

noncomputable def HCPolySupport.HighContrast.normalizedCenteredCoeff {d : ℕ} [NeZero d] (a : CoeffSpace d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) : CoeffSpace d

The coefficient sample after skew recentering and exact scalar normalization.

Equations

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

theorem HCPolySupport.HighContrast.exists_normalizedReferenceCoeffFamily {d : ℕ} [NeZero d] (a : CoeffSpace d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (t : ℤ) : ∃ (aRef : Book.Ch03.CoeffFamily d), ∀ (Q : TriadicCube d), (aRef.coeffOn Q).toCoeffField = affineCoefficient (Selection.normalizedRoot (symmPart abar)) ⋯ ((normalizedCenteredCoeff a abar hS).coeffOn (Response.adaptedDomain ⋯ t)).toCoeffField

The exactly normalized coefficient produces a compatible reference-cube family for every parent adapted domain.