High-contrast homogenization: Geometry.IntegralOrder

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

Bochner integrals of matrices, and matrix Jensen

The averaging step of the annealed primal-adjoint order needs three things about the expectation of a random symmetric matrix: that it is computed entrywise, that it respects the Loewner order, and that it obeys the operator Jensen inequality for the inverse.

The order statements are the generic Bochner ones, but they are unavailable off the shelf: the Loewner order on Matrix n n ℝ is a scoped partial order and Mathlib does not record that it is closed. The first section supplies exactly that, from the description of positive semidefiniteness as a symmetry condition together with one nonnegativity condition per test vector — each of them closed, because the matrix entries and the quadratic forms are continuous linear functionals on a finite-dimensional space.

Matrix Jensen is the reference text's argument, unchanged: for positive definite Y the doubled matrix (Y I; I Y⁻¹) is positive semidefinite, its Schur complement in the lower right corner being zero; averaging the doubling of a random X gives (E X, I; I, E (X⁻¹)), and reading the Schur complement of that average in the upper left corner returns (E X)⁻¹ ≤ E (X⁻¹).

The Loewner order is closed

def HCPolySupport.HighContrast.quadForm {n : Type u_1} [Fintype n] (x : n → ℝ) : Matrix n n ℝ →ₗ[ℝ] ℝ

The quadratic form at a fixed vector, read as a linear functional of the matrix.

Equations

