High-contrast homogenization: #
Provider.PolynomialHomogenization.Root.Corrector.C1FixedProjectionDecayCore
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Fixed-projection decay in a coefficient-energy space #
One exact minimizer is fixed at the base scale. At an observation scale its residual is split into the current minimizing residual and the telescoped finite-affine increments. Geometric excess decay absorbs the latter without changing the requested exponent.
theorem
HCPolySupport.HighContrast.Root.sqrt_normalizedEnergy_fixed_le_minimizer_add_slopeDifference
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{lam Lam : ℝ}
(hEll : IsEllipticFieldOn lam Lam U a)
(hvol : 0 < MeasureTheory.volume U)
(hvoltop : MeasureTheory.volume U ≠ ⊤)
(T : Vec d →ₗ[ℝ] ↥(HilbertVectorL2 U))
(J : ↥(HilbertVectorL2 U))
(bFixed bMin : Vec d)
:
√(normalizedLocalSymmetricEnergy hEll (J - T bFixed)) ≤ √(normalizedLocalSymmetricEnergy hEll (J - T bMin)) + √(normalizedLocalSymmetricEnergy hEll (T (bMin - bFixed)))
Comparison of a fixed competitor with the current minimizer.
theorem
HCPolySupport.HighContrast.Root.sqrt_normalizedEnergy_fixed_realRateDecay_of_incrementRows
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{lam Lam : ℝ}
(hEll : IsEllipticFieldOn lam Lam U a)
(hvol : 0 < MeasureTheory.volume U)
(hvoltop : MeasureTheory.volume U ≠ ⊤)
(T : Vec d →ₗ[ℝ] ↥(HilbertVectorL2 U))
(J : ↥(HilbertVectorL2 U))
(b : ℤ → Vec d)
{n q m : ℤ}
(hnq : n ≤ q)
(hqm : q ≤ m)
(eta A B terminalEnergy : ℝ)
(heta : 1 / 2 ≤ eta)
(hB : 0 ≤ B)
(hterminal : 0 ≤ terminalEnergy)
(hmin : √(normalizedLocalSymmetricEnergy hEll (J - T (b q))) ≤ A * Real.rpow 3 (-eta * (↑m - ↑q)) * terminalEnergy)
(hincrement :
∀ j ∈ Finset.Ico n q,
√(normalizedLocalSymmetricEnergy hEll (T (b (j + 1) - b j))) ≤ B * Real.rpow 3 ((↑q - ↑j) / 4) * Real.rpow 3 (-eta * (↑m - ↑j)) * terminalEnergy)
:
The same base-selected slope has the desired real-rate decay at every intermediate scale once the current-minimizer row and the propagated successive-increment rows have their bounds.