Coarse-graining support: Support.Book.Ch02.Theorems.HomogenizationErrorDefinitions #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Public Chapter 2.5 HCPolySupport-Error Theorem Surface #
This file records the note-facing basic properties of
\mathcal E_{s,\infty,1}. The coefficient field is the public
TriadicCoeffFamily, so ellipticity and cube compatibility are a.e. facts.
structure
HCPolySupport.Book.Ch02.HomogenizationErrorInfinityOneBasicTheory
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : TriadicCoeffFamily d)
(a0 : Mat d)
:
Public theorem package for
l.multiscale.homogenization.error.basic.definitions, in the downstream
p = infinity, q = 1 form used by the Chapter 3 coarse estimates.
- scaleResponse_nonneg {k : ℤ} : k ≤ Q.scale → 0 ≤ scaleResponseAtScale Q k MultiscaleExponent.infinity a a0
- error_nonneg {s : ℝ} : 0 < s → 0 ≤ HomogenizationErrorOnCube Q s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0
- oneCube_le_error {s : ℝ} : 0 < s → scaleResponseAtScale Q Q.scale MultiscaleExponent.infinity a a0 ≤ HomogenizationErrorOnCube Q s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0
- error_antitone {t s : ℝ} : 0 < t → t < s → HomogenizationErrorOnCube Q s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0 ≤ HomogenizationErrorOnCube Q t MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0
- descendant_error_le {R : TriadicCube d} {k : ℤ} {s : ℝ} : R ∈ descendantsAtScale Q k → 0 < s → HomogenizationErrorOnCube R s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0 ≤ Real.rpow 3 (s * ↑(Q.scale - k).toNat) * HomogenizationErrorOnCube Q s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0
- descendants_error_sup_le {k : ℤ} {s : ℝ} : k ≤ Q.scale → 0 < s → (finsetSupReal (descendantsAtScale Q k) fun (R : TriadicCube d) => HomogenizationErrorOnCube R s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0) ≤ Real.rpow 3 (s * ↑(Q.scale - k).toNat) * HomogenizationErrorOnCube Q s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0
Instances For
Aggregate public theorem package for the homogenization-error part of Sec. 2.5.
- infinity_one_basic (Q : TriadicCube d) (a : TriadicCoeffFamily d) (a0 : Mat d) : HomogenizationErrorInfinityOneBasicTheory Q a a0