High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Corrector .SelectedGenerationRoundedEllipsoidTerminalCubeSolution

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

Terminal ellipsoid solution at a selected rounded generation

The printed-order recurrence selects a rounded generation after its analytic constant is known. This file transports a physical weak solution through that selected matrix and packages the terminal origin-cube solution used by the finite recurrence.

def HCPolySupport.HighContrast.Root.selectedRoundedPullbackEllipsoid {d : ℕ} [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) (abar : Mat d) (r : ℝ) : Set (Vec d)

The inverse image of a physical ellipsoid under a selected rounded grid.

Equations

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

def HCPolySupport.HighContrast.Root.selectedRoundedPhysicalCube {d : ℕ} [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) (abar : Mat d) (m : ℤ) : Set (Vec d)

The physical image of an origin cube under a selected rounded grid.

Equations

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

theorem HCPolySupport.HighContrast.Root.selectedRoundedPullbackEllipsoid_eq {d : ℕ} [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (r : ℝ) : selectedRoundedPullbackEllipsoid geom abar r = {y : Vec d | vecDot y (matVecMul (geom.referenceMatrix abar hS)⁻¹ y) ≤ r ^ 2}

The selected rounded pullback has the exact quadratic sublevel-set form.

theorem HCPolySupport.HighContrast.Root.openCube_terminalGeneration_subset_selectedRoundedPullbackEllipsoid {d : ℕ} [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) {R : ℝ} (hR : 0 < R) : openCubeSet (originCube d (roundedEllipsoidTerminalGeneration R hR)) ⊆ selectedRoundedPullbackEllipsoid geom abar R

The standard interior terminal cube lies inside the selected-generation pullback ellipsoid.

theorem HCPolySupport.HighContrast.Root.selectedRoundedPhysicalCube_terminalGeneration_subset_ellipsoid {d : ℕ} [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) {R : ℝ} (hR : 0 < R) : selectedRoundedPhysicalCube geom abar (roundedEllipsoidTerminalGeneration R hR) ⊆ ellipsoid abar R

The selected terminal physical cube lies in the original ellipsoid.

theorem HCPolySupport.HighContrast.Root.exists_roundedEllipsoidTerminalCubeSolutionAtGeneration {d : ℕ} [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) (a : CoeffSpace d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (aRounded : Book.Ch03.CoeffFamily d) (hRoundedAE : ∀ (Q : TriadicCube d), (aRounded.coeffOn Q).toCoeffField =ᵐ[MeasureTheory.volume] roundedCenteredCoefficientAtGeneration geom.generation ⋯ abar hS ↑↑a) {R : ℝ} (hR : 0 < 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 (roundedEllipsoidTerminalGeneration R hR)) aRounded), w.toH1.grad = fun (y : Vec d) => matVecMul (geom.grid (symmPart abar)) (Du (matVecMul (geom.grid (symmPart abar)) y))

A physical weak solution gives the terminal Chapter 3 cube solution at the selected rounded generation.