High-contrast homogenization: Provider.Regularity.FiniteAffineSlopeMap

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

Finite affine-solution best-fit slopes

This module restricts a finite affine-boundary solution to a smaller centered cube and composes that scalar L² datum with the affine best-fit maps. The resulting coefficient and slope maps are algebraic linear maps. No matrix inverse or quantitative coefficient-space norm is introduced here.

theorem HCPolySupport.HighContrast.originCube_mem_descendantsAtDepth_of_int_le {d : ℕ} {k m : ℤ} (hkm : k ≤ m) : originCube d k ∈ descendantsAtDepth (originCube d m) (m - k).toNat

noncomputable def HCPolySupport.HighContrast.finiteAffineSolutionInnerH1 {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (k m : ℤ) (hkm : k ≤ m) (e : Vec d) : H1Function (Book.Ch02.cubeDomain (originCube d k)).carrier

The affine-boundary solution on Q_m, restricted as an H¹ function to the inner cube Q_k.

Equations

• HCPolySupport.HighContrast.finiteAffineSolutionInnerH1 a k m hkm e = (HCPolySupport.HighContrast.finiteAffineSolution a m e).toH1.restrictToOpenSubcube ⋯

@[simp]

theorem HCPolySupport.HighContrast.finiteAffineSolutionInnerH1_toFun {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (k m : ℤ) (hkm : k ≤ m) (e : Vec d) : (finiteAffineSolutionInnerH1 a k m hkm e).toFun = (finiteAffineSolution a m e).toH1.toFun

Restriction leaves the selected finite solution's representative unchanged.

@[simp]

theorem HCPolySupport.HighContrast.finiteAffineSolutionInnerH1_grad {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (k m : ℤ) (hkm : k ≤ m) (e : Vec d) : (finiteAffineSolutionInnerH1 a k m hkm e).grad = (finiteAffineSolution a m e).toH1.grad

Restriction leaves the selected finite solution's weak gradient unchanged.

theorem HCPolySupport.HighContrast.finiteAffineSolutionInnerH1_toFun_add_ae {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (k m : ℤ) (hkm : k ≤ m) (e e' : Vec d) : (finiteAffineSolutionInnerH1 a k m hkm (e + e')).toFun =ᵐ[volumeMeasureOn (Book.Ch02.cubeDomain (originCube d k)).carrier] fun (x : Vec d) => (finiteAffineSolutionInnerH1 a k m hkm e).toFun x + (finiteAffineSolutionInnerH1 a k m hkm e').toFun x

theorem HCPolySupport.HighContrast.finiteAffineSolutionInnerH1_toFun_smul_ae {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (k m : ℤ) (hkm : k ≤ m) (r : ℝ) (e : Vec d) : (finiteAffineSolutionInnerH1 a k m hkm (r • e)).toFun =ᵐ[volumeMeasureOn (Book.Ch02.cubeDomain (originCube d k)).carrier] fun (x : Vec d) => r * (finiteAffineSolutionInnerH1 a k m hkm e).toFun x

theorem HCPolySupport.HighContrast.h1_toScalarL2_eq_of_ae_eq {d : ℕ} {U : Set (Vec d)} (u v : H1Function U) (huv : u.toFun =ᵐ[volumeMeasureOn U] v.toFun) : u.toScalarL2 = v.toScalarL2

noncomputable def HCPolySupport.HighContrast.finiteAffineSolutionInnerL2LinearMap {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (k m : ℤ) (hkm : k ≤ m) : Vec d →ₗ[ℝ] ↥(ScalarL2 (Book.Ch02.cubeDomain (originCube d k)).carrier)

The inner-cube scalar L² realization of finite affine-boundary solutions, linear in the boundary slope.

Equations

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

theorem HCPolySupport.HighContrast.finiteAffineSolutionInnerL2LinearMap_apply {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (k m : ℤ) (hkm : k ≤ m) (e : Vec d) : (finiteAffineSolutionInnerL2LinearMap a k m hkm) e = (finiteAffineSolutionInnerH1 a k m hkm e).toScalarL2

Application of the inner finite-solution L² map.

noncomputable def HCPolySupport.HighContrast.finiteAffineBestFitCoefficients {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (k m : ℤ) (hkm : k ≤ m) : Vec d →ₗ[ℝ] AffineCoefficients d

Best affine coefficients on Q_k for the finite solution posed on Q_m, linear in its boundary slope.

Equations

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

noncomputable def HCPolySupport.HighContrast.finiteAffineBestFitIntercept {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (k m : ℤ) (hkm : k ≤ m) : Vec d →ₗ[ℝ] ℝ

Best affine intercept on Q_k for the finite solution posed on Q_m.

Equations

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

noncomputable def HCPolySupport.HighContrast.finiteAffineBestFitSlope {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (k m : ℤ) (hkm : k ≤ m) : Vec d →ₗ[ℝ] Vec d

Best affine slope on Q_k for the finite solution posed on Q_m.

Equations

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

@[simp]

theorem HCPolySupport.HighContrast.finiteAffineBestFitIntercept_apply {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (k m : ℤ) (hkm : k ≤ m) (e : Vec d) : (finiteAffineBestFitIntercept a k m hkm) e = (originCubeAffineBestFitIntercept d k) ((finiteAffineSolutionInnerL2LinearMap a k m hkm) e)

Application of the finite-solution best intercept map.

@[simp]

theorem HCPolySupport.HighContrast.finiteAffineBestFitSlope_apply {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (k m : ℤ) (hkm : k ≤ m) (e : Vec d) : (finiteAffineBestFitSlope a k m hkm) e = (originCubeAffineBestFitSlope d k) ((finiteAffineSolutionInnerL2LinearMap a k m hkm) e)

Application of the finite-solution best slope map.

theorem HCPolySupport.HighContrast.normalizedAffineCandidateError_finiteAffineBestFit_le {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (k m : ℤ) (hkm : k ≤ m) (e : Vec d) (c : ℝ) (p : Vec d) : normalizedAffineCandidateError (originCube d k) (finiteAffineSolution a m e).toH1.toFun ((finiteAffineBestFitIntercept a k m hkm) e) ((finiteAffineBestFitSlope a k m hkm) e) ≤ normalizedAffineCandidateError (originCube d k) (finiteAffineSolution a m e).toH1.toFun c p

The finite-solution best coefficients attain the normalized affine error on the inner cube.