Coarse-graining support: Support.Book.Ch02.Theorems.MultiscaleEllipticity.Basic

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

Basic Helpers for Chapter 2.5 Multiscale Ellipticity

This file contains the matrix-norm, finite-supremum, and scale-weight helper lemmas used by the public multiscale ellipticity theorem package.

theorem HCPolySupport.Book.Ch02.matrixNorm_eq_matrixOperatorNorm {d : ℕ} (A : Mat d) : matrixNorm A = matrixOperatorNorm A

theorem HCPolySupport.Book.Ch02.matrixFrobeniusNorm_eq_matNorm {d : ℕ} (A : Mat d) : matrixFrobeniusNorm A = matNorm A

theorem HCPolySupport.Book.Ch02.matrixNorm_nonneg {d : ℕ} (A : Mat d) : 0 ≤ matrixNorm A

theorem HCPolySupport.Book.Ch02.matrixNorm_le_matNorm {d : ℕ} (A : Mat d) : matrixNorm A ≤ matNorm A

theorem HCPolySupport.Book.Ch02.matNorm_le_dim_mul_matrixNorm {d : ℕ} (A : Mat d) : matNorm A ≤ ↑d * matrixNorm A

theorem HCPolySupport.Book.Ch02.matNorm_le_sum_abs_entries {d : ℕ} (A : Mat d) : matNorm A ≤ ∑ i : Fin d, ∑ j : Fin d, |A i j|

The legacy Frobenius norm is bounded by the entrywise l¹ norm.

theorem HCPolySupport.Book.Ch02.matrixNorm_le_matrixNorm_add_matrixNorm_sub {d : ℕ} (A B : Mat d) : matrixNorm A ≤ matrixNorm B + matrixNorm (A - B)

Triangle inequality for the Chapter 2 matrix norm around a center.

theorem HCPolySupport.Book.Ch02.matrixNorm_le_matrixNorm_add_sum_abs_sub_entries {d : ℕ} (A B : Mat d) : matrixNorm A ≤ matrixNorm B + ∑ i : Fin d, ∑ j : Fin d, |A i j - B i j|

The Chapter 2 matrix norm around a center is controlled by the entrywise l¹ size of the centered matrix.

theorem HCPolySupport.Book.Ch02.coarseBMatrixNorm_nonneg {d : ℕ} (Q : TriadicCube d) (a : TriadicCoeffFamily d) : 0 ≤ coarseBMatrixNorm Q a

theorem HCPolySupport.Book.Ch02.coarseSigmaStarInvMatrixNorm_nonneg {d : ℕ} (Q : TriadicCube d) (a : TriadicCoeffFamily d) : 0 ≤ coarseSigmaStarInvMatrixNorm Q a

theorem HCPolySupport.Book.Ch02.one_le_matrixNorm_one {d : ℕ} [NeZero d] : 1 ≤ matrixNorm 1

theorem HCPolySupport.Book.Ch02.matrixNorm_inv_le_of_mul_eq_one {d : ℕ} [NeZero d] {A B : Mat d} (hAB : A * B = 1) (hApos : 0 < matrixNorm A) : (matrixNorm A)⁻¹ ≤ matrixNorm B

theorem HCPolySupport.Book.Ch02.bCoarse_isSymm {d : ℕ} (U : Domain d) (a : CoeffOn U) : Matrix.IsSymm (bCoarse U a)

theorem HCPolySupport.Book.Ch02.posSemidef_of_matLoewnerLE_of_posSemidef_of_isSymm {d : ℕ} {A B : Mat d} (hA : Matrix.PosSemidef A) (hBsymm : Matrix.IsSymm B) (hAB : MatLoewnerLE A B) : Matrix.PosSemidef B

theorem HCPolySupport.Book.Ch02.bCoarse_posSemidef {d : ℕ} (U : Domain d) (a : CoeffOn U) : Matrix.PosSemidef (bCoarse U a)

theorem HCPolySupport.Book.Ch02.matrixNorm_le_matNorm_of_matLoewnerLE_of_posSemidef {d : ℕ} {A B : Mat d} (hA : Matrix.PosSemidef A) (hB : Matrix.PosSemidef B) (hAB : MatLoewnerLE A B) : matrixNorm A ≤ matNorm B

theorem HCPolySupport.Book.Ch02.matrixNorm_le_of_matLoewnerLE_of_posSemidef {d : ℕ} {A B : Mat d} (hA : Matrix.PosSemidef A) (hB : Matrix.PosSemidef B) (hAB : MatLoewnerLE A B) : matrixNorm A ≤ matrixNorm B

theorem HCPolySupport.Book.Ch02.matrixNorm_le_center_add_sum_abs_sub_entries_of_matLoewnerLE {d : ℕ} {A B center : Mat d} (hA : Matrix.PosSemidef A) (hB : Matrix.PosSemidef B) (hAB : MatLoewnerLE A B) : matrixNorm A ≤ matrixNorm center + ∑ i : Fin d, ∑ j : Fin d, |B i j - center i j|

A positive semidefinite matrix below B in Löwner order is controlled by the norm of any deterministic center plus the entrywise centered size of B.

theorem HCPolySupport.Book.Ch02.matrixNorm_pos_of_posDef {d : ℕ} [NeZero d] {A : Mat d} (hA : Matrix.PosDef A) : 0 < matrixNorm A

