High-contrast homogenization: Provider.Regularity.FiniteCorrector

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

Finite affine-boundary solutions on Euclidean cubes

This module constructs the homogeneous solution with affine boundary values on a centered triadic cube. The construction retains the zero-trace correction returned by the Dirichlet solver, so both the function-level boundary condition and its gradient consequence are available to deterministic comparison estimates.

noncomputable def HCPolySupport.HighContrast.finiteAffinePointwiseCoeff {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) : Book.Ch02.CoeffOn (Book.Ch02.cubeDomain (originCube d m))

The pointwise elliptic representative of the coefficient family on the scale-m origin cube.

Equations

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

theorem HCPolySupport.HighContrast.finiteAffinePointwiseCoeff_isElliptic {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) : IsEllipticFieldOn (finiteAffinePointwiseCoeff a m).lam (finiteAffinePointwiseCoeff a m).Lam (Book.Ch02.cubeDomain (originCube d m)).carrier (finiteAffinePointwiseCoeff a m).toCoeffField

noncomputable def HCPolySupport.HighContrast.finiteAffineBoundaryH1 {d : ℕ} (m : ℤ) (e : Vec d) : H1Function (Book.Ch02.cubeDomain (originCube d m)).carrier

The affine boundary datum x ↦ e · x on a centered triadic cube.

Equations

• HCPolySupport.HighContrast.finiteAffineBoundaryH1 m e = HCPolySupport.H1Function.affineOnIsSobolevRegularDomain ⋯ e

@[simp]

theorem HCPolySupport.HighContrast.finiteAffineBoundaryH1_grad {d : ℕ} (m : ℤ) (e : Vec d) : (finiteAffineBoundaryH1 m e).grad = fun (x : Vec d) => e

The affine boundary datum has the prescribed constant gradient.

@[simp]

theorem HCPolySupport.HighContrast.finiteAffineBoundaryH1_toFun {d : ℕ} (m : ℤ) (e : Vec d) : (finiteAffineBoundaryH1 m e).toFun = fun (x : Vec d) => vecDot e x

The affine boundary datum is the Euclidean linear function x ↦ e · x.

