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

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

Chapter 2.5 Multiscale Ellipticity Constants

This file locks the public definitions from Section 2.5 of the notes. The multiscale quantities are deliberately built from the Chapter 2 CoeffOn interface on open cube domains, and the compatibility of a coefficient field across nested cubes is recorded almost everywhere.

theorem HCPolySupport.Book.Ch02.openCubeSet_nonempty {d : ℕ} (Q : TriadicCube d) : (openCubeSet Q).Nonempty

The open realization of a triadic cube is a nonempty public Chapter 2 domain.

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

The public Chapter 2 domain associated with an open triadic cube.

Equations

• HCPolySupport.Book.Ch02.cubeDomain Q = { carrier := HCPolySupport.openCubeSet Q, isDomain := ⋯, nonempty := ⋯ }

@[simp]

theorem HCPolySupport.Book.Ch02.cubeDomain_coe {d : ℕ} (Q : TriadicCube d) : (cubeDomain Q).carrier = openCubeSet Q

structure HCPolySupport.Book.Ch02.TriadicCoeffFamily (d : ℕ) : Type

A coefficient field on the triadic cube hierarchy.

For each open triadic cube it provides a CoeffOn object, hence ellipticity and measurability are a.e. on that cube. The restrictsTo_of_subset field says that the representatives are compatible across nested cubes only modulo null sets; this is the public replacement for old representative-level cube restrictions.

• coeffOn (Q : TriadicCube d) : CoeffOn (cubeDomain Q)

  The measurable, almost-everywhere elliptic coefficient object assigned to each open triadic cube.

• restrictsTo_of_subset {Q R : TriadicCube d} : openCubeSet R ⊆ openCubeSet Q → (self.coeffOn Q).RestrictsTo (self.coeffOn R)

def HCPolySupport.Book.Ch02.TriadicCoeffFamily.AEEq {d : ℕ} (a b : TriadicCoeffFamily d) : Prop

Two triadic coefficient families are equal when their cube representatives agree a.e. on every open triadic cube.

Equations

• a.AEEq b = ∀ (Q : HCPolySupport.TriadicCube d), (a.coeffOn Q).AEEq (b.coeffOn Q)

theorem HCPolySupport.Book.Ch02.TriadicCoeffFamily.restrictsTo_self {d : ℕ} (a : TriadicCoeffFamily d) (Q : TriadicCube d) : (a.coeffOn Q).RestrictsTo (a.coeffOn Q)

theorem HCPolySupport.Book.Ch02.TriadicCoeffFamily.restrictsTo_descendant {d : ℕ} (a : TriadicCoeffFamily d) {Q R : TriadicCube d} {k : ℤ} (hk : k ≤ Q.scale) (hR : R ∈ descendantsAtScale Q k) : (a.coeffOn Q).RestrictsTo (a.coeffOn R)

Compatibility of a triadic coefficient family with a descendant cube, expressed a.e. on the descendant open cube.

theorem HCPolySupport.Book.Ch02.TriadicCoeffFamily.AEEq.refl {d : ℕ} (a : TriadicCoeffFamily d) : a.AEEq a

theorem HCPolySupport.Book.Ch02.TriadicCoeffFamily.AEEq.symm {d : ℕ} {a b : TriadicCoeffFamily d} (h : a.AEEq b) : b.AEEq a

theorem HCPolySupport.Book.Ch02.TriadicCoeffFamily.AEEq.trans {d : ℕ} {a b c : TriadicCoeffFamily d} (hab : a.AEEq b) (hbc : b.AEEq c) : a.AEEq c

inductive HCPolySupport.Book.Ch02.MultiscaleExponent : Type

Exponents used in the multiscale ellipticity constants: finite q and the endpoint q = infinity.

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

@[instance_reducible]

noncomputable instance HCPolySupport.Book.Ch02.instDecidableEqMultiscaleExponent : DecidableEq MultiscaleExponent

Equations

• HCPolySupport.Book.Ch02.instDecidableEqMultiscaleExponent = HCPolySupport.Book.Ch02.instDecidableEqMultiscaleExponent.decEq

