Chapter 3 coefficient, Besov and cube geometry vocabulary

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

Chapter 3 foundational vocabulary

This file contains the note-facing quantities used in Chapter 3. The coefficient input is the Chapter 2 TriadicCoeffFamily, so all ellipticity and compatibility data remain a.e.-based on open cube domains.

@[reducible, inline]

abbrev HCPolySupport.Book.Ch03.CoeffFamily (d : ℕ) : Type

Cube-indexed coefficient data with a.e. ellipticity and compatibility, as used in Chapter 3.

Equations

• HCPolySupport.Book.Ch03.CoeffFamily d = HCPolySupport.Book.Ch02.TriadicCoeffFamily d

@[reducible, inline]

abbrev HCPolySupport.Book.Ch03.CubeSolution {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) : Type

A Chapter 2 solution on the cube domain for the coefficient selected by the family.

Equations

• HCPolySupport.Book.Ch03.CubeSolution Q a = HCPolySupport.Book.Ch02.Solution (HCPolySupport.Book.Ch02.cubeDomain Q) (a.coeffOn Q)

@[reducible, inline]

abbrev HCPolySupport.Book.Ch03.ForceBesovRegularity {d : ℕ} (Q : TriadicCube d) (s : ℝ) (g : Vec d → Vec d) : Prop

Public regularity package for the manuscript assumption g ∈ H^s(Q; R^d), in the form consumed by the deterministic RHS development.

Equations

• HCPolySupport.Book.Ch03.ForceBesovRegularity Q s g = HCPolySupport.CubeVectorBesovHRegularity Q s g

noncomputable def HCPolySupport.Book.Ch03.negativeBesovVectorDepthAverage {d : ℕ} (Q : TriadicCube d) (F : Vec d → Vec d) (j : ℕ) : ℝ

The depth-j block-average square for a vector field on a parent cube.

Equations

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

noncomputable def HCPolySupport.Book.Ch03.negativeBesovVectorDepthSeminorm {d : ℕ} (Q : TriadicCube d) (s : ℝ) (F : Vec d → Vec d) (j : ℕ) : ℝ

The note-normalized depth contribution in 3^{-s m} B^{-s}_{2,q}.

If R is a depth-j descendant of a scale-m cube, the outer factor 3^{-s m} combines with the scale of R to give this 3^{-s j} weight.

Equations

• HCPolySupport.Book.Ch03.negativeBesovVectorDepthSeminorm Q s F j = Real.rpow 3 (-s * ↑j) * √(HCPolySupport.Book.Ch03.negativeBesovVectorDepthAverage Q F j)

noncomputable def HCPolySupport.Book.Ch03.negativeBesovVectorPartialNormFinite {d : ℕ} (Q : TriadicCube d) (s q : ℝ) (N : ℕ) (F : Vec d → Vec d) : ℝ

Finite-depth vector-valued 3^{-s m} B^{-s}_{2,q} seminorm for finite multiscale exponent q.

Equations

• HCPolySupport.Book.Ch03.negativeBesovVectorPartialNormFinite Q s q N F = (∑ j ∈ Finset.range (N + 1), (HCPolySupport.Book.Ch03.negativeBesovVectorDepthSeminorm Q s F j).rpow q).rpow (1 / q)

noncomputable def HCPolySupport.Book.Ch03.scaleNormalizedNegativeBesovVectorNorm {d : ℕ} (Q : TriadicCube d) (s : ℝ) (q : Ch02.MultiscaleExponent) (F : Vec d → Vec d) : ℝ

Public vector-valued 3^{-s m} B^{-s}_{2,q} seminorm on a cube of scale m, using Euclidean norms of the cube-averaged vector field.

Equations

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

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch03.scaleNormalizedPositiveBesovVectorSeminormTwo {d : ℕ} (Q : TriadicCube d) (s : ℝ) (F : Vec d → Vec d) : ℝ

Note-normalized positive q = 2 Besov seminorm 3^{s m} [F]_{\underline B^s_{2,2}(Q)} for vector fields.

Equations

• HCPolySupport.Book.Ch03.scaleNormalizedPositiveBesovVectorSeminormTwo Q s F = HCPolySupport.cubeBesovPositiveVectorSeminormTwo Q s F

noncomputable def HCPolySupport.Book.Ch03.scaleNormalizedPositiveBesovVectorNormTwo {d : ℕ} (Q : TriadicCube d) (s : ℝ) (F : Vec d → Vec d) : ℝ

Note-normalized positive q = 2 Besov norm for vector fields.

The positive seminorms in the deterministic RHS layer are already normalized by the parent scale. The full norm adds the top-scale average, matching 3^{s m} ||F||_{\underline B^s_{2,2}(Q)}.

