High-contrast homogenization: Entry.Multiscale.Initial.GeometricMean

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

Initialization: the matrix geometric mean and the square-root order toolkit

Operator-order support for the two entry-radius kernels of HCPoly/Entry/Multiscale/Initial/CanonicalMetric.lean: monotonicity of the matrix square root, Loewner congruence and inversion, and the matrix geometric mean A #ᵐ B with its Riccati characterization, commutativity, monotonicity in both arguments and homogeneity (p.global.selection).

These are helper facts of the initialization route, kept in the GeometricMean namespace; they carry no probability law and no annealed premise.

Public geometric-mean toolkit

These helpers support the entry-radius kernels in HCPoly/Entry/Multiscale/Initial/CanonicalMetric.lean.

Part 1. The matrix geometric mean

Ported square-root order toolkit.

Small algebraic helpers ported from HCPoly.Geometry.OperatorOrder /

HCPoly.Geometry.SqrtOrder.

theorem HCPolySupport.HighContrast.Multiscale.GeometricMean.conj_le_conj {ι : Type u_2} [Fintype ι] (C : Matrix ι ι ℝ) {A B : Matrix ι ι ℝ} (h : A ≤ B) : C.conjTranspose * A * C ≤ C.conjTranspose * B * C

Congruence is monotone: conjugating both sides of a Loewner inequality by the same matrix preserves it.

theorem HCPolySupport.HighContrast.Multiscale.GeometricMean.isUnit_det_of_posDef {ι : Type u_2} [Fintype ι] [DecidableEq ι] {A : Matrix ι ι ℝ} (hA : A.PosDef) : IsUnit A.det

theorem HCPolySupport.HighContrast.Multiscale.GeometricMean.norm_mul_self_of_symm {ι : Type u_2} [Fintype ι] [DecidableEq ι] {X : Matrix ι ι ℝ} (hX : X.conjTranspose = X) : ‖X * X‖ = ‖X‖ ^ 2

theorem HCPolySupport.HighContrast.Multiscale.GeometricMean.isHermitian_pow {ι : Type u_2} [Fintype ι] [DecidableEq ι] {X : Matrix ι ι ℝ} (hX : X.conjTranspose = X) (m : ℕ) : (X ^ m).conjTranspose = X ^ m

theorem HCPolySupport.HighContrast.Multiscale.GeometricMean.inner_toLp {ι : Type u_2} [Fintype ι] (x y : ι → ℝ) : inner ℝ (WithLp.toLp 2 x) (WithLp.toLp 2 y) = x ⬝ᵥ y

theorem HCPolySupport.HighContrast.Multiscale.GeometricMean.norm_toLp_sq_fintype {ι : Type u_2} [Fintype ι] (x : ι → ℝ) : ‖WithLp.toLp 2 x‖ ^ 2 = x ⬝ᵥ x

theorem HCPolySupport.HighContrast.Multiscale.GeometricMean.toEuclideanCLM_apply_fintype {ι : Type u_2} [Fintype ι] [DecidableEq ι] (A : Matrix ι ι ℝ) (x : ι → ℝ) : (Matrix.toEuclideanCLM A) (WithLp.toLp 2 x) = WithLp.toLp 2 (A.mulVec x)

theorem HCPolySupport.HighContrast.Multiscale.GeometricMean.dotProduct_mulVec_symm {ι : Type u_2} [Fintype ι] {A : Matrix ι ι ℝ} (hA : A.transpose = A) (x y : ι → ℝ) : x ⬝ᵥ A.mulVec y = A.mulVec x ⬝ᵥ y

theorem HCPolySupport.HighContrast.Multiscale.GeometricMean.dotProduct_mulVec_le_norm_mul {ι : Type u_2} [Fintype ι] [DecidableEq ι] (A : Matrix ι ι ℝ) (x : ι → ℝ) : x ⬝ᵥ A.mulVec x ≤ ‖A‖ * x ⬝ᵥ x

theorem HCPolySupport.HighContrast.Multiscale.GeometricMean.norm_le_of_le_smul_one {ι : Type u_2} [Fintype ι] [DecidableEq ι] {A : Matrix ι ι ℝ} (hA : A.PosSemidef) {t : ℝ} (ht : 0 ≤ t) (h : A ≤ t • 1) : ‖A‖ ≤ t

theorem HCPolySupport.HighContrast.Multiscale.GeometricMean.le_smul_one_of_norm_le {ι : Type u_2} [Fintype ι] [DecidableEq ι] {A : Matrix ι ι ℝ} (hA : A.PosSemidef) {t : ℝ} (h : ‖A‖ ≤ t) : A ≤ t • 1

theorem HCPolySupport.HighContrast.Multiscale.GeometricMean.norm_le_one_of_le_one {ι : Type u_2} [Fintype ι] [DecidableEq ι] {X : Matrix ι ι ℝ} (hX : X.PosSemidef) (h : X ≤ 1) : ‖X‖ ≤ 1

theorem HCPolySupport.HighContrast.Multiscale.GeometricMean.posDef_conj_of_posDef {ι : Type u_2} [Fintype ι] {A B : Matrix ι ι ℝ} (hA : A.PosDef) (hB : B.PosDef) : (B * A * B).PosDef

