High-contrast homogenization: Provider.Regularity.AffineBestFit

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

Affine best fits on centered Euclidean cubes

This module constructs the unique L² best affine approximation on a centered triadic cube. Its coefficient and slope maps are algebraic linear maps. In particular, no quantitative statement below uses the ambient function-space norm on Vec d; later slope estimates must be stated with euclideanNorm.

@[reducible, inline]

abbrev HCPolySupport.HighContrast.AffineCoefficients (d : ℕ) : Type

Intercept and Euclidean slope of a scalar affine function.

Equations

• HCPolySupport.HighContrast.AffineCoefficients d = (ℝ × HCPolySupport.Vec d)

noncomputable def HCPolySupport.HighContrast.originCubeAffineH1OfCoefficients (d : ℕ) (k : ℤ) (p : AffineCoefficients d) : H1Function (Book.Ch02.cubeDomain (originCube d k)).carrier

The H¹ affine function x ↦ p.1 + p.2 · x on the origin cube at scale k.

Equations

• HCPolySupport.HighContrast.originCubeAffineH1OfCoefficients d k p = HCPolySupport.H1Function.const p.1 + HCPolySupport.H1Function.affineOnIsSobolevRegularDomain ⋯ p.2

theorem HCPolySupport.HighContrast.originCubeAffineH1OfCoefficients_add (d : ℕ) (k : ℤ) (p q : AffineCoefficients d) : originCubeAffineH1OfCoefficients d k (p + q) = originCubeAffineH1OfCoefficients d k p + originCubeAffineH1OfCoefficients d k q

theorem HCPolySupport.HighContrast.originCubeAffineH1OfCoefficients_smul (d : ℕ) (k : ℤ) (r : ℝ) (p : AffineCoefficients d) : originCubeAffineH1OfCoefficients d k (r • p) = r • originCubeAffineH1OfCoefficients d k p

noncomputable def HCPolySupport.HighContrast.originCubeAffineH1LinearMap (d : ℕ) (k : ℤ) : AffineCoefficients d →ₗ[ℝ] H1Function (Book.Ch02.cubeDomain (originCube d k)).carrier

The affine-coefficient embedding into H¹ on a centered cube.

Equations

• HCPolySupport.HighContrast.originCubeAffineH1LinearMap d k = { toFun := HCPolySupport.HighContrast.originCubeAffineH1OfCoefficients d k, map_add' := ⋯, map_smul' := ⋯ }

theorem HCPolySupport.HighContrast.originCubeAffineH1LinearMap_toFun (d : ℕ) (k : ℤ) (p : AffineCoefficients d) : ((originCubeAffineH1LinearMap d k) p).toFun = fun (x : Vec d) => p.1 + vecDot p.2 x

The affine embedding has the literal representative c + e · x.

theorem HCPolySupport.HighContrast.originCubeAffineH1LinearMap_grad (d : ℕ) (k : ℤ) (p : AffineCoefficients d) : ((originCubeAffineH1LinearMap d k) p).grad = fun (x : Vec d) => p.2

The weak gradient of the affine embedding is its slope.

noncomputable def HCPolySupport.HighContrast.originCubeAffineL2LinearMap (d : ℕ) (k : ℤ) : AffineCoefficients d →ₗ[ℝ] ↥(ScalarL2 (Book.Ch02.cubeDomain (originCube d k)).carrier)

The affine-coefficient embedding into scalar L² on a centered cube.

Equations

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

theorem HCPolySupport.HighContrast.originCubeAffineL2LinearMap_apply (d : ℕ) (k : ℤ) (p : AffineCoefficients d) : (originCubeAffineL2LinearMap d k) p = ((originCubeAffineH1LinearMap d k) p).toScalarL2

The L² affine embedding is the realization of the corresponding H¹ function.

theorem HCPolySupport.HighContrast.originCubeAffineL2LinearMap_ae_eq (d : ℕ) (k : ℤ) (p : AffineCoefficients d) : ↑↑((originCubeAffineL2LinearMap d k) p) =ᵐ[volumeMeasureOn (Book.Ch02.cubeDomain (originCube d k)).carrier] fun (x : Vec d) => p.1 + vecDot p.2 x

The L² affine embedding has its expected almost-everywhere representative.

theorem HCPolySupport.HighContrast.originCubeAffineL2LinearMap_injective (d : ℕ) (k : ℤ) : Function.Injective ⇑(originCubeAffineL2LinearMap d k)

Affine coefficients are determined by their L² class on a positive-dimensional origin cube.

noncomputable def HCPolySupport.HighContrast.originCubeAffineL2Submodule (d : ℕ) (k : ℤ) : Submodule ℝ ↥(ScalarL2 (Book.Ch02.cubeDomain (originCube d k)).carrier)

The finite-dimensional subspace of scalar L² represented by affine functions on an origin cube.

Equations

• HCPolySupport.HighContrast.originCubeAffineL2Submodule d k = (HCPolySupport.HighContrast.originCubeAffineL2LinearMap d k).range

theorem HCPolySupport.HighContrast.originCubeAffineL2SubmoduleHasOrthogonalProjection (d : ℕ) (k : ℤ) : (originCubeAffineL2Submodule d k).HasOrthogonalProjection

noncomputable def HCPolySupport.HighContrast.originCubeAffineL2EquivRange (d : ℕ) (k : ℤ) : AffineCoefficients d ≃ₗ[ℝ] ↥(originCubeAffineL2Submodule d k)

Affine coefficients are linearly equivalent to the literal range of the affine L² embedding.

Equations

