Coarse-graining support: Support.Book.Ch02.Theorems.HomogenizationError.Public

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Public Chapter 2.5 HCPolySupport Error Package

This file proves the public basic properties of the homogenization error \mathcal E_{s,\infty,1} from Sec. 2.5.

theorem HCPolySupport.Book.Ch02.homogenizationErrorTheory (d : ℕ) [NeZero d] : HomogenizationErrorTheory d

Aggregate unconditional public theorem package for the Sec. 2.5 homogenization-error facts currently needed downstream.