High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Corrector.C1FixedProjectionIncrement

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

Propagation of consecutive exact-minimizer increments

The difference of two consecutive residuals is the finite affine solution with the difference slope. Its coefficient energy at the smaller scale is therefore bounded by the two minimizing residual energies, and the available fixed-boundary growth theorem propagates that bound to any later observation scale.

theorem HCPolySupport.HighContrast.Root.normalizedLocalSymmetricEnergy_neg_increment {d : ℕ} {U : Set (Vec d)} {b : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U b) (F : ↥(HilbertVectorL2 U)) : normalizedLocalSymmetricEnergy hEll (-F) = normalizedLocalSymmetricEnergy hEll F

theorem HCPolySupport.HighContrast.Root.sqrt_normalizedLocalSymmetricEnergy_neg_increment {d : ℕ} {U : Set (Vec d)} {b : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U b) (F : ↥(HilbertVectorL2 U)) : √(normalizedLocalSymmetricEnergy hEll (-F)) = √(normalizedLocalSymmetricEnergy hEll F)

theorem HCPolySupport.HighContrast.Root.finiteAffineDifferenceEnergy_le_exactResiduals {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) {j m : ℤ} (hjm : j ≤ m) (u : Book.Ch03.CubeSolution (originCube d m) a) (b0 b1 : Vec d) (hb0 : (weightedGradNorm (a.coeffOn (originCube d j)).toCoeffField (openCubeSet (originCube d j)) fun (x : Vec d) => u.toH1.grad x - (finiteAffineSolution a m b0).toH1.grad x) = finiteAffineGradientExcess a j m u) (hb1j : Book.Ch03.h1EnergyNormOnCube (originCube d j) a (finiteAffineGradientResidual a hjm u b1).toH1 ≤ ↑(3 ^ d) * (finiteAffineGradientExcess a (j + 1) m u).toReal) : finiteCenteredCubeSolutionEnergy a m (finiteAffineCubeSolution a m (b0 - b1)) j ≤ (finiteAffineGradientExcess a j m u).toReal + ↑(3 ^ d) * (finiteAffineGradientExcess a (j + 1) m u).toReal

At the smaller of two consecutive minimizer scales, the finite affine increment has energy bounded by the two residual energies.

theorem HCPolySupport.HighContrast.Root.residualEnergy_at_predecessor_le_exactSuccessor {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) {j m : ℤ} (hjm : j + 1 ≤ m) (u : Book.Ch03.CubeSolution (originCube d m) a) (b1 : Vec d) (hb1 : (weightedGradNorm (a.coeffOn (originCube d (j + 1))).toCoeffField (openCubeSet (originCube d (j + 1))) fun (x : Vec d) => u.toH1.grad x - (finiteAffineSolution a m b1).toH1.grad x) = finiteAffineGradientExcess a (j + 1) m u) : Book.Ch03.h1EnergyNormOnCube (originCube d j) a (finiteAffineGradientResidual a ⋯ u b1).toH1 ≤ ↑(3 ^ d) * (finiteAffineGradientExcess a (j + 1) m u).toReal

The previous residual at scale j+1, restricted to its centered child, has the standard normalized-volume loss.

theorem HCPolySupport.HighContrast.Root.finiteAffineExactMinimizerIncrementEnergy_le {d : ℕ} [NeZero d] (s c Cgrow : ℝ) (hgrowth : ∀ (a : Book.Ch02.TriadicCoeffFamily d) (delta : ℝ) (n m : ℤ), n < m → delta ∈ Set.Ioc 0 c → ScalarIdentityGoodMaxOnInterval a s delta n m → ∀ j ∈ Finset.Icc n m, ∀ k ∈ Finset.Icc n m, j ≤ k → ∀ (b : Vec d), finiteCenteredCubeSolutionEnergy a m (finiteAffineCubeSolution a m b) k ≤ Cgrow ^ 2 * Real.rpow 3 (↑(k - j).toNat / 4) * finiteCenteredCubeSolutionEnergy a m (finiteAffineCubeSolution a m b) j) (a : Book.Ch02.TriadicCoeffFamily d) (delta : ℝ) {n j q m : ℤ} (hnm : n < m) (hdelta : delta ∈ Set.Ioc 0 c) (hgood : ScalarIdentityGoodMaxOnInterval a s delta n m) (hj : j ∈ Finset.Ico n q) (hqm : q ≤ m) (u : Book.Ch03.CubeSolution (originCube d m) a) : have b0 := finiteAffineExactMinimizer a ⋯ u; have b1 := finiteAffineExactMinimizer a ⋯ u; finiteCenteredCubeSolutionEnergy a m (finiteAffineCubeSolution a m (b0 - b1)) q ≤ Cgrow ^ 2 * Real.rpow 3 ((↑q - ↑j) / 4) * ((finiteAffineGradientExcess a j m u).toReal + ↑(3 ^ d) * (finiteAffineGradientExcess a (j + 1) m u).toReal)

A consecutive exact-minimizer increment propagated to an observation scale carries precisely the quarter-power growth from the available theorem.