High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorDecay.JointRemainderRows

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

theorem HCPolySupport.HighContrast.cubeSolution_weakFluxIntegrable {d : ℕ} {Q : TriadicCube d} {a : Book.Ch02.TriadicCoeffFamily d} (u : Book.Ch03.CubeSolution Q a) : weakFluxIntegrable (Book.Ch02.cubeDomain Q).carrier (a.coeffOn Q).toCoeffField u

noncomputable def HCPolySupport.HighContrast.jointAffineCubeSolution {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (Phi : Vec d → NormalizedLocalH1Carrier d) (hPhi : IsFiniteAffineCorrectionJointLocalEquation a Phi) (e : Vec d) (q : ℕ) : Book.Ch03.CubeSolution (originCube d ↑q) a

Harmonic cube solution formed by adding the joint local corrector to the affine boundary function.

Equations

• HCPolySupport.HighContrast.jointAffineCubeSolution a Phi hPhi e q = { toH1 := HCPolySupport.HighContrast.finiteAffineBoundaryH1 (↑q) e + id ((Phi e).localH1Function q), isHarmonic := ⋯ }

noncomputable def HCPolySupport.HighContrast.finiteAffineInnerCubeSolution {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (e : Vec d) (q m : ℕ) (hqm : q ≤ m) : Book.Ch03.CubeSolution (originCube d ↑q) a

Restriction to generation q of the finite affine cube solution at generation m.

Equations

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

noncomputable def HCPolySupport.HighContrast.jointFiniteRemainderCubeSolution {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (Phi : Vec d → NormalizedLocalH1Carrier d) (hPhi : IsFiniteAffineCorrectionJointLocalEquation a Phi) (e : Vec d) (q m : ℕ) (hqm : q ≤ m) : Book.Ch03.CubeSolution (originCube d ↑q) a

Difference between the joint affine solution and the restricted finite affine solution, using their integrable fluxes.

Equations

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

theorem HCPolySupport.HighContrast.jointFiniteRemainder_grad {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (Phi : Vec d → NormalizedLocalH1Carrier d) (hPhi : IsFiniteAffineCorrectionJointLocalEquation a Phi) (e : Vec d) (q m : ℕ) (hqm : q ≤ m) : (jointFiniteRemainderCubeSolution a Phi hPhi e q m hqm).toH1.grad = fun (x : Vec d) => e + ((Phi e).localH1Function q).grad x - (finiteAffineSolution a (↑m) e).toH1.grad x

theorem HCPolySupport.HighContrast.jointFiniteRemainder_energy_eq {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (Phi : Vec d → NormalizedLocalH1Carrier d) (hPhi : IsFiniteAffineCorrectionJointLocalEquation a Phi) (e : Vec d) (q m : ℕ) (hqm : q ≤ m) : Book.Ch03.h1EnergyNormOnCube (originCube d ↑q) a (jointFiniteRemainderCubeSolution a Phi hPhi e q m hqm).toH1 = √(normalizedLocalSymmetricEnergy ⋯ ((have this := constantGradientOnOriginCube e ↑q; this) + (Phi e).gradientComponent q - finiteAffineInnerGradientClass a e q (m - q)))

theorem HCPolySupport.HighContrast.exists_jointFiniteRemainderRowsConstant (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) : ∃ (C : ℝ), 0 < C ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (Phi : Vec d → NormalizedLocalH1Carrier d) (hPhi : IsFiniteAffineCorrectionJointLocalEquation a Phi) (e : Vec d) (q m : ℕ) (hqm : q ≤ m) (B : ℝ), scalarIdentityWeakError a s ↑q ≤ 1 → Book.Ch03.h1EnergyNormOnCube (originCube d ↑q) a (jointFiniteRemainderCubeSolution a Phi hPhi e q m hqm).toH1 ≤ B → cubeScaleNormalizedDualNegativeBesovVectorNormTwo (originCube d ↑q) s (jointFiniteRemainderCubeSolution a Phi hPhi e q m hqm).toH1.grad ≤ C * B ∧ (cubeScaleNormalizedDualNegativeBesovVectorNormTwo (originCube d ↑q) s fun (x : Vec d) => matVecMul (Book.Ch03.publicCoeffField (originCube d ↑q) a x) ((jointFiniteRemainderCubeSolution a Phi hPhi e q m hqm).toH1.grad x)) ≤ C * B

The harmonic difference between the joint exact-gauge corrector and a finite affine corrector has both printed-order rows controlled by its coefficient energy, with a law-free multiplier.