High-contrast homogenization: Provider.Recurrence.DetTransport

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

Determinant transport for the fixed-grid recurrence

The proof of p.fixed.geometry.parent.child.recurrence compares two consecutive adapted scales through the relative mean P = E_p^{-1/2} E_j E_p^{-1/2}. Once the mean order E_p ≤ E_j is available, everything the recurrence asks of P is a statement about a positive definite matrix above the identity, and that is what is proved here.

The determinant identities for the parent-child normalization read det P = e^{Δ}, Δ ≥ 0 and |P| ≤ e^{Δ} for the determinant increment Δ = log det E_j - log det E_p. The determinant identity is the change of variables under the congruence; the sign of Δ is monotonicity of the determinant for the Loewner order; and the spectral bound is the observation that the largest eigenvalue of a matrix above the identity is at most the product of all of them.

The recurrence then needs the trace gap b = tr(P - I), and the step b = Σ(λ_i - 1) ≤ Π λ_i - 1 = e^{Δ} - 1 of the fixed-grid proof. Its content is the elementary inequality that for reals at least one the sum of the excesses is at most the excess of the product, proved here by induction on the index set and then read on the eigenvalues.

Finally the fixed-grid proof passes from the child normalization to the parent one by "the exact congruence" E_p^{-1/2}(G - E_j)E_p^{-1/2} = C^t (E_j^{-1/2}(G - E_j)E_j^{-1/2}) C with C = E_j^{1/2} E_p^{-1/2}. That identity holds for an arbitrary matrix in place of G and is pure square-root algebra; it is recorded in that generality.

The sum of excesses and the excess of the product

theorem HCPolySupport.HighContrast.Recurrence.sum_sub_one_le_prod_sub_one {ι : Type u_2} (s : Finset ι) (f : ι → ℝ) (hf : ∀ i ∈ s, 1 ≤ f i) : ∑ i ∈ s, (f i - 1) ≤ ∏ i ∈ s, f i - 1

For reals at least one, the sum of the excesses over one is at most the excess over one of the product. Adjoining a factor multiplies the product by f a and adds f a - 1 to the sum, and the two differ by the nonnegative product (f a - 1)(∏ f - 1).

The trace gap

theorem HCPolySupport.HighContrast.Recurrence.trace_sub_one_le_det_sub_one {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.IsHermitian) (h : 1 ≤ A) : (A - 1).trace ≤ A.det - 1

The trace gap of a matrix above the identity is at most its determinant gap. This is the step b = Σ(λ_i - 1) ≤ Π λ_i - 1 of the fixed-grid recurrence, read on the eigenvalues of the relative mean.

The determinant transport display

theorem HCPolySupport.HighContrast.Recurrence.det_normalize_eq_exp {n : Type u_1} [Fintype n] [DecidableEq n] {Ej Ep : Matrix n n ℝ} (hEj : Ej.PosDef) (hEp : Ep.PosDef) : (matSqrt Ep⁻¹ * Ej * matSqrt Ep⁻¹).det = Real.exp (Real.log Ej.det - Real.log Ep.det)

The determinant increment is the logarithm of the determinant of the relative mean.

theorem HCPolySupport.HighContrast.Recurrence.one_le_normalize {n : Type u_1} [Fintype n] [DecidableEq n] {Ej Ep : Matrix n n ℝ} (hEp : Ep.PosDef) (h : Ep ≤ Ej) : 1 ≤ matSqrt Ep⁻¹ * Ej * matSqrt Ep⁻¹

The relative mean of an ordered pair of positive definite matrices lies above the identity: this is the mean order E_p ≤ E_j conjugated by E_p^{-1/2}.

theorem HCPolySupport.HighContrast.Recurrence.determinant_transport {n : Type u_1} [Fintype n] [DecidableEq n] {Ej Ep : Matrix n n ℝ} (hEj : Ej.PosDef) (hEp : Ep.PosDef) (h : Ep ≤ Ej) : 1 ≤ matSqrt Ep⁻¹ * Ej * matSqrt Ep⁻¹ ∧ 0 ≤ Real.log Ej.det - Real.log Ep.det ∧ (matSqrt Ep⁻¹ * Ej * matSqrt Ep⁻¹).det = Real.exp (Real.log Ej.det - Real.log Ep.det) ∧ ‖matSqrt Ep⁻¹ * Ej * matSqrt Ep⁻¹‖ ≤ Real.exp (Real.log Ej.det - Real.log Ep.det) ∧ (matSqrt Ep⁻¹ * Ej * matSqrt Ep⁻¹ - 1).trace ≤ Real.exp (Real.log Ej.det - Real.log Ep.det) - 1

The determinant identities for the parent-child normalization of the fixed-grid recurrence. For an ordered pair of positive definite means the relative mean P = E_p^{-1/2} E_j E_p^{-1/2} lies above the identity, its determinant is e^{Δ} for the determinant increment Δ = log det E_j - log det E_p, that increment is nonnegative, the spectral size of P is at most e^{Δ}, and the trace gap tr(P - I) is at most e^{Δ} - 1.

The congruence between the two normalizations

theorem HCPolySupport.HighContrast.Recurrence.normalize_congr {n : Type u_1} [Fintype n] [DecidableEq n] {Ej Ep X : Matrix n n ℝ} (hEj : Ej.PosDef) (hEp : Ep.PosDef) : matSqrt Ep⁻¹ * X * matSqrt Ep⁻¹ = (matSqrt Ej * matSqrt Ep⁻¹).transpose * (matSqrt Ej⁻¹ * X * matSqrt Ej⁻¹) * (matSqrt Ej * matSqrt Ep⁻¹)

The exact congruence of the fixed-grid recurrence. Passing from the child normalization by E_j to the parent normalization by E_p is conjugation by C = E_j^{1/2} E_p^{-1/2}; the identity holds for an arbitrary matrix in the centered slot, which is where the averaged child response enters.