• HCPolySupport.HighContrast.originCubeAffineL2EquivRange d k = LinearEquiv.ofInjective (HCPolySupport.HighContrast.originCubeAffineL2LinearMap d k) ⋯

noncomputable def HCPolySupport.HighContrast.originCubeAffineBestFitCoefficients (d : ℕ) (k : ℤ) : ↥(ScalarL2 (Book.Ch02.cubeDomain (originCube d k)).carrier) →ₗ[ℝ] AffineCoefficients d

Coefficients of the orthogonal L² projection onto affine functions.

Equations

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

noncomputable def HCPolySupport.HighContrast.originCubeAffineBestFitIntercept (d : ℕ) (k : ℤ) : ↥(ScalarL2 (Book.Ch02.cubeDomain (originCube d k)).carrier) →ₗ[ℝ] ℝ

Intercept of the unique affine L² best fit.

Equations

• HCPolySupport.HighContrast.originCubeAffineBestFitIntercept d k = LinearMap.fst ℝ ℝ (HCPolySupport.Vec d) ∘ₗ HCPolySupport.HighContrast.originCubeAffineBestFitCoefficients d k

noncomputable def HCPolySupport.HighContrast.originCubeAffineBestFitSlope (d : ℕ) (k : ℤ) : ↥(ScalarL2 (Book.Ch02.cubeDomain (originCube d k)).carrier) →ₗ[ℝ] Vec d

Slope of the unique affine L² best fit.

Equations

• HCPolySupport.HighContrast.originCubeAffineBestFitSlope d k = LinearMap.snd ℝ ℝ (HCPolySupport.Vec d) ∘ₗ HCPolySupport.HighContrast.originCubeAffineBestFitCoefficients d k

theorem HCPolySupport.HighContrast.originCubeAffineBestFitCoefficients_eq (d : ℕ) (k : ℤ) (F : ↥(ScalarL2 (Book.Ch02.cubeDomain (originCube d k)).carrier)) : (originCubeAffineBestFitCoefficients d k) F = ((originCubeAffineBestFitIntercept d k) F, (originCubeAffineBestFitSlope d k) F)

The best coefficient pair consists of the exported intercept and slope.

theorem HCPolySupport.HighContrast.originCubeAffineL2LinearMap_bestFitCoefficients (d : ℕ) (k : ℤ) (F : ↥(ScalarL2 (Book.Ch02.cubeDomain (originCube d k)).carrier)) : (originCubeAffineL2LinearMap d k) ((originCubeAffineBestFitCoefficients d k) F) = (originCubeAffineL2Submodule d k).starProjection F

Re-embedding the best coefficients gives the orthogonal projection onto the affine range.

theorem HCPolySupport.HighContrast.inner_sub_originCubeAffineBestFit_eq_zero (d : ℕ) (k : ℤ) (F : ↥(ScalarL2 (Book.Ch02.cubeDomain (originCube d k)).carrier)) (p : AffineCoefficients d) : inner ℝ (F - (originCubeAffineL2LinearMap d k) ((originCubeAffineBestFitCoefficients d k) F)) ((originCubeAffineL2LinearMap d k) p) = 0

The best-fit residual is orthogonal to every affine function.

theorem HCPolySupport.HighContrast.norm_sub_originCubeAffineBestFit_sq (d : ℕ) (k : ℤ) (F : ↥(ScalarL2 (Book.Ch02.cubeDomain (originCube d k)).carrier)) (p : AffineCoefficients d) : ‖F - (originCubeAffineL2LinearMap d k) p‖ ^ 2 = ‖F - (originCubeAffineL2LinearMap d k) ((originCubeAffineBestFitCoefficients d k) F)‖ ^ 2 + ‖(originCubeAffineL2LinearMap d k) ((originCubeAffineBestFitCoefficients d k) F) - (originCubeAffineL2LinearMap d k) p‖ ^ 2

Pythagorean identity comparing the best affine fit with any affine candidate.

theorem HCPolySupport.HighContrast.norm_sub_originCubeAffineBestFit_le (d : ℕ) (k : ℤ) (F : ↥(ScalarL2 (Book.Ch02.cubeDomain (originCube d k)).carrier)) (p : AffineCoefficients d) : ‖F - (originCubeAffineL2LinearMap d k) ((originCubeAffineBestFitCoefficients d k) F)‖ ≤ ‖F - (originCubeAffineL2LinearMap d k) p‖

The projected affine function minimizes L² distance.

theorem HCPolySupport.HighContrast.normalizedAffineCandidateError_eq_affineL2Norm (d : ℕ) (k : ℤ) (u : H1Function (Book.Ch02.cubeDomain (originCube d k)).carrier) (c : ℝ) (e : Vec d) : normalizedAffineCandidateError (originCube d k) u.toFun c e = cubeBesovScaleWeight 1 (originCube d k) * ((cubeVolume (originCube d k))⁻¹ ^ (1 / 2) * ‖u.toScalarL2 - (originCubeAffineL2LinearMap d k) (c, e)‖)

The normalized affine error is exactly the unnormalized scalar L² norm times the probability-measure and scale factors.

theorem HCPolySupport.HighContrast.normalizedAffineCandidateError_bestFit_le (d : ℕ) (k : ℤ) (u : H1Function (Book.Ch02.cubeDomain (originCube d k)).carrier) (c : ℝ) (e : Vec d) : normalizedAffineCandidateError (originCube d k) u.toFun ((originCubeAffineBestFitIntercept d k) u.toScalarL2) ((originCubeAffineBestFitSlope d k) u.toScalarL2) ≤ normalizedAffineCandidateError (originCube d k) u.toFun c e

The projected coefficients attain the normalized affine-candidate error.