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

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

Response Bounds for Chapter 2.5 HCPolySupport Error

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

theorem HCPolySupport.Book.Ch02.CoeffOn.RestrictsTo.transpose {d : ℕ} {U V : Domain d} {a : CoeffOn U} {b : CoeffOn V} (h : a.RestrictsTo b) : a.transpose.RestrictsTo b.transpose

noncomputable def HCPolySupport.Book.Ch02.descendantsDomainPartition {d : ℕ} (Q : TriadicCube d) (j : ℕ) : DomainPartition (cubeDomain Q)

The public partition of an open triadic cube into descendants at a fixed depth.

Equations

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

theorem HCPolySupport.Book.Ch02.descendantsDomainPartition_weightedAverage {d : ℕ} (Q : TriadicCube d) (j : ℕ) (F : TriadicCube d → ℝ) : ((descendantsDomainPartition Q j).weightedAverage fun (i : (descendantsDomainPartition Q j).Cell) => F ↑i) = descendantsAverage Q j F

theorem HCPolySupport.Book.Ch02.descendantsDomainPartition_weightedMatAverage {d : ℕ} (Q : TriadicCube d) (j : ℕ) (F : TriadicCube d → Mat d) : ((descendantsDomainPartition Q j).weightedMatAverage fun (i : (descendantsDomainPartition Q j).Cell) => F ↑i) = descendantsAverageMat Q j F

The public descendant partition's weighted matrix average is the entrywise descendant average.

theorem HCPolySupport.Book.Ch02.descendantsDomainPartition_weightedBlockAverage {d : ℕ} (Q : TriadicCube d) (j : ℕ) (F : TriadicCube d → BlockMat d) : ((descendantsDomainPartition Q j).weightedBlockAverage fun (i : (descendantsDomainPartition Q j).Cell) => F ↑i) = descendantsAverageBlockMat Q j F

The public descendant partition's weighted block-matrix average is the entrywise descendant average.

theorem HCPolySupport.Book.Ch02.doubledResponseJ_nonneg {d : ℕ} (U : Domain d) (a : CoeffOn U) (P Q : BlockVec d) : 0 ≤ doubledResponseJ U a P Q

theorem HCPolySupport.Book.Ch02.normalizedBlockResponseMax_nonneg {d : ℕ} (Q : TriadicCube d) (a : TriadicCoeffFamily d) (a0 : Mat d) : 0 ≤ normalizedBlockResponseMax Q a a0

theorem HCPolySupport.Book.Ch02.normalizedBlockResponseValueSet_nonempty {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) (a0 : Mat d) : (normalizedBlockResponseValueSet Q a a0).Nonempty

noncomputable def HCPolySupport.Book.Ch02.normalizedBlockResponseUniformBound {d : ℕ} (Q : TriadicCube d) (a : TriadicCoeffFamily d) (a0 : Mat d) : ℝ

A uniform deterministic bound for normalized block response on descendants of Q, depending only on the root cube coefficient object and on a0.

Equations

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

theorem HCPolySupport.Book.Ch02.normalizedBlockResponseValueSet_bddAbove_of_mem_descendantsAtScale {d : ℕ} (a : TriadicCoeffFamily d) {Q R : TriadicCube d} {k : ℤ} (a0 : Mat d) (hR : R ∈ descendantsAtScale Q k) : BddAbove (normalizedBlockResponseValueSet R a a0)

theorem HCPolySupport.Book.Ch02.normalizedBlockResponseMax_le_uniform_of_mem_descendantsAtScale {d : ℕ} [NeZero d] (a : TriadicCoeffFamily d) {Q R : TriadicCube d} {k : ℤ} (a0 : Mat d) (hR : R ∈ descendantsAtScale Q k) : normalizedBlockResponseMax R a a0 ≤ normalizedBlockResponseUniformBound Q a a0

theorem HCPolySupport.Book.Ch02.normalizedBlockResponseMax_le_maxDescendantNormalizedBlockResponseAtScale {d : ℕ} {Q R : TriadicCube d} {k : ℤ} (a : TriadicCoeffFamily d) (a0 : Mat d) (hR : R ∈ descendantsAtScale Q k) : normalizedBlockResponseMax R a a0 ≤ maxDescendantNormalizedBlockResponseAtScale Q k a a0