theorem HCPolySupport.Book.Ch02.vecNormSq_le_matrixNorm_mul_vecDot_matVecMul_of_posSemidef_of_leftInverse {d : ℕ} {A B : Mat d} (hB : Matrix.PosSemidef B) (hleftInv : ∀ (ξ : Vec d), matVecMul B (matVecMul A ξ) = ξ) (ξ : Vec d) : vecNormSq ξ ≤ matrixNorm B * vecDot ξ (matVecMul A ξ)

theorem HCPolySupport.Book.Ch02.bCoarse_posDef {d : ℕ} (U : Domain d) (a : CoeffOn U) : Matrix.PosDef (bCoarse U a)

theorem HCPolySupport.Book.Ch02.matrixNorm_descendantsAverageMat_le_descendantsAverage_matrixNorm {d : ℕ} (Q : TriadicCube d) (j : ℕ) (F : TriadicCube d → Mat d) : matrixNorm (descendantsAverageMat Q j F) ≤ descendantsAverage Q j fun (R : TriadicCube d) => matrixNorm (F R)

theorem HCPolySupport.Book.Ch02.matrixNorm_descendantsAverageMat_le_finsetSupReal_matrixNorm {d : ℕ} (Q : TriadicCube d) (j : ℕ) (F : TriadicCube d → Mat d) : matrixNorm (descendantsAverageMat Q j F) ≤ finsetSupReal (descendantsAtDepth Q j) fun (R : TriadicCube d) => matrixNorm (F R)

theorem HCPolySupport.Book.Ch02.finsetSupReal_eq_finsetSsup {α : Type u_1} (s : Finset α) (f : α → ℝ) : finsetSupReal s f = finsetSsup s f

theorem HCPolySupport.Book.Ch02.finsetSupReal_congr {α : Type u_1} (s : Finset α) {f g : α → ℝ} (hfg : ∀ x ∈ s, f x = g x) : finsetSupReal s f = finsetSupReal s g

theorem HCPolySupport.Book.Ch02.finsetSupReal_image {α : Type u_1} {β : Type u_2} [DecidableEq β] (s : Finset α) (φ : α → β) (f : β → ℝ) (g : α → ℝ) (hfg : ∀ x ∈ s, f (φ x) = g x) : finsetSupReal (Finset.image φ s) f = finsetSupReal s g

theorem HCPolySupport.Book.Ch02.finsetSupReal_nonneg {α : Type u_1} (s : Finset α) (f : α → ℝ) (hf : ∀ x ∈ s, 0 ≤ f x) : 0 ≤ finsetSupReal s f

theorem HCPolySupport.Book.Ch02.finsetSupReal_mono {α : Type u_1} (s : Finset α) (hs : s.Nonempty) {f g : α → ℝ} (hfg : ∀ x ∈ s, f x ≤ g x) : finsetSupReal s f ≤ finsetSupReal s g

theorem HCPolySupport.Book.Ch02.finsetSupReal_const_mul_le {α : Type u_1} (s : Finset α) (hs : s.Nonempty) {c : ℝ} (hc : 0 ≤ c) (f : α → ℝ) : (finsetSupReal s fun (x : α) => c * f x) ≤ c * finsetSupReal s f

theorem HCPolySupport.Book.Ch02.finsetSupReal_le_of_subset {α : Type u_1} (s t : Finset α) (hs : s.Nonempty) (hst : ↑s ⊆ ↑t) (f : α → ℝ) : finsetSupReal s f ≤ finsetSupReal t f

theorem HCPolySupport.Book.Ch02.finsetSupReal_le {α : Type u_1} (s : Finset α) (hs : s.Nonempty) {f : α → ℝ} {C : ℝ} (hC : ∀ x ∈ s, f x ≤ C) : finsetSupReal s f ≤ C

theorem HCPolySupport.Book.Ch02.geometricDiscount_eq_old (s q : ℝ) : geometricDiscount s q = HCPolySupport.geometricDiscount s q

theorem HCPolySupport.Book.Ch02.geometricWeight_eq_old (s q : ℝ) (n : ℕ) : geometricWeight s q n = HCPolySupport.geometricWeight s q n

theorem HCPolySupport.Book.Ch02.old_descendantWeight_eq_multiscaleDescendantWeight {d : ℕ} (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) (s : ℝ) : Real.rpow 3 (2 * s * ↑(Q.scale - k).toNat) = multiscaleDescendantWeight Q k s

theorem HCPolySupport.Book.Ch02.infinityWeight_nonneg (s : ℝ) (n : ℕ) : 0 ≤ Real.rpow 3 (-2 * s * ↑n)

theorem HCPolySupport.Book.Ch02.infinityWeight_le_one {s : ℝ} (hs : 0 ≤ s) (n : ℕ) : Real.rpow 3 (-2 * s * ↑n) ≤ 1

theorem HCPolySupport.Book.Ch02.infinityWeight_le_of_le {t s : ℝ} (hts : t ≤ s) (n : ℕ) : Real.rpow 3 (-2 * s * ↑n) ≤ Real.rpow 3 (-2 * t * ↑n)

theorem HCPolySupport.Book.Ch02.infinityWeight_shift (s : ℝ) (h n : ℕ) : Real.rpow 3 (-2 * s * ↑n) = Real.rpow 3 (2 * s * ↑h) * Real.rpow 3 (-2 * s * ↑(n + h))