High-contrast homogenization: Provider.Regularity.AffineFlatnessPrep

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

Affine-candidate error algebra on Euclidean cubes

The normalized distance below is the scale-invariant L² quantity used in affine approximation. The main lemmas transfer one affine candidate across a comparison estimate. They are metric-algebra statements and do not assert constant-coefficient harmonic decay.

noncomputable def HCPolySupport.HighContrast.normalizedCubeL2Distance {d : ℕ} (Q : TriadicCube d) (f g : Vec d → ℝ) : ℝ

Scale-normalized L² distance between two scalar fields on a triadic cube.

Equations

• HCPolySupport.HighContrast.normalizedCubeL2Distance Q f g = HCPolySupport.cubeBesovScaleWeight 1 Q * HCPolySupport.cubeLpNorm Q 2 fun (x : HCPolySupport.Vec d) => f x - g x

noncomputable def HCPolySupport.HighContrast.normalizedAffineCandidateError {d : ℕ} (Q : TriadicCube d) (f : Vec d → ℝ) (c : ℝ) (e : Vec d) : ℝ

Scale-normalized L² error relative to the affine candidate x ↦ c + e · x.

Equations

• HCPolySupport.HighContrast.normalizedAffineCandidateError Q f c e = HCPolySupport.HighContrast.normalizedCubeL2Distance Q f fun (x : HCPolySupport.Vec d) => c + HCPolySupport.vecDot e x

theorem HCPolySupport.HighContrast.normalizedCubeL2Distance_nonneg {d : ℕ} (Q : TriadicCube d) (f g : Vec d → ℝ) : 0 ≤ normalizedCubeL2Distance Q f g

The normalized cube distance is nonnegative.

theorem HCPolySupport.HighContrast.normalizedAffineCandidateError_nonneg {d : ℕ} (Q : TriadicCube d) (f : Vec d → ℝ) (c : ℝ) (e : Vec d) : 0 ≤ normalizedAffineCandidateError Q f c e

Every normalized affine-candidate error is nonnegative.

theorem HCPolySupport.HighContrast.normalizedAffineCandidateError_le_distance_add {d : ℕ} (Q : TriadicCube d) (u h : Vec d → ℝ) (c : ℝ) (e : Vec d) (hcomparison : MeasureTheory.MemLp (fun (x : Vec d) => u x - h x) 2 (normalizedCubeMeasure Q)) (hcandidate : MeasureTheory.MemLp (fun (x : Vec d) => h x - (c + vecDot e x)) 2 (normalizedCubeMeasure Q)) : normalizedAffineCandidateError Q u c e ≤ normalizedCubeL2Distance Q u h + normalizedAffineCandidateError Q h c e

Moving an affine candidate across an intermediate comparison function costs at most the normalized distance to that function.