Equations

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

noncomputable def HCPolySupport.Book.Ch03.scaleNormalizedDualNegativeBesovVectorNormTwo {d : ℕ} (Q : TriadicCube d) (s : ℝ) (F : Vec d → Vec d) : ℝ

Public vector-valued genuine dual negative Besov norm, normalized as 3^{-s m} [F]_{\underline B^{-s}_{2,2}(Q)}.

This is deliberately separate from scaleNormalizedNegativeBesovVectorNorm, which is the concrete/circ seminorm used in the homogeneous coarse-graining estimates.

Equations

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

noncomputable def HCPolySupport.Book.Ch03.openCubeAtScale {d : ℕ} (center : Vec d) (m : ℤ) : Set (Vec d)

Open cube with arbitrary center and triadic scale.

Equations

• HCPolySupport.Book.Ch03.openCubeAtScale center m = {y : HCPolySupport.Vec d | ∀ (i : Fin d), |y i - center i| < Real.rpow 3 ↑m / 2}

theorem HCPolySupport.Book.Ch03.isOpen_openCubeAtScale {d : ℕ} (center : Vec d) (m : ℤ) : IsOpen (openCubeAtScale center m)

theorem HCPolySupport.Book.Ch03.measurableSet_openCubeAtScale {d : ℕ} (center : Vec d) (m : ℤ) : MeasurableSet (openCubeAtScale center m)

theorem HCPolySupport.Book.Ch03.openCubeAtScale_eq_pi_Ioo {d : ℕ} (center : Vec d) (m : ℤ) : openCubeAtScale center m = Set.univ.pi fun (i : Fin d) => Set.Ioo (center i - Real.rpow 3 ↑m / 2) (center i + Real.rpow 3 ↑m / 2)

theorem HCPolySupport.Book.Ch03.openCubeAtScale_zero_eq_openCubeSet_originCube {d : ℕ} (m : ℤ) : openCubeAtScale 0 m = openCubeSet (originCube d m)

theorem HCPolySupport.Book.Ch03.openCubeAtScale_eq_translateSet {d : ℕ} (center : Vec d) (m : ℤ) : openCubeAtScale center m = translateSet center (openCubeAtScale 0 m)

theorem HCPolySupport.Book.Ch03.openCubeAtScale_eq_translateSet_smul_originCube_zero {d : ℕ} (center : Vec d) (m : ℤ) : openCubeAtScale center m = translateSet center (cubeScaleFactor (originCube d m) • openCubeAtScale 0 0)

theorem HCPolySupport.Book.Ch03.openCubeAtScale_eq_translateSet_sub {d : ℕ} (z center : Vec d) (m : ℤ) : openCubeAtScale center m = translateSet z (openCubeAtScale (center - z) m)

noncomputable def HCPolySupport.Book.Ch03.boundaryPatchSet {d : ℕ} (Q : TriadicCube d) (x : Vec d) : Set (Vec d)

The boundary patch cu_m ∩ (x + cu_{m-1}) used in the boundary Caccioppoli statement.

Equations

• HCPolySupport.Book.Ch03.boundaryPatchSet Q x = HCPolySupport.openCubeSet Q ∩ HCPolySupport.Book.Ch03.openCubeAtScale x (Q.scale - 1)

theorem HCPolySupport.Book.Ch03.boundaryPatchSet_eq_translateSet_origin {d : ℕ} (Q : TriadicCube d) (x : Vec d) : boundaryPatchSet Q x = translateSet (triadicCubeShift Q) (boundaryPatchSet (originCube d Q.scale) (x - triadicCubeShift Q))

noncomputable def HCPolySupport.Book.Ch03.caccioppoliCoreSet {d : ℕ} (Q : TriadicCube d) (x : Vec d) : Set (Vec d)

The smaller local energy patch cu_m ∩ (x + cu_{m-2}).

Equations

• HCPolySupport.Book.Ch03.caccioppoliCoreSet Q x = HCPolySupport.openCubeSet Q ∩ HCPolySupport.Book.Ch03.openCubeAtScale x (Q.scale - 2)

theorem HCPolySupport.Book.Ch03.measurableSet_caccioppoliCoreSet {d : ℕ} (Q : TriadicCube d) (x : Vec d) : MeasurableSet (caccioppoliCoreSet Q x)

theorem HCPolySupport.Book.Ch03.caccioppoliCoreSet_eq_translateSet_origin {d : ℕ} (Q : TriadicCube d) (x : Vec d) : caccioppoliCoreSet Q x = translateSet (triadicCubeShift Q) (caccioppoliCoreSet (originCube d Q.scale) (x - triadicCubeShift Q))