Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.CorrectorLocalH1

High-contrast homogenization: Provider.Regularity.CorrectorLocalH1 #

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

Local Sobolev representatives of projective limits #

The projective local carrier stores value and gradient L² classes together with membership in the closed weak-gradient graph. This module recovers the canonical H¹ representative on each exhaustion cube and records its exact class-level characterization.

source
noncomputable def HCPolySupport.HighContrast.NormalizedLocalH1Carrier.localH1Function {d : ℕ} (z : NormalizedLocalH1Carrier d) (n : ℕ) :
H1Function (localGradientCube d n)

The canonical local H¹ representative determined by the value-gradient pair on the nth exhaustion cube.

Equations
Instances For
    source
    @[simp]
    theorem HCPolySupport.HighContrast.NormalizedLocalH1Carrier.localH1Function_toScalarL2 {d : ℕ} (z : NormalizedLocalH1Carrier d) (n : ℕ) :
    (z.localH1Function n).toScalarL2 = z.valueComponent n

    The scalar L² class of the recovered local function is the stored value component.

    source
    @[simp]
    theorem HCPolySupport.HighContrast.NormalizedLocalH1Carrier.localH1Function_gradToHilbertVectorL2 {d : ℕ} (z : NormalizedLocalH1Carrier d) (n : ℕ) :
    (z.localH1Function n).gradToHilbertVectorL2 = z.gradientComponent n

    The Hilbert-vector L² gradient class of the recovered local function is the stored gradient component.

    source
    theorem HCPolySupport.HighContrast.NormalizedLocalH1Carrier.localH1Function_toFun_ae {d : ℕ} (z : NormalizedLocalH1Carrier d) (n : ℕ) :
    (z.localH1Function n).toFun =ᵐ[volumeMeasureOn (localGradientCube d n)] ↑↑(z.valueComponent n)

    The recovered value representative agrees almost everywhere with the stored scalar class.

    source
    theorem HCPolySupport.HighContrast.NormalizedLocalH1Carrier.localH1Function_zero_mean {d : ℕ} (z : NormalizedLocalH1Carrier d) :
    MeanZeroOn (localGradientCube d 0) (z.localH1Function 0).toFun

    The unit-cube local representative has the normalization stored by the projective carrier.