High-contrast homogenization: Provider.Regularity.CorrectorIntrinsicSlope

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

Intrinsic slope and growth classes for local correctors

The normalized slope is read directly from each local L² gradient class. Raw vector fields enter only through an explicit almost-everywhere representative lemma. The admissibility predicates therefore carry no Cauchy certificate, starting scale, or chosen pointwise global representative.

noncomputable def HCPolySupport.HighContrast.localGradientClassAverage {d n : ℕ} (g : ↥(LocalGradientL2 d n)) : Vec d

The normalized coordinate integral of a local gradient L² class.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.localGradientClassAverage_eq_cubeAverageVec_of_ae {d n : ℕ} (g : ↥(LocalGradientL2 d n)) (G : Vec d → Vec d) (hG : ↑↑g =ᵐ[volumeMeasureOn (localGradientCube d n)] fun (x : Vec d) => HilbertVec.ofVec (G x)) : localGradientClassAverage g = cubeAverageVec (originCube d ↑n) G

The class average is the usual cube average of any raw representative which agrees with the class almost everywhere on the open cube.

@[simp]

theorem HCPolySupport.HighContrast.localGradientClassAverage_add {d n : ℕ} (g h : ↥(LocalGradientL2 d n)) : localGradientClassAverage (g + h) = localGradientClassAverage g + localGradientClassAverage h

Local gradient-class averaging is additive.

@[simp]

theorem HCPolySupport.HighContrast.localGradientClassAverage_smul {d n : ℕ} (c : ℝ) (g : ↥(LocalGradientL2 d n)) : localGradientClassAverage (c • g) = c • localGradientClassAverage g

Local gradient-class averaging commutes with real scalar multiplication.

@[simp]

theorem HCPolySupport.HighContrast.localGradientClassAverage_zero {d n : ℕ} : localGradientClassAverage 0 = 0

The average of the zero local class is zero.

@[simp]

theorem HCPolySupport.HighContrast.localGradientClassAverage_neg {d n : ℕ} (g : ↥(LocalGradientL2 d n)) : localGradientClassAverage (-g) = -localGradientClassAverage g

Local gradient-class averaging commutes with negation.

@[simp]

theorem HCPolySupport.HighContrast.localGradientClassAverage_sub {d n : ℕ} (g h : ↥(LocalGradientL2 d n)) : localGradientClassAverage (g - h) = localGradientClassAverage g - localGradientClassAverage h

Local gradient-class averaging commutes with subtraction.

noncomputable def HCPolySupport.HighContrast.affinePlusLocalCarrierH1 {d : ℕ} (e : Vec d) (z : NormalizedLocalH1Carrier d) (n : ℕ) : H1Function (localGradientCube d n)

The full affine-plus-corrector local representative attached to an intrinsic local carrier.

Equations

• HCPolySupport.HighContrast.affinePlusLocalCarrierH1 e z n = (have this := id (HCPolySupport.HighContrast.finiteAffineBoundaryH1 (↑n) e); this) + z.localH1Function n

theorem HCPolySupport.HighContrast.localGradientClassAverage_finiteAffineBoundaryH1 {d : ℕ} (e : Vec d) (n : ℕ) : localGradientClassAverage (have this := ⋯.mp (finiteAffineBoundaryH1 (↑n) e).gradToHilbertVectorL2; this) = e

The local class of the constant affine gradient has normalized average equal to the declared affine slope.

@[simp]

theorem HCPolySupport.HighContrast.affinePlusLocalCarrierH1_gradToHilbertVectorL2 {d : ℕ} (e : Vec d) (z : NormalizedLocalH1Carrier d) (n : ℕ) : (affinePlusLocalCarrierH1 e z n).gradToHilbertVectorL2 = (have this := ⋯.mp (finiteAffineBoundaryH1 (↑n) e).gradToHilbertVectorL2; this) + z.gradientComponent n

The recovered full local gradient class is the affine constant class plus the stored projective corrector component.

def HCPolySupport.HighContrast.HasIntrinsicNormalizedSlope {d : ℕ} (e : Vec d) (z : NormalizedLocalH1Carrier d) : Prop

Intrinsic normalized slope, stated only through local gradient classes.

Equations

• One or more equations did not get rendered due to their size.