Coarse-graining support: Support.Book.Ch05.Theorems.Section52.PointwiseSplits

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

Section 5.2 internals: PointwiseSplits

Pointwise upper and lower finite-one decompositions.

theorem HCPolySupport.Book.Ch05.Section52.sq_add_le_weighted_sum_add_tail_sq_div {L T A W V : ℝ} (hV : 0 < V) (hA : 0 ≤ A) (hW : 0 ≤ W) (hWV : W + V ≤ 1) (hLsq : L ^ 2 ≤ W * A) : (L + T) ^ 2 ≤ A + T ^ 2 / V

noncomputable def HCPolySupport.Book.Ch05.Section52.upperSmallSqrtTailCoeffField {d : ℕ} (m : ℕ) (s : ℝ) (a : RegCoeffField d) : ℝ

The geometrically weighted tail of square roots of maximal descendant B-matrix norms at scales -j in the scale-m origin cube.

Equations

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

theorem HCPolySupport.Book.Ch05.Section52.maxDescendantBMatrixNormCoeffFieldAtScale_nonneg_of_le {d : ℕ} (Q : TriadicCube d) (a : RegCoeffField d) {k : ℤ} (hk : k ≤ Q.scale) : 0 ≤ Ch04.maxDescendantBMatrixNormCoeffFieldAtScale Q k a

theorem HCPolySupport.Book.Ch05.Section52.upperSmallSqrtTailCoeffField_nonneg {d : ℕ} (m : ℕ) {s : ℝ} (hs : 0 ≤ s) (a : RegCoeffField d) : 0 ≤ upperSmallSqrtTailCoeffField m s a

theorem HCPolySupport.Book.Ch05.Section52.LambdaSqCoeffField_originCube_finite_one_le_two_upperSmallSqrtTail_sq_add_two_largeScale_sum {d : ℕ} [NeZero d] (m : ℕ) {s : ℝ} (hs : 0 < s) (a : RegCoeffField d) : Ch04.LambdaSqCoeffField (originCube d ↑m) s (Ch02.MultiscaleExponent.finite 1) a ≤ 2 * upperSmallSqrtTailCoeffField m s a ^ 2 + 2 * ∑ n ∈ section52LargeScaleSet m, section52LargeScaleWeight s m n * Ch04.maxDescendantBMatrixNormCoeffFieldAtScale (originCube d ↑m) n a

theorem HCPolySupport.Book.Ch05.Section52.LambdaSqCoeffField_originCube_finite_one_le_upperSmallSqrtTail_sq_div_add_largeScale_sum {d : ℕ} [NeZero d] (m : ℕ) {s : ℝ} (hs : 0 < s) (a : RegCoeffField d) : Ch04.LambdaSqCoeffField (originCube d ↑m) s (Ch02.MultiscaleExponent.finite 1) a ≤ upperSmallSqrtTailCoeffField m s a ^ 2 / section52SmallTailWeight s m + ∑ n ∈ section52LargeScaleSet m, section52LargeScaleWeight s m n * Ch04.maxDescendantBMatrixNormCoeffFieldAtScale (originCube d ↑m) n a

noncomputable def HCPolySupport.Book.Ch05.Section52.lowerSmallSqrtTailCoeffField {d : ℕ} (m : ℕ) (s : ℝ) (a : RegCoeffField d) : ℝ

The geometrically weighted tail of square roots of maximal descendant inverse Sigma-star matrix norms at scales -j in the scale-m origin cube.

Equations

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

theorem HCPolySupport.Book.Ch05.Section52.maxDescendantSigmaStarInvMatrixNormCoeffFieldAtScale_nonneg_of_le {d : ℕ} (Q : TriadicCube d) (a : RegCoeffField d) {k : ℤ} (hk : k ≤ Q.scale) : 0 ≤ Ch04.maxDescendantSigmaStarInvMatrixNormCoeffFieldAtScale Q k a

theorem HCPolySupport.Book.Ch05.Section52.lowerSmallSqrtTailCoeffField_nonneg {d : ℕ} (m : ℕ) {s : ℝ} (hs : 0 ≤ s) (a : RegCoeffField d) : 0 ≤ lowerSmallSqrtTailCoeffField m s a

theorem HCPolySupport.Book.Ch05.Section52.lambdaSqCoeffField_originCube_finite_one_inv_le_two_lowerSmallSqrtTail_sq_add_two_largeScale_sum {d : ℕ} [NeZero d] (m : ℕ) {s : ℝ} (hs : 0 < s) (a : RegCoeffField d) : (Ch04.lambdaSqCoeffField (originCube d ↑m) s (Ch02.MultiscaleExponent.finite 1) a)⁻¹ ≤ 2 * lowerSmallSqrtTailCoeffField m s a ^ 2 + 2 * ∑ n ∈ section52LargeScaleSet m, section52LargeScaleWeight s m n * Ch04.maxDescendantSigmaStarInvMatrixNormCoeffFieldAtScale (originCube d ↑m) n a

theorem HCPolySupport.Book.Ch05.Section52.lambdaSqCoeffField_originCube_finite_one_inv_le_lowerSmallSqrtTail_sq_div_add_largeScale_sum {d : ℕ} [NeZero d] (m : ℕ) {s : ℝ} (hs : 0 < s) (a : RegCoeffField d) : (Ch04.lambdaSqCoeffField (originCube d ↑m) s (Ch02.MultiscaleExponent.finite 1) a)⁻¹ ≤ lowerSmallSqrtTailCoeffField m s a ^ 2 / section52SmallTailWeight s m + ∑ n ∈ section52LargeScaleSet m, section52LargeScaleWeight s m n * Ch04.maxDescendantSigmaStarInvMatrixNormCoeffFieldAtScale (originCube d ↑m) n a