Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.CorrectorIntrinsicSlopeCanonical

High-contrast homogenization: Provider.Regularity.CorrectorIntrinsicSlopeCanonical #

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

Topological reduction of canonical intrinsic slope #

This module isolates the topology-only part of normalized-slope identification. The intrinsic full-gradient slope is equivalent to vanishing corrector-gradient averages, and the average commutes with every fixed-cube joint local limit.

source
theorem HCPolySupport.HighContrast.continuous_localGradientClassAverage {d n : ℕ} :
Continuous localGradientClassAverage

Averaging a local gradient class is continuous.

source
def HCPolySupport.HighContrast.HasVanishingCorrectorGradientAverage {d : ℕ} (z : NormalizedLocalH1Carrier d) :
Prop

The corrector part has asymptotically vanishing normalized gradient average on the centered exhaustion.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem HCPolySupport.HighContrast.HasVanishingCorrectorGradientAverage.hasIntrinsicNormalizedSlope {d : ℕ} {e : Vec d} {z : NormalizedLocalH1Carrier d} (h : HasVanishingCorrectorGradientAverage z) :
    HasIntrinsicNormalizedSlope e z

    Vanishing corrector averages imply the intrinsic full-gradient slope.

    source
    theorem HCPolySupport.HighContrast.HasIntrinsicNormalizedSlope.hasVanishingCorrectorGradientAverage {d : ℕ} {e : Vec d} {z : NormalizedLocalH1Carrier d} (h : HasIntrinsicNormalizedSlope e z) :
    HasVanishingCorrectorGradientAverage z

    Intrinsic full-gradient slope forces the corrector-class averages to vanish.

    source
    theorem HCPolySupport.HighContrast.finiteAffineCorrectionLocalGradientAverage_tendsto {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (hCauchy : FiniteAffineCorrectionLocalCauchy a) (e : Vec d) (n : ℕ) :
    Filter.Tendsto (fun (k : ℕ) => localGradientClassAverage (normalizedLocalPair (finiteAffineCorrectionLocalSequence a e) n k).2) Filter.atTop (nhds (localGradientClassAverage ((finiteAffineCorrectionJointLocalLimit a hCauchy e).gradientComponent n)))

    On every fixed cube, the averages of normalized finite-corrector gradient classes converge to the average of the canonical joint-limit component.