Documentation

LeanPool.HighContrastHomogenization.Provider.Quenched.FullBlockHarmonicMean

High-contrast homogenization: Provider.Quenched.FullBlockHarmonicMean #

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

Arithmetic and harmonic means of doubled block matrices #

This module records the finite matrix identity that compares the arithmetic and harmonic means of positive definite doubled block matrices. The comparison keeps an arbitrary deterministic centre, as required by the quadratic fluctuation estimate in the small-contrast argument.

source
noncomputable def HCPolySupport.HighContrast.Quenched.fullBlockArithmeticMean {N d : ℕ} (b : Fin N → FullBlockMat d) :
FullBlockMat d

The arithmetic mean of a nonempty finite family of doubled block matrices.

Equations
Instances For
    source
    noncomputable def HCPolySupport.HighContrast.Quenched.fullBlockHarmonicMean {N d : ℕ} (b : Fin N → FullBlockMat d) :
    FullBlockMat d

    The harmonic mean of a nonempty finite family of doubled block matrices.

    Equations
    Instances For
      source
      theorem HCPolySupport.HighContrast.Quenched.fullBlockHarmonicMean_posDef {N d : ℕ} [NeZero N] {b : Fin N → FullBlockMat d} (hb : ∀ (i : Fin N), Matrix.PosDef (b i)) :
      Matrix.PosDef (fullBlockHarmonicMean b)

      The harmonic mean of positive definite doubled block matrices is positive definite.

      source
      theorem HCPolySupport.HighContrast.Quenched.fullBlockArithmeticMean_eq_harmonicMean_add_averageQuadratic_sub {N d : ℕ} [NeZero N] (b : Fin N → FullBlockMat d) (G : FullBlockMat d) (hb : ∀ (i : Fin N), Matrix.PosDef (b i)) :
      fullBlockArithmeticMean b = fullBlockHarmonicMean b + (↑N)⁻¹ • ∑ i : Fin N, (b i - G) * (b i)⁻¹ * (b i - G) - (fullBlockHarmonicMean b - G) * (fullBlockHarmonicMean b)⁻¹ * (fullBlockHarmonicMean b - G)

      Exact arithmetic-harmonic mean identity with an arbitrary symmetric comparison matrix.

      source
      theorem HCPolySupport.HighContrast.Quenched.fullBlockArithmeticMean_sub_harmonicMean_le_averageQuadratic {N d : ℕ} [NeZero N] (b : Fin N → FullBlockMat d) (G : FullBlockMat d) (hb : ∀ (i : Fin N), Matrix.PosDef (b i)) (hG : Matrix.IsSymm G) :
      fullBlockArithmeticMean b - fullBlockHarmonicMean b ≤ (↑N)⁻¹ • ∑ i : Fin N, (b i - G) * (b i)⁻¹ * (b i - G)

      The arithmetic-harmonic gap is bounded by the average quadratic fluctuation.