High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Corrector.C1WeightedCorrectorProjection

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

Coefficient-weighted projection of a joint corrector onto a finite span

On a fixed inner cube, finite affine-solution gradients form an injected finite-dimensional trial space once the scalar good tail is small. The coercive symmetric coefficient form therefore gives a canonical linear least-squares slope selector for the joint corrector family.

noncomputable def HCPolySupport.HighContrast.Root.finiteTrialHarmonicGradient {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) {q m : ℕ} (hqm : q ≤ m) (e : Vec d) : ↥(AHarmonicGradientHilbert.Space (PotentialSolenoidalL2Data.ofSubmoduleClosures (localGradientCube d q)) ⋯)

The finite affine trial gradient at scale m, viewed in the harmonic Hilbert space on the local cube at scale q ≤ m.

Equations

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

theorem HCPolySupport.HighContrast.Root.finiteTrialHarmonicGradient_add {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) {q m : ℕ} (hqm : q ≤ m) (e e' : Vec d) : finiteTrialHarmonicGradient a hqm (e + e') = finiteTrialHarmonicGradient a hqm e + finiteTrialHarmonicGradient a hqm e'

theorem HCPolySupport.HighContrast.Root.finiteTrialHarmonicGradient_smul {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) {q m : ℕ} (hqm : q ≤ m) (c : ℝ) (e : Vec d) : finiteTrialHarmonicGradient a hqm (c • e) = c • finiteTrialHarmonicGradient a hqm e

noncomputable def HCPolySupport.HighContrast.Root.finiteTrialHarmonicGradientLinearMap {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) {q m : ℕ} (hqm : q ≤ m) : Vec d →ₗ[ℝ] ↥(AHarmonicGradientHilbert.Space (PotentialSolenoidalL2Data.ofSubmoduleClosures (localGradientCube d q)) ⋯)

The finite affine full-gradient trial map in the harmonic-gradient Hilbert space of the inner cube.

Equations

• HCPolySupport.HighContrast.Root.finiteTrialHarmonicGradientLinearMap a hqm = { toFun := HCPolySupport.HighContrast.Root.finiteTrialHarmonicGradient a hqm, map_add' := ⋯, map_smul' := ⋯ }

theorem HCPolySupport.HighContrast.Root.jointTargetHarmonicGradient_field_eq {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (hCauchy : FiniteAffineCorrectionLocalCauchy a) (q : ℕ) (e : Vec d) : ↑(AHarmonicGradientHilbert.ofAHarmonicFunction (PotentialSolenoidalL2Data.ofSubmoduleClosures (localGradientCube d q)) ⋯ (finiteAffineCorrectionJointLocalCubeSolution a hCauchy e q).toPointwiseAHarmonic) = (jointAffineFullGradientLinearMap a hCauchy q) e

The harmonic-space target map has the canonical joint affine-gradient representative on the inner cube.

noncomputable def HCPolySupport.HighContrast.Root.jointTargetHarmonicGradientLinearMap {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (hCauchy : FiniteAffineCorrectionLocalCauchy a) (q : ℕ) : Vec d →ₗ[ℝ] ↥(AHarmonicGradientHilbert.Space (PotentialSolenoidalL2Data.ofSubmoduleClosures (localGradientCube d q)) ⋯)

The joint affine-plus-corrector full gradient, as a linear map into the same harmonic-gradient Hilbert space.

Equations

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

theorem HCPolySupport.HighContrast.Root.finiteTrialHarmonicGradientLinearMap_injective {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (s delta c : ℝ) (n0 : ℤ) (hdelta : delta ∈ Set.Ioc 0 c) (hgood : ScalarIdentityGoodTail a s delta n0) (hcoercive : ∀ (a : Book.Ch02.TriadicCoeffFamily d) (delta : ℝ) (n : ℤ), delta ∈ Set.Ioc 0 c → ScalarIdentityGoodTail a s delta n → ∀ (q t : ℕ), n ≤ ↑q → ∀ (e : Vec d), euclideanNorm e ≤ 2 * euclideanNorm (cubeAverageVec (originCube d ↑q) (finiteAffineSolution a (↑(q + t + 2)) e).toH1.grad)) (q m : ℕ) (hnq : n0 ≤ ↑q) (hqm2 : q + 2 ≤ m) : Function.Injective ⇑(finiteTrialHarmonicGradientLinearMap a ⋯)

The finite trial map is injective under the small-good-tail average-slope coercivity estimate.

noncomputable def HCPolySupport.HighContrast.Root.finiteCorrectorWeightedProjection {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (hCauchy : FiniteAffineCorrectionLocalCauchy a) {q m : ℕ} (hqm : q ≤ m) (hT : Function.Injective ⇑(finiteTrialHarmonicGradientLinearMap a hqm)) : Vec d →ₗ[ℝ] Vec d

The coefficient-weighted least-squares parameter map on the inner cube.

Equations

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

theorem HCPolySupport.HighContrast.Root.finiteCorrectorWeightedProjection_minimizes {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (hCauchy : FiniteAffineCorrectionLocalCauchy a) {q m : ℕ} (hqm : q ≤ m) (hT : Function.Injective ⇑(finiteTrialHarmonicGradientLinearMap a hqm)) (e b : Vec d) : have T := finiteTrialHarmonicGradientLinearMap a hqm; have J := jointTargetHarmonicGradientLinearMap a hCauchy q; have B := AHarmonicGradientHilbert.symmCoeffBilin (PotentialSolenoidalL2Data.ofSubmoduleClosures (localGradientCube d q)) ⋯; quadraticEnergy B (J e - T ((finiteCorrectorWeightedProjection a hCauchy hqm hT) e)) ≤ quadraticEnergy B (J e - T b)

The selected residual minimizes the coefficient quadratic energy against every finite affine trial slope.