Documentation

LeanPool.HighContrastHomogenization.Provider.PolynomialHomogenization.Root.Corrector.C1CoefficientEnergySeminorm

High-contrast homogenization: #

Provider.PolynomialHomogenization.Root.Corrector.C1CoefficientEnergySeminorm

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

The local coefficient-energy seminorm #

The symmetric coefficient operator is positive on every positive-volume domain. Its quadratic form therefore defines a seminorm. This is the Minkowski step needed to telescope finite-corrector increments without introducing the lower ellipticity constant into the quantitative constant.

source
theorem HCPolySupport.HighContrast.hilbertSymmCoeffOperator_isPositive {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < MeasureTheory.volume U) (hvoltop : MeasureTheory.volume U ≠ ⊤) :
(hilbertSymmCoeffOperator hEll).IsPositive

The local symmetric coefficient operator is positive on a domain of positive volume.

source
theorem HCPolySupport.HighContrast.sqrt_inner_apply_add_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : E →L[ℝ] E) (hT : T.IsPositive) (x y : E) :
√(inner ℝ (T (x + y)) (x + y)) ≤ √(inner ℝ (T x) x) + √(inner ℝ (T y) y)

The square root of a positive operator's quadratic form satisfies the triangle inequality.

source
theorem HCPolySupport.HighContrast.sqrt_normalizedLocalSymmetricEnergy_add_le {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < MeasureTheory.volume U) (hvoltop : MeasureTheory.volume U ≠ ⊤) (F G : ↥(HilbertVectorL2 U)) :
√(normalizedLocalSymmetricEnergy hEll (F + G)) ≤ √(normalizedLocalSymmetricEnergy hEll F) + √(normalizedLocalSymmetricEnergy hEll G)

The square root of normalized local symmetric energy is subadditive.

source
theorem HCPolySupport.HighContrast.sqrt_normalizedLocalSymmetricEnergy_sub_le_sum_Ico {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < MeasureTheory.volume U) (hvoltop : MeasureTheory.volume U ≠ ⊤) (g : ℕ → ↥(HilbertVectorL2 U)) (k m : ℕ) (hkm : k ≤ m) :
√(normalizedLocalSymmetricEnergy hEll (g m - g k)) ≤ ∑ j ∈ Finset.Ico k m, √(normalizedLocalSymmetricEnergy hEll (g (j + 1) - g j))

A finite coefficient-energy telescope is bounded by the sum of its successive coefficient-energy increments.

source
theorem HCPolySupport.HighContrast.sqrt_normalizedLocalSymmetricEnergy_limit_sub_le_of_uniform_tail {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (g : ℕ → ↥(HilbertVectorL2 U)) (L : ↥(HilbertVectorL2 U)) (B : ℝ) (hlim : Filter.Tendsto g Filter.atTop (nhds L)) (k : ℕ) (htail : ∀ (m : ℕ), k ≤ m → √(normalizedLocalSymmetricEnergy hEll (g m - g k)) ≤ B) :
√(normalizedLocalSymmetricEnergy hEll (L - g k)) ≤ B

A uniform coefficient-energy tail passes to a local Hilbert limit.