Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.PrintOrderRoundedGenerationHarmonicAffineDecay

High-contrast homogenization: Provider.Regularity.PrintOrderRoundedGenerationHarmonicAffineDecay #

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

Affine decay for the rounded constant reference #

This file proves the deterministic constant-coefficient affine improvement used at HC (5.66). The rounded matrix itself is the weak operator in the statement. Its fixed 99/100--101/100 order bounds are used only to make all geometric constants dimension-only.

source
noncomputable def HCPolySupport.HighContrast.roundedAffineVolumeRatioBound (d : ℕ) :
ℝ

Dimension-only upper bound used for volumes of rounded affine pullbacks.

Equations
Instances For
    source
    noncomputable def HCPolySupport.HighContrast.roundedAffineNormFactor (d : ℕ) :
    ℝ

    Real-valued square-root factor associated with the rounded affine volume-ratio bound.

    Equations
    Instances For
      source
      theorem HCPolySupport.HighContrast.exists_printOrderRoundedReference_harmonic_normalized_affine_candidate_error_decay (d : ℕ) [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) (theta : ℝ) (htheta : 0 < theta) :
      ∃ (N : ℕ), 0 < N ∧ ∀ (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (k : ℤ) (u : H1Function (openCubeSet (originCube d k))), IsWeakSolutionOn (constantCoeffField (geom.referenceMatrix abar hS)) (openCubeSet (originCube d k)) u.grad → ∀ (c : ℝ) (e : Vec d), ∃ (c' : ℝ) (e' : Vec d), normalizedAffineCandidateError (originCube d (k - ↑N)) u.toFun c' e' ≤ theta * normalizedAffineCandidateError (originCube d k) u.toFun c e

      A solution of the genuinely rounded constant equation admits an affine improvement with any prescribed positive contraction. The proof is an exact coordinate normalization; no identity residual is introduced.