High-contrast homogenization: Provider.Regularity.PrintOrderRoundedGenerationUniformRecurrence #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Uniform finite recurrence for one selected rounded geometry #
The rounded generation and all analytic constants are selected before the coefficient sample. The stochastic certificate enters only through the printed-order weak-error row.
theorem
HCPolySupport.HighContrast.exists_printOrderRoundedGenerationUniformFiniteRecurrenceConstant
(d : ℕ)
[NeZero d]
(g : ℝ)
(geom : RoundedGenerationAnalyticGeometry d)
(hg : g ∈ Set.Ico 0 1)
(hdual : PrintOrderRoundedReferenceDualRegularityAtGeneration d g geom.generation)
:
∃ (C : ℝ),
1 ≤ C ∧ ∀ (a : CoeffSpace d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (aRounded : Book.Ch03.CoeffFamily d),
(∀ (Q : TriadicCube d), (aRounded.coeffOn Q).toCoeffField = ↑↑(geom.centeredCoeffSpace abar hS a)) →
∀ (n m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) aRounded),
n ≤ m →
RoundedGenerationSpatialGoodMaxOnInterval geom.generation a abar hS (printCertificateOrder g) 1 n m →
∀ h ∈ Finset.Icc n m,
finiteCenteredCubeSolutionEnergy aRounded m u h ≤ C * finiteCenteredCubeSolutionEnergy aRounded m u m + C * ∑ j ∈ Finset.Ioc h m,
roundedGenerationSpatialWeakError geom.generation a abar hS (printCertificateOrder g) j * finiteCenteredCubeSolutionEnergy aRounded m u j
At a fixed selected geometry, one constant controls the finite recurrence for every centered coefficient realization.
theorem
HCPolySupport.HighContrast.finiteCenteredEnergy_le_of_roundedGenerationGoodTail
{d : ℕ}
{generation : ℤ}
{a : CoeffSpace d}
{abar : Mat d}
{hS : Matrix.PosDef (symmPart abar)}
{s : ℝ}
{aRounded : Book.Ch03.CoeffFamily d}
{C : ℝ}
(hC : 1 ≤ C)
{n m : ℤ}
(hnm : n ≤ m)
(u : Book.Ch03.CubeSolution (originCube d m) aRounded)
(hrecurrence :
∀ q ∈ Finset.Icc n m,
finiteCenteredCubeSolutionEnergy aRounded m u q ≤ C * finiteCenteredCubeSolutionEnergy aRounded m u m + C * ∑ j ∈ Finset.Ioc q m,
roundedGenerationSpatialWeakError generation a abar hS s j * finiteCenteredCubeSolutionEnergy aRounded m u j)
(hTail : RoundedGenerationSpatialGoodTailOnInterval generation a abar hS s (2 * C)⁻¹ n m)
(h : ℤ)
:
h ∈ Finset.Icc n m →
finiteCenteredCubeSolutionEnergy aRounded m u h ≤ 2 * C * finiteCenteredCubeSolutionEnergy aRounded m u m
A finite recurrence driven by a selected-generation row closes under the summable good-tail bound at that same generation and order.