High-contrast homogenization: Provider.Regularity.PrintOrderRoundedGenerationOuterResponse #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Selected-generation rounded outer response at the printed order #
The order-generic response maximum theorem applies directly at
(1 + g) / 4 on every admissible rounded grid. This interface keeps both
the selected generation and the resulting g-dependent geometric discount.
theorem
HCPolySupport.HighContrast.exists_summable_roundedGenerationResponseMaxRow_le_printOrderPowerTail_sq
{d : ℕ}
[NeZero d]
{generation : ℤ}
(hl : ↑(kZero d) ≤ generation)
(a : CoeffSpace d)
(abar : Mat d)
(hS : Matrix.PosDef (symmPart abar))
(t : ℤ)
(aRef : Book.Ch03.CoeffFamily d)
(haRef :
∀ (R : TriadicCube d),
(aRef.coeffOn R).toCoeffField = affineCoefficient (Selection.normalizedRoot (symmPart abar)) ⋯
((normalizedCenteredCoeff a abar hS).coeffOn (Response.adaptedDomain ⋯ t)).toCoeffField)
{g amplitude kappa x : ℝ}
(hg : g ∈ Set.Ico 0 1)
(hAmplitude : 0 ≤ amplitude)
(hKappa : 0 < kappa)
(hTail : ScalarIdentityPowerTail aRef (printCertificateOrder g) amplitude kappa x)
(hx : 0 < x)
(M : ℤ)
(hActive : x ≤ 3 ^ M)
:
∃ (G : ℕ) (Z : ℕ → Finset (Fin d → ℤ)),
3 ^ ↑G ≤ 1 + 3 * (100 / 99 * witnessEccentricity (symmPart abar) * √↑d) ∧ (∀ (l : ℕ),
↑(Z l) = {w : Fin d → ℤ | adaptedCellCenter (roundedGrid generation (symmPart abar)) (M - ↑l) w ∈ adaptedCell (roundedGrid generation (symmPart abar)) M}) ∧ (∀ (l : ℕ), (Z l).card = 3 ^ (d * l)) ∧ (Summable fun (l : ℕ) =>
Book.Ch02.geometricWeight (printCertificateOrder g) 2 l * Book.Ch02.finsetSupReal (Z l) fun (w : Fin d → ℤ) =>
roundedNormalizedDoubledResponseMaxAtGeneration generation a abar hS (M - ↑l) w) ∧ (∑' (l : ℕ), Book.Ch02.geometricWeight (printCertificateOrder g) 2 l * Book.Ch02.finsetSupReal (Z l) fun (w : Fin d → ℤ) =>
roundedNormalizedDoubledResponseMaxAtGeneration generation a abar hS (M - ↑l) w) ≤ max 1 (6 * ↑d * √↑d * (101 / 100 * witnessEccentricity (symmPart abar))) * (Book.Ch02.geometricDiscount (1 - 2 * printCertificateOrder g) 1)⁻¹ * Real.rpow 3 (2 * printCertificateOrder g * ↑G) * (amplitude * (3 ^ M / x) ^ (-kappa)) ^ 2
The full rounded spatial-response row inherits a power tail at the printed order with the exact order-generic boundary-layer prefactor.