Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.FiniteAffineRegularityJointAssembly

High-contrast homogenization: Provider.Regularity.FiniteAffineRegularityJointAssembly #

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

Joint finite-excess decay and infinite corrector assembly #

One small good-tail threshold supplies both the finite-volume real-rate excess estimate and the unique joint normalized local corrector family with its local equations.

source
def HCPolySupport.HighContrast.IsFiniteAffineCorrectionJointLocalEquation {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (Phi : Vec d → NormalizedLocalH1Carrier d) :
Prop

Joint normalized local-limit and fixed-cube equation property.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem HCPolySupport.HighContrast.exists_scalarIdentityFiniteExcessDecayAndJointLocalEquationConstants (d : ℕ) [NeZero d] (s eta : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) (heta0 : 0 ≤ eta) (heta1 : eta < 1) :
    ∃ (Cfamily : ℝ) (c : ℝ) (Cdec : ℝ), 1 ≤ Cfamily ∧ c ∈ Set.Ioo 0 1 ∧ 0 < Cdec ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (delta : ℝ) (n : ℤ), delta ∈ Set.Ioc 0 c → ScalarIdentityGoodTail a s delta n → (∃! Phi : Vec d → NormalizedLocalH1Carrier d, IsFiniteAffineCorrectionJointLocalEquation a Phi) ∧ ∀ (m : ℤ), n < m → ∃ (Q : ℤ → Mat d), IsFiniteAffineSlopeFamily a delta Cfamily n m Q ∧ ∀ (u : Book.Ch03.CubeSolution (originCube d m) a), finiteAffineGradientExcess a n m u ≤ ENNReal.ofReal (Cdec * Real.rpow 3 (-eta * ↑(m - n))) * finiteAffineGradientExcess a m m u

    A single scalar good tail produces both sides of the regularity interface: real-rate finite excess decay on every later interval and the unique joint normalized local corrector family satisfying every fixed-cube equation.