High-contrast homogenization: Provider.Regularity.MixedOrderFiniteRecurrenceCore #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Finite energy recurrence over an independent response row #
The finite sequence argument only uses a nonnegative forcing row, its pointwise unit bound, and four analytic estimates. In particular, the order used to construct those analytic estimates is not part of the recurrence bookkeeping.
theorem
HCPolySupport.HighContrast.exists_mixedResponseFiniteLipschitzEnergyRecurrenceConstant
(d N : ℕ)
(hN : 0 < N)
(Cstep : ℝ)
(hCstep : 0 ≤ Cstep)
(Cc : ℝ)
(hCc : 0 < Cc)
(Ct : ℝ)
(hCt : 0 < Ct)
(Ce : ℝ)
(hCe : 0 < Ce)
:
∃ (C : ℝ),
1 ≤ C ∧ ∀ (aRounded : Book.Ch03.CoeffFamily d) (R : ℤ → ℝ),
(∀ (j : ℤ), 0 ≤ R j) →
(∀ (m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) aRounded),
∀ k ≤ m,
FiniteLipschitzCoreInternal.finiteLipschitzAffineErrorRow aRounded m u (k - ↑N) ≤ 1 / 8 * FiniteLipschitzCoreInternal.finiteLipschitzAffineErrorRow aRounded m u k + Cstep * R k * FiniteLipschitzCoreInternal.finiteLipschitzEnergyRow aRounded m u k) →
(∀ (k : ℤ) (u : Book.Ch03.CubeSolution (originCube d k) aRounded) (c : ℝ) (e : Vec d),
R k ≤ 1 →
Book.Ch03.h1EnergyNormOnCube (originCube d (k - 2)) aRounded
(finiteCubeSolutionRestriction aRounded ⋯ u).toH1 ≤ Cc * (normalizedAffineCandidateError (originCube d k) u.toH1.toFun c e + euclideanNorm e)) →
(∀ (m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) aRounded),
R m ≤ 1 →
euclideanNorm (FiniteLipschitzCoreInternal.finiteLipschitzBestSlope aRounded m u m) ≤ Ct * FiniteLipschitzCoreInternal.finiteLipschitzEnergyRow aRounded m u m) →
(∀ (m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) aRounded),
∀ k ≤ m,
R k ≤ 1 →
FiniteLipschitzCoreInternal.finiteLipschitzAffineErrorRow aRounded m u k ≤ Ce * FiniteLipschitzCoreInternal.finiteLipschitzEnergyRow aRounded m u k) →
∀ (n m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) aRounded),
n ≤ m →
(∀ k ∈ Finset.Icc n m, R k ≤ 1) →
∀ h ∈ Finset.Icc n m,
FiniteLipschitzCoreInternal.finiteLipschitzEnergyRow aRounded m u h ≤ C * FiniteLipschitzCoreInternal.finiteLipschitzEnergyRow aRounded m u m + C * ∑ j ∈ Finset.Ioc h m,
R j * FiniteLipschitzCoreInternal.finiteLipschitzEnergyRow aRounded m u j
A fixed-step affine recurrence and three response-row analytic estimates imply the finite energy recurrence, without assigning a fractional order to the response row.