High-contrast homogenization: Provider.Quenched.FullBlockSharpHarmonic

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

Harmonic means and the sharp involution

Conjugation by the doubled-block reflection turns the inverse of a sharp matrix back into the original matrix. Consequently, the harmonic mean of a finite family of sharp matrices is exactly the sharp of the arithmetic mean of the original family. Combining this identity with order reversal gives the lower comparison used in the quadratic fluctuation estimate.

theorem HCPolySupport.HighContrast.Quenched.fullBlockHarmonicMean_fullBlockSharp {N d : ℕ} [NeZero N] (A : Fin N → FullBlockMat d) (hA : ∀ (i : Fin N), Matrix.PosDef (A i)) : (fullBlockHarmonicMean fun (i : Fin N) => fullBlockSharp (A i)) = fullBlockSharp (fullBlockArithmeticMean A)

The harmonic mean of a finite family of sharp matrices is the sharp of the arithmetic mean of the original matrices.

theorem HCPolySupport.HighContrast.Quenched.fullBlockHarmonicMean_fullBlockSharp_le {N d : ℕ} [NeZero N] {A : Fin N → FullBlockMat d} {P : FullBlockMat d} (hA : ∀ (i : Fin N), Matrix.PosDef (A i)) (hP : Matrix.PosDef P) (hle : P ≤ fullBlockArithmeticMean A) : (fullBlockHarmonicMean fun (i : Fin N) => fullBlockSharp (A i)) ≤ fullBlockSharp P

If a positive definite parent lies below the arithmetic mean of its children, then the harmonic mean of the children’s sharps lies below the sharp of the parent.

theorem HCPolySupport.HighContrast.Quenched.fullBlockArithmeticMean_sharp_sub_parentSharp_le_averageQuadratic {N d : ℕ} [NeZero N] (A : Fin N → FullBlockMat d) (G P : FullBlockMat d) (hA : ∀ (i : Fin N), Matrix.PosDef (A i)) (hG : Matrix.IsSymm G) (hP : Matrix.PosDef P) (hle : P ≤ fullBlockArithmeticMean A) : (fullBlockArithmeticMean fun (i : Fin N) => fullBlockSharp (A i)) - fullBlockSharp P ≤ (↑N)⁻¹ • ∑ i : Fin N, (fullBlockSharp (A i) - G) * (fullBlockSharp (A i))⁻¹ * (fullBlockSharp (A i) - G)

The arithmetic mean of the children’s sharps, minus the parent sharp, is bounded by the average quadratic fluctuation around any symmetric centre.

theorem HCPolySupport.HighContrast.Quenched.fullBlockFinsetAverage_sharp_sub_parentSharp_le_averageQuadratic {ι : Type u_1} {d : ℕ} (Z : Finset ι) (hZ : Z.Nonempty) (A : ι → FullBlockMat d) (G P : FullBlockMat d) (hA : ∀ i ∈ Z, Matrix.PosDef (A i)) (hG : Matrix.IsSymm G) (hP : Matrix.PosDef P) (hle : P ≤ (↑Z.card)⁻¹ • ∑ i ∈ Z, A i) : (↑Z.card)⁻¹ • ∑ i ∈ Z, fullBlockSharp (A i) - fullBlockSharp P ≤ (↑Z.card)⁻¹ • ∑ i ∈ Z, (fullBlockSharp (A i) - G) * (fullBlockSharp (A i))⁻¹ * (fullBlockSharp (A i) - G)

Finset-indexed form of the sharp arithmetic-harmonic gap. This avoids an enumeration choice when the children are supplied by an aligned subdivision.