High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Corrector .SelectedGenerationRoundedEllipsoidWeightedNormBridge

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

Weighted norms on a selected rounded generation

The mixed-order recurrence chooses its rounded coordinate matrix after the analytic constants have been fixed. The matrix remains uniformly close to the normalized reference, so the standard rounded-ellipsoid volume and weighted-norm comparisons hold with the same dimension-only constants.

theorem HCPolySupport.HighContrast.Root.euclideanBall_half_subset_selectedRoundedPullbackEllipsoid {d : ℕ} [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (r : ℝ) : euclideanBall d (r / 2) ⊆ selectedRoundedPullbackEllipsoid geom abar r

The Euclidean ball of half the physical radius lies in the pullback for every admissible selected rounded generation.

theorem HCPolySupport.HighContrast.Root.selectedRoundedPullbackEllipsoid_subset_euclideanBall_two_mul {d : ℕ} [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) {r : ℝ} (hr : 0 < r) : selectedRoundedPullbackEllipsoid geom abar r ⊆ euclideanBall d (2 * r)

The selected pullback ellipsoid lies in the Euclidean ball of twice the physical radius.

theorem HCPolySupport.HighContrast.Root.selectedRoundedPullbackEllipsoid_subset_outerCube {d : ℕ} [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) {r : ℝ} (hr : 0 < r) : selectedRoundedPullbackEllipsoid geom abar r ⊆ openCubeSet (originCube d (roundedEllipsoidOuterGeneration r hr))

The selected pullback lies in the canonical dimension-free outer cube.

theorem HCPolySupport.HighContrast.Root.selectedRoundedPullbackEllipsoid_mono {d : ℕ} [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) {r R : ℝ} (hr : 0 < r) (hrR : r ≤ R) : selectedRoundedPullbackEllipsoid geom abar r ⊆ selectedRoundedPullbackEllipsoid geom abar R

The selected rounded pullback is monotone in its positive radius.

theorem HCPolySupport.HighContrast.Root.volume_selectedRoundedPullbackEllipsoid_ne_zero {d : ℕ} [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) {r : ℝ} (hr : 0 < r) : MeasureTheory.volume (selectedRoundedPullbackEllipsoid geom abar r) ≠ 0

A positive-radius selected pullback ellipsoid has positive volume.

theorem HCPolySupport.HighContrast.Root.volume_selectedRoundedPullbackEllipsoid_ne_top {d : ℕ} [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) {r : ℝ} (hr : 0 < r) : MeasureTheory.volume (selectedRoundedPullbackEllipsoid geom abar r) ≠ ⊤

A positive-radius selected pullback ellipsoid has finite volume.

theorem HCPolySupport.HighContrast.Root.outerCube_volume_ratio_lt_selectedRoundedPullbackEllipsoid {d : ℕ} [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) {r : ℝ} (hr : 0 < r) : (MeasureTheory.volume (openCubeSet (originCube d (roundedEllipsoidOuterGeneration r hr)))).toReal / (MeasureTheory.volume (selectedRoundedPullbackEllipsoid geom abar r)).toReal < (12 * √↑d) ^ d

The canonical outer cube has a dimension-only real volume ratio over a selected pullback ellipsoid.

theorem HCPolySupport.HighContrast.Root.outerCube_volume_ratio_le_selectedRoundedPullbackEllipsoid_ofReal {d : ℕ} [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) {r : ℝ} (hr : 0 < r) : MeasureTheory.volume (openCubeSet (originCube d (roundedEllipsoidOuterGeneration r hr))) / MeasureTheory.volume (selectedRoundedPullbackEllipsoid geom abar r) ≤ ENNReal.ofReal ((12 * √↑d) ^ d)

ENNReal form of the selected outer-cube volume-ratio bound.

theorem HCPolySupport.HighContrast.Root.selectedRoundedPullbackEllipsoid_volume_ratio_lt_terminalCube {d : ℕ} [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) {R : ℝ} (hR : 0 < R) : (MeasureTheory.volume (selectedRoundedPullbackEllipsoid geom abar R)).toReal / (MeasureTheory.volume (openCubeSet (originCube d (roundedEllipsoidTerminalGeneration R hR)))).toReal < (1200 * ↑d) ^ d

The selected pullback at the terminal radius has a dimension-only real volume ratio over the interior terminal cube.

theorem HCPolySupport.HighContrast.Root.selectedRoundedPullbackEllipsoid_volume_ratio_le_terminalCube_ofReal {d : ℕ} [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) {R : ℝ} (hR : 0 < R) : MeasureTheory.volume (selectedRoundedPullbackEllipsoid geom abar R) / MeasureTheory.volume (openCubeSet (originCube d (roundedEllipsoidTerminalGeneration R hR))) ≤ ENNReal.ofReal ((1200 * ↑d) ^ d)

ENNReal form of the selected terminal volume-ratio bound.

theorem HCPolySupport.HighContrast.Root.selectedRoundedPullbackEllipsoid_volume_ratio_lt_of_near_terminal {d : ℕ} [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) {r R : ℝ} (hr : 0 < r) (hR : 0 < R) (hnear : R < 400 * ↑d * r) : (MeasureTheory.volume (selectedRoundedPullbackEllipsoid geom abar R)).toReal / (MeasureTheory.volume (selectedRoundedPullbackEllipsoid geom abar r)).toReal < (4800 * ↑d * √↑d) ^ d

Near the terminal radius, selected pullback volumes have a dimension-only ratio.

theorem HCPolySupport.HighContrast.Root.selectedRoundedPullbackEllipsoid_volume_ratio_le_of_near_terminal_ofReal {d : ℕ} [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) {r R : ℝ} (hr : 0 < r) (hR : 0 < R) (hnear : R < 400 * ↑d * r) : MeasureTheory.volume (selectedRoundedPullbackEllipsoid geom abar R) / MeasureTheory.volume (selectedRoundedPullbackEllipsoid geom abar r) ≤ ENNReal.ofReal ((4800 * ↑d * √↑d) ^ d)

ENNReal form of the selected near-terminal volume-ratio bound.

theorem HCPolySupport.HighContrast.Root.weightedGradNorm_selectedRoundedPullbackEllipsoid_le_outerCube {d : ℕ} [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) {r : ℝ} (hr : 0 < r) (b : CoeffField d) (F : Vec d → Vec d) : weightedGradNorm b (selectedRoundedPullbackEllipsoid geom abar r) F ≤ ENNReal.ofReal ((12 * √↑d) ^ d) ^ (1 / 2) * weightedGradNorm b (openCubeSet (originCube d (roundedEllipsoidOuterGeneration r hr))) F

Weighted energy on a selected pullback is controlled by its canonical outer origin cube.

theorem HCPolySupport.HighContrast.Root.weightedGradNorm_terminalCube_le_selectedRoundedPullbackEllipsoid {d : ℕ} [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) {R : ℝ} (hR : 0 < R) (b : CoeffField d) (F : Vec d → Vec d) : weightedGradNorm b (openCubeSet (originCube d (roundedEllipsoidTerminalGeneration R hR))) F ≤ ENNReal.ofReal ((1200 * ↑d) ^ d) ^ (1 / 2) * weightedGradNorm b (selectedRoundedPullbackEllipsoid geom abar R) F

Weighted energy on the terminal cube is controlled by the selected pullback at the terminal radius.

theorem HCPolySupport.HighContrast.Root.weightedGradNorm_selectedRoundedPullbackEllipsoid_le_of_near_terminal {d : ℕ} [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) {r R : ℝ} (hr : 0 < r) (hR : 0 < R) (hrR : r ≤ R) (hnear : R < 400 * ↑d * r) (b : CoeffField d) (F : Vec d → Vec d) : weightedGradNorm b (selectedRoundedPullbackEllipsoid geom abar r) F ≤ ENNReal.ofReal ((4800 * ↑d * √↑d) ^ d) ^ (1 / 2) * weightedGradNorm b (selectedRoundedPullbackEllipsoid geom abar R) F

The selected near-terminal branch closes directly by normalized-domain restriction.

theorem HCPolySupport.HighContrast.Root.weightedGradNorm_roundedCenteredCoefficientAtGeneration_le_of_finiteEnergy {d : ℕ} (l : ℤ) (hl : ↑(kZero d) ≤ l) (aPhysical : 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 l hl abar hS ↑↑aPhysical) (m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) aRounded) (h : ℤ) (hhm : h ≤ m) (H : ℝ) (hH : 0 ≤ H) (henergy : finiteCenteredCubeSolutionEnergy aRounded m u h ≤ H * finiteCenteredCubeSolutionEnergy aRounded m u m) : weightedGradNorm (roundedCenteredCoefficientAtGeneration l hl abar hS ↑↑aPhysical) (openCubeSet (originCube d h)) u.toH1.grad ≤ ENNReal.ofReal H * weightedGradNorm (roundedCenteredCoefficientAtGeneration l hl abar hS ↑↑aPhysical) (openCubeSet (originCube d m)) u.toH1.grad

A finite centered-energy estimate lifts to the selected-generation coefficient by the application's almost-everywhere identification.

theorem HCPolySupport.HighContrast.Root.weightedGradNorm_selectedRoundedCenteredPullback {d : ℕ} [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) {U : Set (Vec d)} (hU : MeasurableSet U) (a : CoeffField d) (F : Vec d → Vec d) : weightedGradNorm (fun (x : Vec d) => specBound (symmPart abar)⁻¹ • (a x - skewPart abar)) U F = weightedGradNorm (roundedCenteredCoefficientAtGeneration geom.generation ⋯ abar hS a) (matImage (geom.grid (symmPart abar))⁻¹ U) fun (y : Vec d) => matVecMul (geom.grid (symmPart abar)) (F (matVecMul (geom.grid (symmPart abar)) y))

The normalized skew-centered physical weighted norm is exactly the norm of its selected-generation coefficient and gradient pullback.