Coarse-graining support: Support.Book.Ch02.ParentTruncatedHomogenizationError

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

noncomputable def HCPolySupport.Book.Ch02.normalizedBlockResponseESetOnCube {d : ℕ} (Q : TriadicCube d) (a : CoeffOn (cubeDomain Q)) (a0 : Mat d) : Set ENNReal

Doubled responses converted to extended nonnegative reals, on unit block vectors transformed by the inverse square root and square root of the constant block matrix.

Equations

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

noncomputable def HCPolySupport.Book.Ch02.normalizedBlockResponseEMaxOnCube {d : ℕ} (Q : TriadicCube d) (a : CoeffOn (cubeDomain Q)) (a0 : Mat d) : ENNReal

The extended nonnegative supremum of the constant-matrix-normalized doubled responses.

Equations

• HCPolySupport.Book.Ch02.normalizedBlockResponseEMaxOnCube Q a a0 = sSup (HCPolySupport.Book.Ch02.normalizedBlockResponseESetOnCube Q a a0)

noncomputable def HCPolySupport.Book.Ch02.parentMaxNormalizedBlockResponseAtScale {d : ℕ} (Q : TriadicCube d) (k : ℤ) (hk : k ≤ Q.scale) (a : CoeffOn (cubeDomain Q)) (a0 : Mat d) : ENNReal

The maximum normalized doubled response over scale-k descendants, using the parent coefficient restricted to each subcube.

Equations

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

noncomputable def HCPolySupport.Book.Ch02.homogenizationErrorGeometricEWeight (s q : ℝ) (j : ℕ) : ENNReal

The extended nonnegative geometric weight formed from 1 - 3 ^ (-s*q) and 3 ^ (-s*q*j).

Equations

• HCPolySupport.Book.Ch02.homogenizationErrorGeometricEWeight s q j = ENNReal.ofReal (1 - Real.rpow 3 (-s * q)) * ENNReal.ofReal (Real.rpow 3 (-s * q * ↑j))

noncomputable def HCPolySupport.Book.Ch02.parentTruncatedHomogenizationErrorInfinityFinite {d : ℕ} (Q : TriadicCube d) (n : ℤ) (hn : n ≤ Q.scale) (a : CoeffOn (cubeDomain Q)) (a0 : Mat d) (s q : ℝ) : ENNReal

The weighted sum of maximal descendant responses below n to power q/2, raised to 1/q in the extended nonnegative reals.

Equations

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

noncomputable def HCPolySupport.Book.Ch02.parentTruncatedHomogenizationErrorInfinityOneScalar {d : ℕ} (Q : TriadicCube d) (n : ℤ) (hn : n ≤ Q.scale) (a : CoeffOn (cubeDomain Q)) (sigma0 : ℝ) (_hsigma0 : 0 < sigma0) (s : ↑FractionalOrder) : ENNReal

The source-order, scalar-comparator, q = 1 truncated response error.

At each physical scale it maximizes over descendants of the one parent coefficient, and only then performs the weighted scale sum.

Equations

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

noncomputable def HCPolySupport.Book.Ch02.parentTruncatedHomogenizationErrorInfinityTwoScalar {d : ℕ} (Q : TriadicCube d) (n : ℤ) (hn : n ≤ Q.scale) (a : CoeffOn (cubeDomain Q)) (sigma0 : ℝ) (_hsigma0 : 0 < sigma0) (s : ↑FractionalOrder) : ENNReal

The source-order, scalar-comparator, q = 2 truncated response error.

Equations

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

noncomputable def HCPolySupport.Book.Ch02.parentTruncatedNormalizedBlockResponseScalarEMaxAtScale {d : ℕ} (Q : TriadicCube d) (k : ℤ) (hk : k ≤ Q.scale) (a : CoeffOn (cubeDomain Q)) (sigma0 : ℝ) (_hsigma0 : 0 < sigma0) : ENNReal

The canonical scalar-comparator parent response maximum at physical scale k. This is the finite supremum over the descendants of Q at that scale, using literal restrictions of the one parent coefficient.

Equations

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

theorem HCPolySupport.Book.Ch02.parentTruncatedHomogenizationErrorInfinityOneScalar_eq_tsum {d : ℕ} (Q : TriadicCube d) (n : ℤ) (hn : n ≤ Q.scale) (a : CoeffOn (cubeDomain Q)) (sigma0 : ℝ) (hsigma0 : 0 < sigma0) (s : ↑FractionalOrder) : parentTruncatedHomogenizationErrorInfinityOneScalar Q n hn a sigma0 hsigma0 s = ∑' (j : ℕ), ENNReal.ofReal (1 - Real.rpow 3 (-↑s)) * ENNReal.ofReal (Real.rpow 3 (-↑s * ↑j)) * parentTruncatedNormalizedBlockResponseScalarEMaxAtScale Q (n - ↑j) ⋯ a sigma0 hsigma0 ^ (1 / 2)

Exact series characterization of the canonical scalar q = 1 truncated parent error. This only unfolds its frozen definition.

theorem HCPolySupport.Book.Ch02.parentTruncatedHomogenizationErrorInfinityTwoScalar_eq_tsum {d : ℕ} (Q : TriadicCube d) (n : ℤ) (hn : n ≤ Q.scale) (a : CoeffOn (cubeDomain Q)) (sigma0 : ℝ) (hsigma0 : 0 < sigma0) (s : ↑FractionalOrder) : parentTruncatedHomogenizationErrorInfinityTwoScalar Q n hn a sigma0 hsigma0 s = (∑' (j : ℕ), ENNReal.ofReal (1 - Real.rpow 3 (-↑s * 2)) * ENNReal.ofReal (Real.rpow 3 (-↑s * 2 * ↑j)) * parentTruncatedNormalizedBlockResponseScalarEMaxAtScale Q (n - ↑j) ⋯ a sigma0 hsigma0) ^ (1 / 2)

Exact series characterization of the canonical scalar q = 2 truncated parent error. This only unfolds its frozen definition.

noncomputable def HCPolySupport.Book.Ch02.normalizedBlockResponseEUpperBoundOnCube {d : ℕ} (Q : TriadicCube d) (a : CoeffOn (cubeDomain Q)) (a0 : Mat d) : ENNReal

The ellipticity-based expression combining row bounds for the constant block matrix's square root and inverse square root, used to bound the normalized response.

Equations

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

noncomputable def HCPolySupport.Book.Ch02.normalizedBlockResponseScalarEValueSetOnCube {d : ℕ} (Q : TriadicCube d) (a : CoeffOn (cubeDomain Q)) (sigma0 : ℝ) (_hsigma0 : 0 < sigma0) : Set ENNReal

The ℝ≥0∞-valued unit-sphere response values for the positive scalar comparator sigma0 I on one cube.

This is a scalar-facing wrapper around the private matrix implementation. In particular, it deliberately exposes a supremum API below, rather than claiming that a maximizing vector has been constructed.

Equations

• HCPolySupport.Book.Ch02.normalizedBlockResponseScalarEValueSetOnCube Q a sigma0 _hsigma0 = HCPolySupport.Book.Ch02.normalizedBlockResponseESetOnCube Q a (HCPolySupport.scalarMatrix sigma0)

noncomputable def HCPolySupport.Book.Ch02.normalizedBlockResponseScalarEMaxOnCube {d : ℕ} (Q : TriadicCube d) (a : CoeffOn (cubeDomain Q)) (sigma0 : ℝ) (hsigma0 : 0 < sigma0) : ENNReal

The one-cube scalar-comparator response supremum. This definition does not assert that the supremum is attained.

Equations

• HCPolySupport.Book.Ch02.normalizedBlockResponseScalarEMaxOnCube Q a sigma0 hsigma0 = sSup (HCPolySupport.Book.Ch02.normalizedBlockResponseScalarEValueSetOnCube Q a sigma0 hsigma0)

theorem HCPolySupport.Book.Ch02.mem_normalizedBlockResponseScalarEValueSetOnCube_iff {d : ℕ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {sigma0 : ℝ} {hsigma0 : 0 < sigma0} {y : ENNReal} : y ∈ normalizedBlockResponseScalarEValueSetOnCube Q a sigma0 hsigma0 ↔ ∃ (e : FullBlockVec d), fullBlockVecNormSq e = 1 ∧ y = ENNReal.ofReal (doubledResponseJ (cubeDomain Q) a (ofFullBlockVec (Matrix.mulVec (constantFullBlockMatrixInvSqrt (scalarMatrix sigma0)) e)) (ofFullBlockVec (Matrix.mulVec (constantFullBlockMatrixSqrt (scalarMatrix sigma0)) e)))

Membership in the scalar response value set is exactly the nonnegative extended-real encoding of a unit-sphere doubled response.

theorem HCPolySupport.Book.Ch02.normalizedBlockResponseScalarEValueSetOnCube_ne_top {d : ℕ} {Q : TriadicCube d} {a : CoeffOn (cubeDomain Q)} {sigma0 : ℝ} {hsigma0 : 0 < sigma0} {y : ENNReal} (hy : y ∈ normalizedBlockResponseScalarEValueSetOnCube Q a sigma0 hsigma0) : y ≠ ⊤

Every scalar response value is finite, as follows from its ENNReal.ofReal representation.

theorem HCPolySupport.Book.Ch02.normalizedBlockResponseScalar_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffOn (cubeDomain Q)) (sigma0 : ℝ) (_hsigma0 : 0 < sigma0) (e : FullBlockVec d) (_he : fullBlockVecNormSq e = 1) : 0 ≤ doubledResponseJ (cubeDomain Q) a (ofFullBlockVec (Matrix.mulVec (constantFullBlockMatrixInvSqrt (scalarMatrix sigma0)) e)) (ofFullBlockVec (Matrix.mulVec (constantFullBlockMatrixSqrt (scalarMatrix sigma0)) e))

The real response encoded by the scalar value set is nonnegative.

theorem HCPolySupport.Book.Ch02.normalizedBlockResponseScalarEValueSetOnCube_nonempty {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffOn (cubeDomain Q)) (sigma0 : ℝ) (hsigma0 : 0 < sigma0) : (normalizedBlockResponseScalarEValueSetOnCube Q a sigma0 hsigma0).Nonempty

The scalar response value set is nonempty.

theorem HCPolySupport.Book.Ch02.normalizedBlockResponseScalarEValueSetOnCube_bddAbove {d : ℕ} (Q : TriadicCube d) (a : CoeffOn (cubeDomain Q)) (sigma0 : ℝ) (hsigma0 : 0 < sigma0) : BddAbove (normalizedBlockResponseScalarEValueSetOnCube Q a sigma0 hsigma0)

The scalar response value set is bounded above in ℝ≥0∞.

theorem HCPolySupport.Book.Ch02.normalizedBlockResponseScalarEValueSetOnCube_le_eMax {d : ℕ} (Q : TriadicCube d) (a : CoeffOn (cubeDomain Q)) (sigma0 : ℝ) (hsigma0 : 0 < sigma0) {y : ENNReal} (hy : y ∈ normalizedBlockResponseScalarEValueSetOnCube Q a sigma0 hsigma0) : y ≤ normalizedBlockResponseScalarEMaxOnCube Q a sigma0 hsigma0

Every scalar response value is bounded by the one-cube response supremum.

theorem HCPolySupport.Book.Ch02.normalizedBlockResponseScalarEMaxOnCube_isLUB {d : ℕ} (Q : TriadicCube d) (a : CoeffOn (cubeDomain Q)) (sigma0 : ℝ) (hsigma0 : 0 < sigma0) : IsLUB (normalizedBlockResponseScalarEValueSetOnCube Q a sigma0 hsigma0) (normalizedBlockResponseScalarEMaxOnCube Q a sigma0 hsigma0)

The scalar response maximum is the least upper bound of the value set. No attainment assertion is included.

theorem HCPolySupport.Book.Ch02.normalizedBlockResponseScalarEMaxOnCube_lt_top {d : ℕ} (Q : TriadicCube d) (a : CoeffOn (cubeDomain Q)) (sigma0 : ℝ) (hsigma0 : 0 < sigma0) : normalizedBlockResponseScalarEMaxOnCube Q a sigma0 hsigma0 < ⊤

The scalar response supremum is finite.