High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Corrector.C1CanonicalProjectionExactness

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

Exactness of the canonical finite-corrector projection

The coefficient-weighted least-squares selector minimizes the same local quadratic form that defines the finite affine excess. When its harmonic target is the restriction of a cube solution, it therefore realizes that excess exactly.

theorem HCPolySupport.HighContrast.Root.residualWeightedNorm_sq_eq_ofReal_energy {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) {q m : ℕ} (hqm : q ≤ m) (u : Book.Ch03.CubeSolution (originCube d ↑m) a) (b : Vec d) : (weightedGradNorm (a.coeffOn (originCube d ↑q)).toCoeffField (openCubeSet (originCube d ↑q)) fun (x : Vec d) => u.toH1.grad x - (finiteAffineSolution a (↑m) b).toH1.grad x) ^ 2 = ENNReal.ofReal (normalizedLocalSymmetricEnergy ⋯ (finiteAffineGradientResidual a ⋯ u b).toH1.gradToHilbertVectorL2)

Squaring a finite-affine residual norm gives its real normalized coefficient energy.

theorem HCPolySupport.HighContrast.Root.finiteCorrectorWeightedProjection_spec_of_target {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (hCauchy : FiniteAffineCorrectionLocalCauchy a) {q m : ℕ} (hqm : q ≤ m) (hT : Function.Injective ⇑(finiteTrialHarmonicGradientLinearMap a hqm)) (e : Vec d) (u : Book.Ch03.CubeSolution (originCube d ↑m) a) (hJ : ↑((jointTargetHarmonicGradientLinearMap a hCauchy q) e) = (finiteCubeSolutionRestriction a ⋯ u).toH1.gradToHilbertVectorL2) : (weightedGradNorm (a.coeffOn (originCube d ↑q)).toCoeffField (openCubeSet (originCube d ↑q)) fun (x : Vec d) => u.toH1.grad x - (finiteAffineSolution a (↑m) ((finiteCorrectorWeightedProjection a hCauchy hqm hT) e)).toH1.grad x) = finiteAffineGradientExcess a (↑q) (↑m) u

If the harmonic target map agrees with the restriction of a cube solution, the canonical weighted projection realizes its finite affine gradient excess.

theorem HCPolySupport.HighContrast.Root.finiteCorrectorWeightedProjection_eq_exactMinimizer_of_target {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (hCauchy : FiniteAffineCorrectionLocalCauchy a) {q m : ℕ} (hqm : q ≤ m) (hT : Function.Injective ⇑(finiteTrialHarmonicGradientLinearMap a hqm)) (e : Vec d) (u : Book.Ch03.CubeSolution (originCube d ↑m) a) (hJ : ↑((jointTargetHarmonicGradientLinearMap a hCauchy q) e) = (finiteCubeSolutionRestriction a ⋯ u).toH1.gradToHilbertVectorL2) : (finiteCorrectorWeightedProjection a hCauchy hqm hT) e = finiteAffineExactMinimizer a ⋯ u

Under the same target identification, the canonical projection is the proof-irrelevant exact affine-excess minimizer.