High-contrast homogenization: Geometry.AnnealedSharpOrder

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

The annealed sharp order

The annealed primal-adjoint order says that the expectation of the random block matrix A(U) dominates its own sharp: E(U)^♯ ≤ E(U). The reference proof has three moves: an algebraic identity, an external pathwise bound, and matrix Jensen.

The primal-adjoint involution F ↦ R F⁻¹ R and the dual block, formed with the swap matrix R of s.scale.selection, make the inverse of the sharp conjugation by the reflection, so the random matrix Z := R A R has Z⁻¹ = A^♯; that is fullBlockSharp_inv below. The pathwise block order, which gives 0 < A^♯ ≤ A along every realization, is one of the properties of the coarse block that s.introduction takes from HC: it is not proved here and appears as the explicit hypothesis hsharp. It is what makes both Z and Z⁻¹ integrable, so that no inverse moment is needed. Matrix Jensen then gives (E Z)⁻¹ ≤ E (Z⁻¹), and the chain

E(U)^♯ = (E Z)⁻¹ ≤ E (Z⁻¹) = E (A^♯) ≤ E (A) = E(U)

closes the lemma, the last step being monotonicity of the average.

theorem HCPolySupport.HighContrast.fullBlockSharp_inv {d : ℕ} {H : FullBlockMat d} (hH : Matrix.PosDef H) : (fullBlockSharp H)⁻¹ = fullBlockRefl d * H * fullBlockRefl d

The dual identity: the inverse of the sharp is conjugation by the reflection.

theorem HCPolySupport.HighContrast.refl_conj_inv {d : ℕ} {H : FullBlockMat d} (hH : Matrix.PosDef H) : (fullBlockRefl d * H * fullBlockRefl d)⁻¹ = fullBlockSharp H

Conjugation by the reflection recovers the sharp, in the direction the averaging argument uses.

theorem HCPolySupport.HighContrast.integrable_refl_conj {d : ℕ} {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {F : α → FullBlockMat d} (hF : MeasureTheory.Integrable F μ) : MeasureTheory.Integrable (fun (a : α) => fullBlockRefl d * F a * fullBlockRefl d) μ

Conjugation by the reflection keeps an integrable function integrable.

theorem HCPolySupport.HighContrast.integral_refl_conj {d : ℕ} {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {F : α → FullBlockMat d} (hF : MeasureTheory.Integrable F μ) : ∫ (a : α), fullBlockRefl d * F a * fullBlockRefl d ∂μ = (fullBlockRefl d * ∫ (a : α), F a ∂μ) * fullBlockRefl d

Conjugation by the reflection commutes with the average, the reflection being a fixed matrix.

theorem HCPolySupport.HighContrast.fullBlockSharp_integral_le_integral {d : ℕ} {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {A : α → FullBlockMat d} (hpos : ∀ (a : α), Matrix.PosDef (A a)) (hsharp : ∀ (a : α), fullBlockSharp (A a) ≤ A a) (hint : MeasureTheory.Integrable A μ) (hintSharp : MeasureTheory.Integrable (fun (a : α) => fullBlockSharp (A a)) μ) (hEpos : Matrix.PosDef (∫ (a : α), A a ∂μ)) : fullBlockSharp (∫ (a : α), A a ∂μ) ≤ ∫ (a : α), A a ∂μ

The annealed primal-adjoint order: the average of a random positive definite block matrix dominates its own sharp. The pathwise block order enters as the hypothesis hsharp; it is one of the properties of the coarse block taken from HC and is not proved here.