Documentation

LeanPool.HighContrastHomogenization.Provider.PolynomialHomogenization.Root.CorrectorComposition.IdentityGaugeTerminalCube

High-contrast homogenization: #

Provider.PolynomialHomogenization.Root.CorrectorComposition.IdentityGaugeTerminalCube

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

The terminal cube solution for the row's own family — (b1) + (b4) #

CorrectorComposition.exists_exactRootTerminalCubeSolution produces a cube solution for any family whose representative is a.e. the exact-root coefficient bRef. The undelayed simultaneous-slope row Root.exists_printOrderUndelayedExactGaugeRow quantifies over u : Book.Ch03.CubeSolution (originCube d m) aIdentity for its own identity-gauge family aIdentity, characterised by

∀ Q, (aIdentity.coeffOn Q).toCoeffField =
  ⇑(geom.centeredCoeffSpace 1 hI (exactGaugeCoeffSpace a abar hS)).1

The bridge between the two is available: rawIdentityCoeff_ae_global identifies that representative, globally and cube by cube, with the exact-root one, and exists_normalizedReferenceCoeffFamily manufactures a family carrying the exact-root identity pointwise. Composing the three closes items (b1) and (b4) together: the ball datum of the large-scale C¹ slope approximation terminal yields a cube solution of the very type the row consumes.

What is still missing for ExactRootGaugeTerminal after this module is recorded in the report: the two volume-ratio comparisons (b2) at the exact root (the Euclidean-ball analogues of the two rounded-ellipsoid weighted-gradient comparisons), and the carrier identification, which is the same residue Root.SelectedReferenceCoeffExact that the corrector-and-flux decay clause and the Liouville characterization clause carry.

source
theorem HCPolySupport.HighContrast.CorrectorComposition.exists_identityGaugeTerminalCubeSolution (d : ℕ) [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) {a : CoeffSpace d} {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) (hI : Matrix.PosDef (symmPart 1)) (aIdentity : Book.Ch03.CoeffFamily d) (hIdentity : ∀ (Q : TriadicCube d), (aIdentity.coeffOn Q).toCoeffField = ↑↑(geom.centeredCoeffSpace 1 hI (exactGaugeCoeffSpace a abar hS))) {R : ℝ} (m : ℤ) (hm : matImage (Selection.normalizedRoot (symmPart abar)) (openCubeSet (originCube d m)) ⊆ ellipsoid abar R) (u : Vec d → ℝ) (Du : Vec d → Vec d) (hu : MemH1a (↑↑a) (ellipsoid abar R) u Du) (hweak : IsWeakSolutionOn (↑↑a) (ellipsoid abar R) Du) :
∃ (w : Book.Ch03.CubeSolution (originCube d m) aIdentity), w.toH1.grad = fun (y : Vec d) => matVecMul (Selection.normalizedRoot (symmPart abar)) (Du (matVecMul (Selection.normalizedRoot (symmPart abar)) y))

The terminal cube solution at the identity-gauge family. From a physical MemH1a weak solution on the ellipsoid, a Chapter 3 cube solution for the canonical identity-gauge family aIdentity on any origin cube whose exact-root image lies inside the ellipsoid.