theorem HCPolySupport.Book.Ch02.maxDescendantNormalizedBlockResponseAtScale_le_of_mem_descendantsAtScale {d : ℕ} {Q R : TriadicCube d} {k l : ℤ} (a : TriadicCoeffFamily d) (a0 : Mat d) (hR : R ∈ descendantsAtScale Q k) (hl : l ≤ R.scale) : maxDescendantNormalizedBlockResponseAtScale R l a a0 ≤ maxDescendantNormalizedBlockResponseAtScale Q l a a0

theorem HCPolySupport.Book.Ch02.normalizedBlockResponseMax_le_maxDescendantNormalizedBlockResponseAtScale_of_le {d : ℕ} [NeZero d] (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) (a : TriadicCoeffFamily d) (a0 : Mat d) : normalizedBlockResponseMax Q a a0 ≤ maxDescendantNormalizedBlockResponseAtScale Q k a a0

theorem HCPolySupport.Book.Ch02.maxDescendantNormalizedBlockResponseAtScale_nonneg {d : ℕ} (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) (a : TriadicCoeffFamily d) (a0 : Mat d) : 0 ≤ maxDescendantNormalizedBlockResponseAtScale Q k a a0

theorem HCPolySupport.Book.Ch02.maxDescendantNormalizedBlockResponseAtScale_le_uniform {d : ℕ} [NeZero d] (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) (a : TriadicCoeffFamily d) (a0 : Mat d) : maxDescendantNormalizedBlockResponseAtScale Q k a a0 ≤ normalizedBlockResponseUniformBound Q a a0

theorem HCPolySupport.Book.Ch02.maxDescendantNormalizedBlockResponseAtScale_le_of_le {d : ℕ} [NeZero d] (Q : TriadicCube d) {k l : ℤ} (hkl : k ≤ l) (hlQ : l ≤ Q.scale) (a : TriadicCoeffFamily d) (a0 : Mat d) : maxDescendantNormalizedBlockResponseAtScale Q l a a0 ≤ maxDescendantNormalizedBlockResponseAtScale Q k a a0

theorem HCPolySupport.Book.Ch02.scaleResponseAtScale_infinity_nonneg {d : ℕ} (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) (a : TriadicCoeffFamily d) (a0 : Mat d) : 0 ≤ scaleResponseAtScale Q k MultiscaleExponent.infinity a a0

theorem HCPolySupport.Book.Ch02.scaleResponseAtScale_infinity_le_of_mem_descendantsAtScale {d : ℕ} {Q R : TriadicCube d} {k l : ℤ} (a : TriadicCoeffFamily d) (a0 : Mat d) (hR : R ∈ descendantsAtScale Q k) (hl : l ≤ R.scale) : scaleResponseAtScale R l MultiscaleExponent.infinity a a0 ≤ scaleResponseAtScale Q l MultiscaleExponent.infinity a a0

theorem HCPolySupport.Book.Ch02.scaleResponseAtScale_infinity_le_of_le {d : ℕ} [NeZero d] (Q : TriadicCube d) {k l : ℤ} (hkl : k ≤ l) (hlQ : l ≤ Q.scale) (a : TriadicCoeffFamily d) (a0 : Mat d) : scaleResponseAtScale Q l MultiscaleExponent.infinity a a0 ≤ scaleResponseAtScale Q k MultiscaleExponent.infinity a a0

theorem HCPolySupport.Book.Ch02.scaleResponseAtScale_infinity_self_le {d : ℕ} [NeZero d] (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) (a : TriadicCoeffFamily d) (a0 : Mat d) : scaleResponseAtScale Q Q.scale MultiscaleExponent.infinity a a0 ≤ scaleResponseAtScale Q k MultiscaleExponent.infinity a a0

theorem HCPolySupport.Book.Ch02.scaleResponseAtScale_infinity_le_uniform {d : ℕ} [NeZero d] (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) (a : TriadicCoeffFamily d) (a0 : Mat d) : scaleResponseAtScale Q k MultiscaleExponent.infinity a a0 ≤ (normalizedBlockResponseUniformBound Q a a0).rpow (1 / 2)