noncomputable def HCPolySupport.HighContrast.finiteAffineForcing {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (e : Vec d) : Vec d → Vec d

The forcing vector field given by the negative coefficient flux of the constant slope e.

Equations

• HCPolySupport.HighContrast.finiteAffineForcing a m e x = -HCPolySupport.matVecMul ((HCPolySupport.HighContrast.finiteAffinePointwiseCoeff a m).toCoeffField x) e

noncomputable def HCPolySupport.HighContrast.finiteAffineCorrection {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (e : Vec d) : H10Function (Book.Ch02.cubeDomain (originCube d m)).carrier

The zero-trace correction in the finite affine Dirichlet problem.

Equations

• HCPolySupport.HighContrast.finiteAffineCorrection a m e = HCPolySupport.zeroTraceDirichletRightHandSideSolutionOfClosureRealization ⋯ ⋯ ⋯ ⋯

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

The affine datum x ↦ e · x plus the zero-trace finite correction on the scale-m cube.

Equations

• HCPolySupport.HighContrast.finiteAffineH1 a m e = HCPolySupport.HighContrast.finiteAffineBoundaryH1 m e + (HCPolySupport.HighContrast.finiteAffineCorrection a m e).toH1Function

theorem HCPolySupport.HighContrast.finiteAffineH1_isHarmonic {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (e : Vec d) : IsAHarmonicGradient (a.coeffOn (originCube d m)).toCoeffField (Book.Ch02.cubeDomain (originCube d m)).carrier (finiteAffineH1 a m e).grad

noncomputable def HCPolySupport.HighContrast.finiteAffineSolution {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (e : Vec d) : Book.Ch03.DirichletForcedCubeSolution (originCube d m) a 0

The affine-boundary homogeneous solution on the centered triadic cube.

Equations

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

theorem HCPolySupport.HighContrast.finiteAffineSolution_toH1 {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (e : Vec d) : (finiteAffineSolution a m e).toH1 = finiteAffineBoundaryH1 m e + (finiteAffineCorrection a m e).toH1Function

The selected solution retains its affine datum and zero-trace correction definitionally.

theorem HCPolySupport.HighContrast.finiteAffineSolution_zeroTraceDifference {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (e : Vec d) : ∃ (w : H10Function (Book.Ch02.cubeDomain (originCube d m)).carrier), w.toFun =ᵐ[volumeMeasureOn (Book.Ch02.cubeDomain (originCube d m)).carrier] fun (x : Vec d) => (finiteAffineSolution a m e).toH1.toFun x - (finiteAffineBoundaryH1 m e).toFun x

The function-level affine boundary condition used by comparison theorems.

noncomputable def HCPolySupport.HighContrast.finiteAffineCubeSolution {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (e : Vec d) : Book.Ch03.CubeSolution (originCube d m) a

The affine-boundary solution as the homogeneous cube-solution carrier.

Equations

• HCPolySupport.HighContrast.finiteAffineCubeSolution a m e = { toH1 := (HCPolySupport.HighContrast.finiteAffineSolution a m e).toH1, isHarmonic := ⋯ }

theorem HCPolySupport.HighContrast.finiteAffineSolution_isAffineDirichletSolution {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (e : Vec d) : IsAffineDirichletSolution (a.coeffOn (originCube d m)).toCoeffField (Book.Ch02.cubeDomain (originCube d m)).carrier e (finiteAffineSolution a m e).toH1

The selected cube solution is harmonic with affine boundary slope e.

theorem HCPolySupport.HighContrast.finiteAffineSolution_grad_ae_eq_of_isAffineDirichletSolution {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (e : Vec d) (u : H1Function (Book.Ch02.cubeDomain (originCube d m)).carrier) (hu : IsAffineDirichletSolution (a.coeffOn (originCube d m)).toCoeffField (Book.Ch02.cubeDomain (originCube d m)).carrier e u) : (finiteAffineSolution a m e).toH1.grad =ᵐ[volumeMeasureOn (Book.Ch02.cubeDomain (originCube d m)).carrier] u.grad

Any affine Dirichlet solution with the same slope has the selected weak gradient almost everywhere.

theorem HCPolySupport.HighContrast.finiteAffineSolution_grad_add {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (e e' : Vec d) : (finiteAffineSolution a m (e + e')).toH1.grad =ᵐ[volumeMeasureOn (Book.Ch02.cubeDomain (originCube d m)).carrier] fun (x : Vec d) => (finiteAffineSolution a m e).toH1.grad x + (finiteAffineSolution a m e').toH1.grad x

The selected affine-solution gradient is additive in the boundary slope.

theorem HCPolySupport.HighContrast.finiteAffineSolution_grad_smul {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (c : ℝ) (e : Vec d) : (finiteAffineSolution a m (c • e)).toH1.grad =ᵐ[volumeMeasureOn (Book.Ch02.cubeDomain (originCube d m)).carrier] fun (x : Vec d) => c • (finiteAffineSolution a m e).toH1.grad x

The selected affine-solution gradient is homogeneous in the boundary slope.

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

The selected affine solution is additive in the boundary slope almost everywhere.

theorem HCPolySupport.HighContrast.finiteAffineSolution_toFun_smul {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (c : ℝ) (e : Vec d) : (finiteAffineSolution a m (c • e)).toH1.toFun =ᵐ[volumeMeasureOn (Book.Ch02.cubeDomain (originCube d m)).carrier] fun (x : Vec d) => c * (finiteAffineSolution a m e).toH1.toFun x

The selected affine solution is homogeneous in the boundary slope almost everywhere.

theorem HCPolySupport.HighContrast.finiteAffineBoundaryH1_isConstantCoeffForcedEquation {d : ℕ} (m : ℤ) (e : Vec d) : Book.Ch03.IsConstantCoeffForcedEquation (originCube d m) (identityConstantCoeffMatrix d) (finiteAffineBoundaryH1 m e) 0

noncomputable def HCPolySupport.HighContrast.finiteAffineComparisonDatum {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (e : Vec d) : Book.Ch03.CoarseGrainingComparisonDatum (originCube d m) a (identityConstantCoeffMatrix d) 0

Comparison data pairing the a-harmonic finite affine solution with the affine solution for the identity coefficient and zero forcing.

Equations

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

theorem HCPolySupport.HighContrast.exists_finiteAffineSolutionEnergyEstimateConstant (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs_lt : s < 1) : ∃ (C : ℝ), 0 < C ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (e : Vec d), Book.Ch03.h1EnergyNormOnCube (originCube d m) a (finiteAffineSolution a m e).toH1 ≤ C * (1 + scalarIdentityWeakError a s m) * euclideanNorm e

The coefficient-energy norm of the finite affine-boundary solution is controlled by the q = 2 identity response error at the same order.

theorem HCPolySupport.HighContrast.exists_finiteAffineSolutionNegativeBesovEstimateConstant_at_error_order (d : ℕ) [NeZero d] (sOut b : ℝ) (hb : 0 < b) (h2b : 2 * b < sOut) (hsOut_lt : sOut < 1) : ∃ (C : ℝ), 0 < C ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (e : Vec d), Book.Ch03.homogenizationComparisonNegativeBesovLHS (originCube d m) a (identityConstantCoeffMatrix d) sOut (finiteAffineSolution a m e).toH1 (finiteAffineBoundaryH1 m e) ≤ C * scalarIdentityWeakError a b m * (1 + scalarIdentityWeakError a b m) * euclideanNorm e

The printed display HC (5.61) at matched order. At output order sOut, the finite solution's weak gradient and flux errors are controlled by the q = 2 response error at every order b with 2 * b < sOut; the symmetric split b = r / 2 of the negative-Besov estimate constant is the special case r = 2 * b. Taking sOut := b + 1 / 2 therefore admits every b < 1 / 2.

theorem HCPolySupport.HighContrast.exists_finiteAffineSolutionL2SlopeErrorEstimateConstant_at_error_order (d : ℕ) [NeZero d] (b : ℝ) (hb : 0 < b) (hb_lt : b < 1 / 2) : ∃ (C : ℝ), 0 < C ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (e : Vec d), (cubeBesovScaleWeight 1 (originCube d m) * cubeLpNorm (originCube d m) 2 fun (x : Vec d) => (finiteAffineCorrection a m e).toFun x) ≤ C * scalarIdentityWeakError a b m * (1 + scalarIdentityWeakError a b m) * euclideanNorm e

The printed display HC (5.62) at matched order. The normalized L² size of the finite zero-trace correction is controlled by the response error at the same order b, for every b ∈ (0, 1/2) — the printed window of HC, Proposition 5.3.