theorem HCPolySupport.HighContrast.Multiscale.GeometricMean.inv_smul_of_posDef {ι : Type u_2} [Fintype ι] [DecidableEq ι] {A : Matrix ι ι ℝ} (hA : A.PosDef) {a : ℝ} (ha : a ≠ 0) : (a • A)⁻¹ = a⁻¹ • A⁻¹

noncomputable def HCPolySupport.HighContrast.Multiscale.GeometricMean.geoMean {ι : Type u_2} [Fintype ι] [DecidableEq ι] (A B : Matrix ι ι ℝ) : Matrix ι ι ℝ

The matrix geometric mean A # B = A^{1/2}(A^{-1/2} B A^{-1/2})^{1/2} A^{1/2}.

Equations

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

theorem HCPolySupport.HighContrast.Multiscale.GeometricMean.geoMeanPosDef {ι : Type u_2} [Fintype ι] [DecidableEq ι] {A B : Matrix ι ι ℝ} (hA : A.PosDef) (hB : B.PosDef) : (geoMean A B).PosDef

theorem HCPolySupport.HighContrast.Multiscale.GeometricMean.sqrtCancel {ι : Type u_2} [Fintype ι] [DecidableEq ι] {A : Matrix ι ι ℝ} (hA : A.PosDef) : matSqrt A * matSqrt A⁻¹ = 1 ∧ matSqrt A⁻¹ * matSqrt A = 1

theorem HCPolySupport.HighContrast.Multiscale.GeometricMean.riccatiOfRoots {ι : Type u_2} [Fintype ι] [DecidableEq ι] {P R S B : Matrix ι ι ℝ} (hPR : P * R = 1) (hRP : R * P = 1) (hSS : S * S = R * B * R) : P * S * P * (R * R) * (P * S * P) = B

theorem HCPolySupport.HighContrast.Multiscale.GeometricMean.geoMean_riccati {ι : Type u_2} [Fintype ι] [DecidableEq ι] {A B : Matrix ι ι ℝ} (hA : A.PosDef) (hB : B.PosDef) : geoMean A B * A⁻¹ * geoMean A B = B

theorem HCPolySupport.HighContrast.Multiscale.GeometricMean.eq_geoMean_of_riccati {ι : Type u_2} [Fintype ι] [DecidableEq ι] {A B X : Matrix ι ι ℝ} (hA : A.PosDef) (hX : X.PosDef) (h : X * A⁻¹ * X = B) : X = geoMean A B

theorem HCPolySupport.HighContrast.Multiscale.GeometricMean.invRiccati {ι : Type u_2} [Fintype ι] [DecidableEq ι] {A B X : Matrix ι ι ℝ} (h : X * A⁻¹ * X = B) : X⁻¹ * A⁻¹⁻¹ * X⁻¹ = B⁻¹

theorem HCPolySupport.HighContrast.Multiscale.GeometricMean.eq_geoMean_comm_of_riccati {ι : Type u_2} [Fintype ι] [DecidableEq ι] {A B X : Matrix ι ι ℝ} (hA : A.PosDef) (hB : B.PosDef) (hX : X.PosDef) (hric : X * A⁻¹ * X = B) : X = geoMean B A

theorem HCPolySupport.HighContrast.Multiscale.GeometricMean.geoMean_comm {ι : Type u_2} [Fintype ι] [DecidableEq ι] {A B : Matrix ι ι ℝ} (hA : A.PosDef) (hB : B.PosDef) : geoMean A B = geoMean B A

theorem HCPolySupport.HighContrast.Multiscale.GeometricMean.geoMean_mono_right {ι : Type u_2} [Fintype ι] [DecidableEq ι] {A B₀ B₁ : Matrix ι ι ℝ} (hA : A.PosDef) (hB₀ : B₀.PosDef) (hB₁ : B₁.PosDef) (h : B₀ ≤ B₁) : geoMean A B₀ ≤ geoMean A B₁

theorem HCPolySupport.HighContrast.Multiscale.GeometricMean.geoMean_mono {ι : Type u_2} [Fintype ι] [DecidableEq ι] {A₀ A₁ B₀ B₁ : Matrix ι ι ℝ} (hA₀ : A₀.PosDef) (hA₁ : A₁.PosDef) (hB₀ : B₀.PosDef) (hB₁ : B₁.PosDef) (hA : A₀ ≤ A₁) (hB : B₀ ≤ B₁) : geoMean A₀ B₀ ≤ geoMean A₁ B₁

theorem HCPolySupport.HighContrast.Multiscale.GeometricMean.geoMean_self {ι : Type u_2} [Fintype ι] [DecidableEq ι] {A : Matrix ι ι ℝ} (hA : A.PosDef) : geoMean A A = A

theorem HCPolySupport.HighContrast.Multiscale.GeometricMean.geoMean_smul {ι : Type u_2} [Fintype ι] [DecidableEq ι] {A B : Matrix ι ι ℝ} (hA : A.PosDef) (hB : B.PosDef) {a b : ℝ} (ha : 0 < a) (hb : 0 < b) : geoMean (a • A) (b • B) = √(a * b) • geoMean A B