Documentation

LeanPool.HighContrastHomogenization.Provider.PolynomialHomogenization.Root.Corrector.C1BaseSlopeEnergyControl

High-contrast homogenization: #

Provider.PolynomialHomogenization.Root.Corrector.C1BaseSlopeEnergyControl

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

Energy control of the base exact slope #

The large-scale Lipschitz estimate controls the original solution on the base cube without a volume-ratio loss. Coefficient-energy Minkowski and exact minimality then control the finite affine comparison and its boundary slope.

source
theorem HCPolySupport.HighContrast.Root.exists_baseExactMinimizerSlopeEnergyConstants (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) :
∃ (K : ℝ) (c : ℝ), 0 < K ∧ c ∈ Set.Ioo 0 1 ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (delta : ℝ) (n m : ℕ), delta ∈ Set.Ioc 0 c → ScalarIdentityGoodTail a s delta ↑n → ∀ (hnm2 : n + 2 ≤ m) (u : Book.Ch03.CubeSolution (originCube d ↑m) a), euclideanNorm (finiteAffineExactMinimizer a ⋯ u) ≤ K * Book.Ch03.h1EnergyNormOnCube (originCube d ↑m) a u.toH1

The exact base-cube minimizing slope is bounded by the original outer solution energy with a dimension-only constant.