noncomputable def HCPolySupport.Book.Ch02.instDecidableEqMultiscaleExponent.decEq (x✝ x✝¹ : MultiscaleExponent) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• HCPolySupport.Book.Ch02.instDecidableEqMultiscaleExponent.decEq (HCPolySupport.Book.Ch02.MultiscaleExponent.finite value) HCPolySupport.Book.Ch02.MultiscaleExponent.infinity = isFalse ⋯
• HCPolySupport.Book.Ch02.instDecidableEqMultiscaleExponent.decEq HCPolySupport.Book.Ch02.MultiscaleExponent.infinity (HCPolySupport.Book.Ch02.MultiscaleExponent.finite value) = isFalse ⋯
• HCPolySupport.Book.Ch02.instDecidableEqMultiscaleExponent.decEq HCPolySupport.Book.Ch02.MultiscaleExponent.infinity HCPolySupport.Book.Ch02.MultiscaleExponent.infinity = isTrue ⋯

def HCPolySupport.Book.Ch02.MultiscaleExponent.IsAdmissible : MultiscaleExponent → Prop

Admissible exponents in the public Sec. 2.5 definitions: finite q ≥ 1 or the endpoint q = infinity.

Equations

• (HCPolySupport.Book.Ch02.MultiscaleExponent.finite q).IsAdmissible = (1 ≤ q)
• HCPolySupport.Book.Ch02.MultiscaleExponent.infinity.IsAdmissible = True

@[simp]

theorem HCPolySupport.Book.Ch02.MultiscaleExponent.isAdmissible_finite {q : ℝ} : (finite q).IsAdmissible ↔ 1 ≤ q

@[simp]

theorem HCPolySupport.Book.Ch02.MultiscaleExponent.isAdmissible_infinity : infinity.IsAdmissible

def HCPolySupport.Book.Ch02.matrixNormSq {d : ℕ} (A : Mat d) : ℝ

Legacy Frobenius-style squared matrix norm retained for compatibility with older deterministic infrastructure.

Equations

• HCPolySupport.Book.Ch02.matrixNormSq A = ∑ i : Fin d, ∑ j : Fin d, A i j ^ 2

noncomputable def HCPolySupport.Book.Ch02.matrixNorm {d : ℕ} (A : Mat d) : ℝ

Euclidean/L2 operator norm used for |b| and |sigma_*^{-1}| in the public Sec. 2.5 definitions.

Equations

• HCPolySupport.Book.Ch02.matrixNorm A = ‖Matrix.toEuclideanCLM A‖

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

Supremum of a real-valued function over a finite set.

The old deterministic files use the same sSup convention, which leaves the definition total even when the finite set is empty.

Equations

• HCPolySupport.Book.Ch02.finsetSupReal s f = sSup (f '' ↑s)

noncomputable def HCPolySupport.Book.Ch02.multiscaleDescendantWeight {d : ℕ} (Q : TriadicCube d) (k : ℤ) (s : ℝ) : ℝ

The scale factor 3^{2s(m-k)} appearing in one-cube descendant bounds.

Equations

• HCPolySupport.Book.Ch02.multiscaleDescendantWeight Q k s = Real.rpow 3 (2 * s * ↑(Q.scale - k))

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

One-cube norm |b(Q; a)|, where b is the canonical public coarse matrix on the open cube.

Equations

• HCPolySupport.Book.Ch02.coarseBMatrixNorm Q a = HCPolySupport.Book.Ch02.matrixNorm (HCPolySupport.Book.Ch02.bCoarse (HCPolySupport.Book.Ch02.cubeDomain Q) (a.coeffOn Q))

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

One-cube norm |sigma_*^{-1}(Q; a)|, where sigma_*^{-1} is the canonical public coarse matrix on the open cube.

Equations

• HCPolySupport.Book.Ch02.coarseSigmaStarInvMatrixNorm Q a = HCPolySupport.Book.Ch02.matrixNorm (HCPolySupport.Book.Ch02.sigmaStarInvCoarse (HCPolySupport.Book.Ch02.cubeDomain Q) (a.coeffOn Q))

noncomputable def HCPolySupport.Book.Ch02.maxDescendantBMatrixNormAtScale {d : ℕ} (Q : TriadicCube d) (k : ℤ) (a : TriadicCoeffFamily d) : ℝ

The maximum of |b(R; a)| over descendants of Q at scale k.

Equations

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

noncomputable def HCPolySupport.Book.Ch02.maxDescendantSigmaStarInvMatrixNormAtScale {d : ℕ} (Q : TriadicCube d) (k : ℤ) (a : TriadicCoeffFamily d) : ℝ

The maximum of |sigma_*^{-1}(R; a)| over descendants of Q at scale k.

Equations

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

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

Geometric normalization c_{s,q} = 1 - 3^{-s q} for finite exponents.

Equations

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

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

The finite-exponent geometric weight c_{s,q} 3^{-s q n}.

Equations

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

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

Finite-exponent coarse-grained upper ellipticity \Lambda_{s,q}(Q; a).

