High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Corrector.C1GradientMinimizerAttainment

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

Attainment of the finite affine-gradient excess

The affine-gradient candidates form a finite-dimensional subspace of the Hilbert realization of harmonic gradients. Coercive Hilbert minimization therefore selects an exact best candidate.

noncomputable def HCPolySupport.HighContrast.Root.finiteAffineHarmonicGradient {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) {n m : ℤ} (hnm : n ≤ m) (e : Vec d) : ↥(AHarmonicGradientHilbert.Space (PotentialSolenoidalL2Data.ofSubmoduleClosures (openCubeSet (originCube d n))) ⋯)

The harmonic Hilbert-space gradient on cube n of the finite affine solution with slope e on cube m, for n ≤ m.

Equations

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

theorem HCPolySupport.HighContrast.Root.finiteAffineHarmonicGradient_add {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) {n m : ℤ} (hnm : n ≤ m) (e e' : Vec d) : finiteAffineHarmonicGradient a hnm (e + e') = finiteAffineHarmonicGradient a hnm e + finiteAffineHarmonicGradient a hnm e'

theorem HCPolySupport.HighContrast.Root.finiteAffineHarmonicGradient_smul {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) {n m : ℤ} (hnm : n ≤ m) (c : ℝ) (e : Vec d) : finiteAffineHarmonicGradient a hnm (c • e) = c • finiteAffineHarmonicGradient a hnm e

noncomputable def HCPolySupport.HighContrast.Root.finiteAffineHarmonicGradientLinearMap {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) {n m : ℤ} (hnm : n ≤ m) : Vec d →ₗ[ℝ] ↥(AHarmonicGradientHilbert.Space (PotentialSolenoidalL2Data.ofSubmoduleClosures (openCubeSet (originCube d n))) ⋯)

The linear map sending a slope to the restricted finite affine harmonic gradient on the smaller origin cube.

Equations

• HCPolySupport.HighContrast.Root.finiteAffineHarmonicGradientLinearMap a hnm = { toFun := HCPolySupport.HighContrast.Root.finiteAffineHarmonicGradient a hnm, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def HCPolySupport.HighContrast.Root.restrictedSolutionHarmonicGradient {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) {n m : ℤ} (hnm : n ≤ m) (u : Book.Ch03.CubeSolution (originCube d m) a) : ↥(AHarmonicGradientHilbert.Space (PotentialSolenoidalL2Data.ofSubmoduleClosures (openCubeSet (originCube d n))) ⋯)

The harmonic Hilbert-space gradient of a cube solution restricted from scale m to scale n ≤ m.

Equations

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

noncomputable def HCPolySupport.HighContrast.Root.affineResidualHarmonicGradient {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) {n m : ℤ} (hnm : n ≤ m) (u : Book.Ch03.CubeSolution (originCube d m) a) (e : Vec d) : ↥(AHarmonicGradientHilbert.Space (PotentialSolenoidalL2Data.ofSubmoduleClosures (openCubeSet (originCube d n))) ⋯)

The harmonic gradient of the residual after subtracting the finite affine solution with slope e, restricted to the smaller origin cube.

Equations

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

theorem HCPolySupport.HighContrast.Root.exists_finiteAffineGradientExcess_candidate_le {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) {n m : ℤ} (hnm : n ≤ m) (u : Book.Ch03.CubeSolution (originCube d m) a) : ∃ (b : Vec d), (weightedGradNorm (a.coeffOn (originCube d n)).toCoeffField (openCubeSet (originCube d n)) fun (x : Vec d) => u.toH1.grad x - (finiteAffineSolution a m b).toH1.grad x) ≤ finiteAffineGradientExcess a n m u

The finite affine-gradient excess has an exact minimizing slope.

theorem HCPolySupport.HighContrast.Root.exists_finiteAffineGradientExcess_candidate_eq {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) {n m : ℤ} (hnm : n ≤ m) (u : Book.Ch03.CubeSolution (originCube d m) a) : ∃ (b : Vec d), (weightedGradNorm (a.coeffOn (originCube d n)).toCoeffField (openCubeSet (originCube d n)) fun (x : Vec d) => u.toH1.grad x - (finiteAffineSolution a m b).toH1.grad x) = finiteAffineGradientExcess a n m u

A selected minimizing slope realizes the defining infimum exactly.