High-contrast homogenization: Provider.Regularity.PrintOrderRoundedGenerationResponseMax

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Spatial response rows at a selected rounded generation

The physical doubled response is maximized on cells of one admissible rounded grid. Its complete depth row is controlled by the same normalized-root weak error used by the quantitative certificate.

noncomputable def HCPolySupport.HighContrast.roundedNormalizedDoubledResponseMaxAtGeneration {d : ℕ} (l : ℤ) (a : CoeffSpace d) (abar : Mat d) (_hS : Matrix.PosDef (symmPart abar)) (k : ℤ) (w : Fin d → ℤ) : ℝ

The physical doubled response on one cell of a selected rounded grid, maximized over normalized primal and dual loads.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.exists_summable_roundedGenerationResponseMaxRow_le_scalarIdentityWeakError_sq {d : ℕ} [NeZero d] {l : ℤ} (hl : ↑(kZero d) ≤ l) (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) {s : ℝ} (hs : 0 < s) (hsHalf : s < 1 / 2) (M : ℤ) : ∃ (G : ℕ) (Z : ℕ → Finset (Fin d → ℤ)), 3 ^ ↑G ≤ 1 + 3 * (100 / 99 * witnessEccentricity (symmPart abar) * √↑d) ∧ (∀ (u : ℕ), ↑(Z u) = {w : Fin d → ℤ | adaptedCellCenter (roundedGrid l (symmPart abar)) (M - ↑u) w ∈ adaptedCell (roundedGrid l (symmPart abar)) M}) ∧ (∀ (u : ℕ), (Z u).card = 3 ^ (d * u)) ∧ (Summable fun (u : ℕ) => Book.Ch02.geometricWeight s 2 u * Book.Ch02.finsetSupReal (Z u) fun (w : Fin d → ℤ) => roundedNormalizedDoubledResponseMaxAtGeneration l a abar hS (M - ↑u) w) ∧ (∑' (u : ℕ), Book.Ch02.geometricWeight s 2 u * Book.Ch02.finsetSupReal (Z u) fun (w : Fin d → ℤ) => roundedNormalizedDoubledResponseMaxAtGeneration l a abar hS (M - ↑u) w) ≤ max 1 (6 * ↑d * √↑d * (101 / 100 * witnessEccentricity (symmPart abar))) * (Book.Ch02.geometricDiscount (1 - 2 * s) 1)⁻¹ * Real.rpow 3 (2 * s * ↑G) * scalarIdentityWeakError aRef s (M + ↑G) ^ 2

A selected rounded spatial row is controlled by one enclosing normalized-root weak error.