High-contrast homogenization: Provider.Regularity.PrintOrderRoundedGenerationGeometry #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Normalized-root fillings for a selected rounded grid #
All geometric estimates below are uniform over rounding generations above the admissibility threshold. The exact normalized-root cells fill a target cell of the selected grid with the same row constants as in the canonical case.
theorem
HCPolySupport.HighContrast.exists_coeffSpaceDoubledResponse_roundedGrid_le_rowMajorant
{d : ℕ}
[NeZero d]
{l : ℤ}
(hl : ↑(kZero d) ≤ l)
{m : Mat d}
(hm : Matrix.PosDef m)
(n j : ℤ)
(y : Vec d)
(a : CoeffSpace d)
(P Q : BlockVec d)
:
∃ (Z : ℤ → Finset (Fin d → ℤ)),
(∀ (r : ℤ),
↑(Z r) = Transport.fillingIndex (Selection.normalizedRoot m) n (adaptedCellTranslate (roundedGrid l m) j y) r) ∧ ∀ (B : ℤ → ℝ),
(∀ (r : ℤ), 0 ≤ B r) →
(∀ (u : ℕ),
∀ w ∈ Z (n - ↑u),
Book.Ch02.doubledResponseJ (Response.adaptedDomainAt ⋯ (n - ↑u) w)
(a.coeffOn (Response.adaptedDomainAt ⋯ (n - ↑u) w)) P Q ≤ B (n - ↑u)) →
(Summable fun (u : ℕ) =>
(if u = 0 then 1 else 6 * ↑d * √↑d * (101 / 100 * witnessEccentricity m) * 3 ^ (n - ↑u - j)) * B (n - ↑u)) →
Transport.coeffSpaceDoubledResponse (adaptedCellTranslate (roundedGrid l m) j y) a P Q ≤ ∑' (u : ℕ), (if u = 0 then 1 else 6 * ↑d * √↑d * (101 / 100 * witnessEccentricity m) * 3 ^ (n - ↑u - j)) * B (n - ↑u)
theorem
HCPolySupport.HighContrast.exists_outerCellIndices_enclosed_by_normalizedRoot_at_generation
{d : ℕ}
[NeZero d]
{l : ℤ}
(hl : ↑(kZero d) ≤ l)
{m : Mat d}
(hm : Matrix.PosDef m)
(M : ℤ)
:
∃ (G : ℕ) (Z : ℕ → Finset (Fin d → ℤ)),
3 ^ ↑G ≤ 1 + 3 * (100 / 99 * witnessEccentricity m * √↑d) ∧ (∀ (u : ℕ),
↑(Z u) = {w : Fin d → ℤ | adaptedCellCenter (roundedGrid l m) (M - ↑u) w ∈ adaptedCell (roundedGrid l m) M}) ∧ (∀ (u : ℕ), (Z u).card = 3 ^ (d * u)) ∧ ∀ (u : ℕ),
∀ w ∈ Z u,
adaptedCellTranslate (roundedGrid l m) (M - ↑u) (adaptedCellCenter (roundedGrid l m) (M - ↑u) w) ⊆
adaptedCell (Selection.normalizedRoot m) (M + ↑G)
theorem
HCPolySupport.HighContrast.translateCube_mem_descendants_of_generation_filling
{d : ℕ}
[NeZero d]
{l : ℤ}
{m : Mat d}
(hm : Matrix.PosDef m)
{n j M : ℤ}
(hnM : n ≤ M)
{y : Vec d}
{Z : ℤ → Finset (Fin d → ℤ)}
(hZ :
∀ (r : ℤ),
↑(Z r) = Transport.fillingIndex (Selection.normalizedRoot m) n (adaptedCellTranslate (roundedGrid l m) j y) r)
(hEnclose : adaptedCellTranslate (roundedGrid l m) j y ⊆ adaptedCell (Selection.normalizedRoot m) M)
{r : ℤ}
{w : Fin d → ℤ}
(hw : w ∈ Z r)
: