Coarse-graining support: Support.Deterministic.MultiscaleQuantities

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

inductive HCPolySupport.MultiscaleExponent : Type

A multiscale aggregation exponent, either a real value or infinity.

• finite (value : ℝ) : MultiscaleExponent
• infinity : MultiscaleExponent

def HCPolySupport.fullBlockVecNormSq {d : ℕ} (x : FullBlockVec d) : ℝ

The sum of squared coordinates of a full block vector.

Equations

• HCPolySupport.fullBlockVecNormSq x = ∑ i : HCPolySupport.BlockCoord d, x i ^ 2

def HCPolySupport.matNormSq {d : ℕ} (A : Mat d) : ℝ

The sum of squared entries of a matrix.

Equations

• HCPolySupport.matNormSq A = ∑ i : Fin d, ∑ j : Fin d, A i j ^ 2

noncomputable def HCPolySupport.matNorm {d : ℕ} (A : Mat d) : ℝ

The Frobenius norm of a real matrix.

Equations

• HCPolySupport.matNorm A = √(HCPolySupport.matNormSq A)

noncomputable def HCPolySupport.finsetAverage {α : Type u_1} (s : Finset α) (f : α → ℝ) : ℝ

The sum of values on a finite set divided by its cardinality, yielding zero for the empty set.

Equations

• HCPolySupport.finsetAverage s f = (↑s.card)⁻¹ * s.sum f

noncomputable def HCPolySupport.finsetSsup {α : Type u_1} (s : Finset α) (f : α → ℝ) : ℝ

The real supremum of the values attained on a finite set.

Equations

• HCPolySupport.finsetSsup s f = sSup (f '' ↑s)

noncomputable def HCPolySupport.coarseBBlockNorm {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) : ℝ

The Frobenius norm of the upper-left coarse block matrix on a cube.

Equations

• HCPolySupport.coarseBBlockNorm Q a = HCPolySupport.matNorm (HCPolySupport.coarseBlockMatrix (HCPolySupport.cubeSet Q) a).upperLeft

noncomputable def HCPolySupport.coarseSigmaStarInvBlockNorm {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) : ℝ

The Frobenius norm of the lower-right coarse block matrix on a cube.

Equations

• HCPolySupport.coarseSigmaStarInvBlockNorm Q a = HCPolySupport.matNorm (HCPolySupport.coarseBlockMatrix (HCPolySupport.cubeSet Q) a).lowerRight

noncomputable def HCPolySupport.maxDescendantBBlockNormAtScale {d : ℕ} (Q : TriadicCube d) (k : ℤ) (a : CoeffField d) : ℝ

The real supremum of upper-left coarse block norms over descendants at scale k.

Equations

• HCPolySupport.maxDescendantBBlockNormAtScale Q k a = HCPolySupport.finsetSsup (HCPolySupport.descendantsAtScale Q k) fun (R : HCPolySupport.TriadicCube d) => HCPolySupport.coarseBBlockNorm R a

noncomputable def HCPolySupport.maxDescendantSigmaStarInvNormAtScale {d : ℕ} (Q : TriadicCube d) (k : ℤ) (a : CoeffField d) : ℝ

The real supremum of lower-right coarse block norms over descendants at scale k.

Equations

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

noncomputable def HCPolySupport.geometricDiscount (s q : ℝ) : ℝ

The geometric normalization factor 1 - 3 ^ (-s * q).

Equations

• HCPolySupport.geometricDiscount s q = 1 - Real.rpow 3 (-s * q)

noncomputable def HCPolySupport.geometricWeight (s q : ℝ) (n : ℕ) : ℝ

The depth-n geometric weight (1 - 3 ^ (-s * q)) * 3 ^ (-s * q * n).

Equations

• HCPolySupport.geometricWeight s q n = HCPolySupport.geometricDiscount s q * Real.rpow 3 (-s * q * ↑n)

noncomputable def HCPolySupport.LambdaSqFinite {d : ℕ} (Q : TriadicCube d) (s q : ℝ) (a : CoeffField d) : ℝ

The weighted sum of descendant upper-left block maxima to power q/2, raised to 2/q.

Equations

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

noncomputable def HCPolySupport.lambdaSqFinite {d : ℕ} (Q : TriadicCube d) (s q : ℝ) (a : CoeffField d) : ℝ

The weighted sum of descendant lower-right block maxima to power q/2, raised to -2/q.

Equations

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

noncomputable def HCPolySupport.LambdaSqInfinity {d : ℕ} (Q : TriadicCube d) (s : ℝ) (a : CoeffField d) : ℝ

The real supremum over depths of upper-left block maxima weighted by 3 ^ (-2 * s * n).

Equations

• HCPolySupport.LambdaSqInfinity Q s a = sSup {m : ℝ | ∃ (n : ℕ), m = Real.rpow 3 (-2 * s * ↑n) * HCPolySupport.maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a}

noncomputable def HCPolySupport.lambdaSqInfinity {d : ℕ} (Q : TriadicCube d) (s : ℝ) (a : CoeffField d) : ℝ

The inverse real supremum of lower-right block maxima weighted by 3 ^ (-2 * s * n).

Equations

• HCPolySupport.lambdaSqInfinity Q s a = (sSup {m : ℝ | ∃ (n : ℕ), m = Real.rpow 3 (-2 * s * ↑n) * HCPolySupport.maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a})⁻¹

noncomputable def HCPolySupport.LambdaSq {d : ℕ} (Q : TriadicCube d) (s : ℝ) (q : MultiscaleExponent) (a : CoeffField d) : ℝ

The upper multiscale quantity, using the power-sum or supremum formula according to the exponent.

Equations

• HCPolySupport.LambdaSq Q s (HCPolySupport.MultiscaleExponent.finite q_2) a = HCPolySupport.LambdaSqFinite Q s q_2 a
• HCPolySupport.LambdaSq Q s HCPolySupport.MultiscaleExponent.infinity a = HCPolySupport.LambdaSqInfinity Q s a

noncomputable def HCPolySupport.lambdaSq {d : ℕ} (Q : TriadicCube d) (s : ℝ) (q : MultiscaleExponent) (a : CoeffField d) : ℝ

The lower multiscale quantity, using the inverse power-sum or inverse supremum formula.

Equations

• HCPolySupport.lambdaSq Q s (HCPolySupport.MultiscaleExponent.finite q_2) a = HCPolySupport.lambdaSqFinite Q s q_2 a
• HCPolySupport.lambdaSq Q s HCPolySupport.MultiscaleExponent.infinity a = HCPolySupport.lambdaSqInfinity Q s a

noncomputable def HCPolySupport.ThetaRatio {d : ℕ} (Q : TriadicCube d) (s t : ℝ) (a : CoeffField d) : ℝ

Deterministic cube-level contrast ratio Λ_{s,1}(Q) / λ_{t,1}(Q). This is not the annealed Chapter-5 sequence Θ_n.

Equations

• HCPolySupport.ThetaRatio Q s t a = HCPolySupport.LambdaSq Q s (HCPolySupport.MultiscaleExponent.finite 1) a / HCPolySupport.lambdaSq Q t (HCPolySupport.MultiscaleExponent.finite 1) a

noncomputable def HCPolySupport.constantFullBlockMatrix {d : ℕ} (a0 : Mat d) : FullBlockMat d

The full block-coordinate matrix associated with the constant coefficient matrix a0.

Equations

• HCPolySupport.constantFullBlockMatrix a0 = HCPolySupport.toFullBlockMat (HCPolySupport.blockMatrixOfCoeff a0)

noncomputable def HCPolySupport.constantFullBlockMatrixSqrt {d : ℕ} (a0 : Mat d) : FullBlockMat d

The continuous-functional-calculus square root of the constant full block matrix.

Equations

• HCPolySupport.constantFullBlockMatrixSqrt a0 = CFC.sqrt (HCPolySupport.constantFullBlockMatrix a0)

noncomputable def HCPolySupport.constantFullBlockMatrixInvSqrt {d : ℕ} (a0 : Mat d) : FullBlockMat d

The matrix inverse of the square root of the constant full block matrix.

Equations

• HCPolySupport.constantFullBlockMatrixInvSqrt a0 = (HCPolySupport.constantFullBlockMatrixSqrt a0)⁻¹

noncomputable def HCPolySupport.normalizedBlockResponseValueSet {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) : Set ℝ

Block responses on unit block vectors, with inputs 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.normalizedBlockResponseMax {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) : ℝ

The real supremum of block responses normalized by the constant block matrix.

Equations

• HCPolySupport.normalizedBlockResponseMax Q a a0 = sSup (HCPolySupport.normalizedBlockResponseValueSet Q a a0)

noncomputable def HCPolySupport.maxDescendantNormalizedBlockResponseAtScale {d : ℕ} (Q : TriadicCube d) (k : ℤ) (a : CoeffField d) (a0 : Mat d) : ℝ

The real supremum of normalized block responses over descendants at scale k.

Equations

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

noncomputable def HCPolySupport.scaleResponseAtScale {d : ℕ} (Q : TriadicCube d) (k : ℤ) (p : MultiscaleExponent) (a : CoeffField d) (a0 : Mat d) : ℝ

The descendant mean of normalized responses to power p/2, raised to 1/p; at infinity, the square root of their real supremum.

Equations

• One or more equations did not get rendered due to their size.
• HCPolySupport.scaleResponseAtScale Q k HCPolySupport.MultiscaleExponent.infinity a a0 = (HCPolySupport.maxDescendantNormalizedBlockResponseAtScale Q k a a0).rpow (1 / 2)

noncomputable def HCPolySupport.HomogenizationErrorFinite {d : ℕ} (Q : TriadicCube d) (n : ℤ) (s : ℝ) (p : MultiscaleExponent) (q : ℝ) (a : CoeffField d) (a0 : Mat d) : ℝ

The geometrically weighted q-power sum of scale responses below scale n, raised to 1/q.

Equations

• HCPolySupport.HomogenizationErrorFinite Q n s p q a a0 = (∑' (l : ℕ), HCPolySupport.geometricWeight s q l * (HCPolySupport.scaleResponseAtScale Q (n - ↑l) p a a0).rpow q).rpow (1 / q)

noncomputable def HCPolySupport.HomogenizationErrorInfinity {d : ℕ} (Q : TriadicCube d) (n : ℤ) (s : ℝ) (p : MultiscaleExponent) (a : CoeffField d) (a0 : Mat d) : ℝ

The real supremum of scale responses below n, weighted by 3 ^ (-s * l).

Equations

• HCPolySupport.HomogenizationErrorInfinity Q n s p a a0 = sSup {m : ℝ | ∃ (l : ℕ), m = Real.rpow 3 (-s * ↑l) * HCPolySupport.scaleResponseAtScale Q (n - ↑l) p a a0}

noncomputable def HCPolySupport.HomogenizationError {d : ℕ} (Q : TriadicCube d) (n : ℤ) (s : ℝ) (p q : MultiscaleExponent) (a : CoeffField d) (a0 : Mat d) : ℝ

The multiscale response error, using power-sum or supremum aggregation over scales.

Equations

• HCPolySupport.HomogenizationError Q n s p (HCPolySupport.MultiscaleExponent.finite q_2) a a0 = HCPolySupport.HomogenizationErrorFinite Q n s p q_2 a a0
• HCPolySupport.HomogenizationError Q n s p HCPolySupport.MultiscaleExponent.infinity a a0 = HCPolySupport.HomogenizationErrorInfinity Q n s p a a0

noncomputable def HCPolySupport.HomogenizationErrorOnCube {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : MultiscaleExponent) (a : CoeffField d) (a0 : Mat d) : ℝ

The multiscale response error starting at the parent cube's own scale.

Equations

• HCPolySupport.HomogenizationErrorOnCube Q s p q a a0 = HCPolySupport.HomogenizationError Q Q.scale s p q a a0