High-contrast homogenization: Provider.Regularity.PrintOrderRoundedGenerationResponseScale #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Selected-generation rounded response scale at the printed fractional order #
The boundary-layer discount and affine multiplier already used by the canonical response row apply uniformly to every admissible rounded generation.
theorem
HCPolySupport.HighContrast.exists_summable_roundedGenerationResponseMaxRow_le_printOrderAffineTail_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) ≤ (printOrderRoundedResponseAffineConstant d g * witnessEccentricity (symmPart abar) * (amplitude * (3 ^ M / x) ^ (-kappa))) ^ 2
The outer response row is controlled by the printed-order affine loss.
theorem
HCPolySupport.HighContrast.exists_summable_roundedGenerationResponseMaxRow_le_printOrderEffectiveScale_powerTail_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 :
roundedAffineEffectiveScale (printOrderRoundedResponseAffineConstant d g)
(specBound (symmPart abar) * specBound (symmPart abar)⁻¹) kappa 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) ≤ (amplitude * (3 ^ M / roundedAffineEffectiveScale (printOrderRoundedResponseAffineConstant d g)
(specBound (symmPart abar) * specBound (symmPart abar)⁻¹) kappa x) ^ (-kappa)) ^ 2
The printed-order affine scale absorbs the rounded response loss.