• HCPolySupport.HighContrast.quadForm x = { toFun := fun (A : Matrix n n ℝ) => star x ⬝ᵥ A.mulVec x, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def HCPolySupport.HighContrast.quadFormCLM {n : Type u_1} [Fintype n] (x : n → ℝ) : Matrix n n ℝ →L[ℝ] ℝ

The quadratic form at a fixed vector is continuous, the matrices forming a finite-dimensional normed space.

Equations

• HCPolySupport.HighContrast.quadFormCLM x = LinearMap.toContinuousLinearMap (HCPolySupport.HighContrast.quadForm x)

noncomputable def HCPolySupport.HighContrast.entryCLM {n : Type u_1} [Fintype n] (i j : n) : Matrix n n ℝ →L[ℝ] ℝ

A single matrix entry, as a continuous linear functional.

Equations

• HCPolySupport.HighContrast.entryCLM i j = LinearMap.toContinuousLinearMap (Matrix.entryLinearMap ℝ ℝ i j)

theorem HCPolySupport.HighContrast.isClosed_setOf_nonneg {n : Type u_1} [Finite n] : IsClosed {A : Matrix n n ℝ | 0 ≤ A}

The positive semidefinite cone is closed. Symmetry is an intersection of equalities between entries, and positivity is an intersection of inequalities between continuous quadratic forms.

theorem HCPolySupport.HighContrast.instOrderClosedTopology {n : Type u_1} [Finite n] : OrderClosedTopology (Matrix n n ℝ)

The Loewner order is closed. Scoped rather than global: the order itself is only available after open scoped MatrixOrder, and a consumer outside this namespace can enable the instance with attribute [local instance].

Integrals of matrix-valued functions

Bridging the coordinatewise and operator-norm topologies

Integrable no longer bundles a norm with its topology, so a bare Matrix n n ℝ-valued Integrable hypothesis is read against the coordinatewise (finite-product) topology that is always active on Matrix n n ℝ, rather than the operator-norm topology this file opens to build continuous linear maps out of it. The identity between the two presentations is continuous in both directions — matrices over a finite index type being finite-dimensional — and that lets a hypothesis read in one presentation feed a lemma stated in the other.

noncomputable def HCPolySupport.HighContrast.piToMatCLM {n : Type u_1} [Fintype n] : (n → n → ℝ) →L[ℝ] Matrix n n ℝ

The identity, read as a continuous linear map from the coordinatewise (finite-product) presentation of Matrix n n ℝ into the matrix type itself.

Equations

• HCPolySupport.HighContrast.piToMatCLM = LinearMap.toContinuousLinearMap { toFun := fun (M : n → n → ℝ) => M, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def HCPolySupport.HighContrast.matToPiCLM {n : Type u_1} [Fintype n] : Matrix n n ℝ →L[ℝ] n → n → ℝ

The identity, read as a continuous linear map from Matrix n n ℝ into its coordinatewise (finite-product) presentation.

Equations

• HCPolySupport.HighContrast.matToPiCLM = LinearMap.toContinuousLinearMap { toFun := fun (M : Matrix n n ℝ) => M, map_add' := ⋯, map_smul' := ⋯ }

theorem HCPolySupport.HighContrast.entry_integral {n : Type u_1} [Fintype n] [DecidableEq n] {α : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {F : α → Matrix n n ℝ} (hF : MeasureTheory.Integrable F μ) (i j : n) : (∫ (a : α), F a ∂μ) i j = ∫ (a : α), F a i j ∂μ

The Bochner integral of matrices is computed entrywise.

theorem HCPolySupport.HighContrast.integral_posSemidef {n : Type u_1} [Fintype n] [DecidableEq n] {α : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → Matrix n n ℝ} (hf : ∀ᵐ (a : α) ∂μ, (f a).PosSemidef) : (∫ (a : α), f a ∂μ).PosSemidef

The average of an almost everywhere positive semidefinite matrix is positive semidefinite.

theorem HCPolySupport.HighContrast.integral_mono' {n : Type u_1} [Fintype n] [DecidableEq n] {α : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → Matrix n n ℝ} (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) (h : f ≤ᵐ[μ] g) : ∫ (a : α), f a ∂μ ≤ ∫ (a : α), g a ∂μ

Averaging is monotone for the Loewner order.

noncomputable def HCPolySupport.HighContrast.conjCLM {n : Type u_1} [Fintype n] (L R : Matrix n n ℝ) : Matrix n n ℝ →L[ℝ] Matrix n n ℝ

Two-sided multiplication by fixed matrices, as a continuous linear map.

Equations

• HCPolySupport.HighContrast.conjCLM L R = LinearMap.toContinuousLinearMap { toFun := fun (M : Matrix n n ℝ) => L * M * R, map_add' := ⋯, map_smul' := ⋯ }

theorem HCPolySupport.HighContrast.integrable_mul_left_mul_right {n : Type u_1} [Fintype n] {α : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (L R : Matrix n n ℝ) {F : α → Matrix n n ℝ} (hF : MeasureTheory.Integrable F μ) : MeasureTheory.Integrable (fun (a : α) => L * F a * R) μ

Multiplying an integrable function by fixed matrices keeps it integrable.

theorem HCPolySupport.HighContrast.integral_mul_left_mul_right {n : Type u_1} [Fintype n] [DecidableEq n] {α : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (L R : Matrix n n ℝ) {F : α → Matrix n n ℝ} (hF : MeasureTheory.Integrable F μ) : ∫ (a : α), L * F a * R ∂μ = (L * ∫ (a : α), F a ∂μ) * R

Fixed two-sided factors pass through the integral.

Doubled matrices

theorem HCPolySupport.HighContrast.integrable_fromBlocks {n : Type u_1} [Fintype n] {α : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {A B C D : α → Matrix n n ℝ} (hA : MeasureTheory.Integrable A μ) (hB : MeasureTheory.Integrable B μ) (hC : MeasureTheory.Integrable C μ) (hD : MeasureTheory.Integrable D μ) : MeasureTheory.Integrable (fun (a : α) => Matrix.fromBlocks (A a) (B a) (C a) (D a)) μ

A doubled matrix with integrable blocks is integrable, read entrywise rather than through a Matrix-valued continuous linear map.

theorem HCPolySupport.HighContrast.integral_fromBlocks {n : Type u_1} [Fintype n] [DecidableEq n] {α : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {A B C D : α → Matrix n n ℝ} (hA : MeasureTheory.Integrable A μ) (hB : MeasureTheory.Integrable B μ) (hC : MeasureTheory.Integrable C μ) (hD : MeasureTheory.Integrable D μ) : ∫ (a : α), Matrix.fromBlocks (A a) (B a) (C a) (D a) ∂μ = Matrix.fromBlocks (∫ (a : α), A a ∂μ) (∫ (a : α), B a ∂μ) (∫ (a : α), C a ∂μ) (∫ (a : α), D a ∂μ)

Doubling commutes with the integral, the integral being entrywise.

theorem HCPolySupport.HighContrast.posSemidef_fromBlocks_inv {n : Type u_1} [Fintype n] [DecidableEq n] {Y : Matrix n n ℝ} (hY : Y.PosDef) : (Matrix.fromBlocks Y 1 1 Y⁻¹).PosSemidef

The trivial Schur complement: for a positive definite Y the doubled matrix (Y I; I Y⁻¹) is positive semidefinite.

theorem HCPolySupport.HighContrast.inv_integral_le_integral_inv {n : Type u_1} [Fintype n] [DecidableEq n] {α : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {X : α → Matrix n n ℝ} (hX : ∀ (a : α), (X a).PosDef) (hXint : MeasureTheory.Integrable X μ) (hXinv : MeasureTheory.Integrable (fun (a : α) => (X a)⁻¹) μ) (hpos : (∫ (a : α), X a ∂μ).PosDef) : (∫ (a : α), X a ∂μ)⁻¹ ≤ ∫ (a : α), (X a)⁻¹ ∂μ

Matrix Jensen, the averaging step of the annealed primal-adjoint order: the inverse of the average of a positive definite random matrix is below the average of its inverse.