Equations

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

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

Finite-exponent coarse-grained lower ellipticity \lambda_{s,q}(Q; a).

Equations

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

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

Endpoint coarse-grained upper ellipticity \Lambda_{s,\infty}(Q; a).

Equations

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

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

Endpoint coarse-grained lower ellipticity \lambda_{s,\infty}(Q; a).

Equations

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

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

Coarse-grained upper ellipticity for finite q and q = infinity.

Equations

• HCPolySupport.Book.Ch02.LambdaSq Q s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite q_1) a = HCPolySupport.Book.Ch02.LambdaSqFinite Q s q_1 a
• HCPolySupport.Book.Ch02.LambdaSq Q s HCPolySupport.Book.Ch02.MultiscaleExponent.infinity a = HCPolySupport.Book.Ch02.LambdaSqInfinity Q s a

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

Coarse-grained lower ellipticity for finite q and q = infinity.

Equations

• HCPolySupport.Book.Ch02.lambdaSq Q s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite q_1) a = HCPolySupport.Book.Ch02.lambdaSqFinite Q s q_1 a
• HCPolySupport.Book.Ch02.lambdaSq Q s HCPolySupport.Book.Ch02.MultiscaleExponent.infinity a = HCPolySupport.Book.Ch02.lambdaSqInfinity Q s a

@[simp]

theorem HCPolySupport.Book.Ch02.LambdaSq_finite {d : ℕ} (Q : TriadicCube d) (s q : ℝ) (a : TriadicCoeffFamily d) : LambdaSq Q s (MultiscaleExponent.finite q) a = LambdaSqFinite Q s q a

@[simp]

theorem HCPolySupport.Book.Ch02.LambdaSq_infinity {d : ℕ} (Q : TriadicCube d) (s : ℝ) (a : TriadicCoeffFamily d) : LambdaSq Q s MultiscaleExponent.infinity a = LambdaSqInfinity Q s a

@[simp]

theorem HCPolySupport.Book.Ch02.lambdaSq_finite {d : ℕ} (Q : TriadicCube d) (s q : ℝ) (a : TriadicCoeffFamily d) : lambdaSq Q s (MultiscaleExponent.finite q) a = lambdaSqFinite Q s q a

@[simp]

theorem HCPolySupport.Book.Ch02.lambdaSq_infinity {d : ℕ} (Q : TriadicCube d) (s : ℝ) (a : TriadicCoeffFamily d) : lambdaSq Q s MultiscaleExponent.infinity a = lambdaSqInfinity Q s a

noncomputable def HCPolySupport.Book.Ch02.maxDescendantUpperEllipticityAtScale {d : ℕ} (Q : TriadicCube d) (k : ℤ) (s : ℝ) (q : MultiscaleExponent) (a : TriadicCoeffFamily d) : ℝ

The maximum of \Lambda_{s,q}(R; a) over descendants of Q at scale k.

Equations

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

noncomputable def HCPolySupport.Book.Ch02.maxDescendantLowerEllipticityInvAtScale {d : ℕ} (Q : TriadicCube d) (k : ℤ) (s : ℝ) (q : MultiscaleExponent) (a : TriadicCoeffFamily d) : ℝ

The maximum of \lambda_{s,q}(R; a)^{-1} over descendants of Q at scale k.

Equations

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

noncomputable def HCPolySupport.Book.Ch02.LambdaS {d : ℕ} (Q : TriadicCube d) (s : ℝ) (a : TriadicCoeffFamily d) : ℝ

The default finite-exponent convention q = 1 for \Lambda_s.

Equations

• HCPolySupport.Book.Ch02.LambdaS Q s a = HCPolySupport.Book.Ch02.LambdaSq Q s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 1) a

noncomputable def HCPolySupport.Book.Ch02.lambdaS {d : ℕ} (Q : TriadicCube d) (s : ℝ) (a : TriadicCoeffFamily d) : ℝ

The default finite-exponent convention q = 1 for \lambda_s.

Equations

• HCPolySupport.Book.Ch02.lambdaS Q s a = HCPolySupport.Book.Ch02.lambdaSq Q s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 1) a

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

Coarse-grained ellipticity ratio \Theta_{s,t}(Q; a) = \Lambda_{s,1}(Q; a) / \lambda_{t,1}(Q; a).

Equations

• HCPolySupport.Book.Ch02.ThetaRatio Q s t a = HCPolySupport.Book.Ch02.LambdaS Q s a / HCPolySupport.Book.Ch02.lambdaS Q t a