Coarse-graining support: Support.Book.Ch03.ABK26.LocalCoarseGrainingDefinitions

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

Exact local finite-p coarse-graining carriers

This file owns the source-facing local finite-p coarse-graining definitions from the ABK26 statement. It reuses the canonical running-scale negative Besov seminorm, overlap positive Besov seminorm, and parent-truncated errors.

theorem HCPolySupport.Book.Ch03.ABK26.memLp_hilbertify_normalizedCube_of_memVectorL2_localCoarseGrainingDefinitions {d : ℕ} {Q : TriadicCube d} {F : Vec d → Vec d} (hF : MemVectorL2 (openCubeSet Q) F) : MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (F x)) 2 (normalizedCubeMeasure Q)

theorem HCPolySupport.Book.Ch03.ABK26.memVectorL2_matVecMul_pointwiseCoeffOn_localCoarseGrainingDefinitions {d : ℕ} (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (u : H1Function (openCubeSet Q)) : MemVectorL2 (openCubeSet Q) fun (x : Vec d) => matVecMul (a.toCoeffField x) (u.grad x)

theorem HCPolySupport.Book.Ch03.ABK26.memVectorL2_localFluxDefect_localCoarseGrainingDefinitions {d : ℕ} {Q R : TriadicCube d} (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (hRQ : openCubeSet R ⊆ openCubeSet Q) (sigma0 : ℝ) (u : H1Function (openCubeSet Q)) : MemVectorL2 (openCubeSet R) fun (x : Vec d) => matVecMul (a.toCoeffField x - scalarMatrix sigma0) (u.grad x)

def HCPolySupport.Book.Ch03.ABK26.MemCubeEuclideanFullWsp {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (g : Vec d → Vec d) : Prop

Full finite-p fractional Sobolev membership on a cube.

Equations

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

def HCPolySupport.Book.Ch03.ABK26.IsForcedEquation {d : ℕ} (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (u : H1Function (openCubeSet Q)) (g : Vec d → Vec d) : Prop

Weak form of the heterogeneous forced equation on a cube.

Equations

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

def HCPolySupport.Book.Ch03.ABK26.IsScalarForcedEquation {d : ℕ} (Q : TriadicCube d) (sigma0 : ℝ) (v : H1Function (openCubeSet Q)) (g : Vec d → Vec d) : Prop

Weak form of the scalar-comparator forced equation on a cube.

Equations

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

def HCPolySupport.Book.Ch03.ABK26.HasH10Difference {d : ℕ} (Q : TriadicCube d) (u v : H1Function (openCubeSet Q)) : Prop

Function-level zero-trace difference on an arbitrary cube.

Equations

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

noncomputable def HCPolySupport.Book.Ch03.ABK26.gradientDifferenceL2Field {d : ℕ} (Q : TriadicCube d) (u v : H1Function (openCubeSet Q)) : CubeEuclideanLpField Q FiniteLpExponent.two

The literal gradient difference, bundled with its L² certificate.

Equations

• HCPolySupport.Book.Ch03.ABK26.gradientDifferenceL2Field Q u v = { toField := fun (x : HCPolySupport.Vec d) => u.grad x - v.grad x, euclideanMemLp := ⋯ }

noncomputable def HCPolySupport.Book.Ch03.ABK26.fluxDifferenceL2Field {d : ℕ} (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (sigma0 : ℝ) (u v : H1Function (openCubeSet Q)) : CubeEuclideanLpField Q FiniteLpExponent.two

The literal heterogeneous/scalar flux difference, bundled with L².

Equations

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

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch03.ABK26.cubeEuclideanPositiveBesovOverlapESeminorm {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (g : Vec d → Vec d) : ENNReal

The canonical reusable overlap positive Besov seminorm.

Equations

• HCPolySupport.Book.Ch03.ABK26.cubeEuclideanPositiveBesovOverlapESeminorm Q s p g = HCPolySupport.cubeEuclideanPositiveBesovOverlapESeminorm Q s p g

noncomputable def HCPolySupport.Book.Ch03.ABK26.restrictH1ToSubcube {d : ℕ} {Q R : TriadicCube d} (u : H1Function (openCubeSet Q)) (hRQ : openCubeSet R ⊆ openCubeSet Q) : H1Function (openCubeSet R)

Restriction of an H¹ function to a subcube.

Equations

• HCPolySupport.Book.Ch03.ABK26.restrictH1ToSubcube u hRQ = u.restrict ⋯ hRQ

@[simp]

theorem HCPolySupport.Book.Ch03.ABK26.restrictH1ToSubcube_toFun {d : ℕ} {Q R : TriadicCube d} (u : H1Function (openCubeSet Q)) (hRQ : openCubeSet R ⊆ openCubeSet Q) : (restrictH1ToSubcube u hRQ).toFun = u.toFun

@[simp]

theorem HCPolySupport.Book.Ch03.ABK26.restrictH1ToSubcube_grad {d : ℕ} {Q R : TriadicCube d} (u : H1Function (openCubeSet Q)) (hRQ : openCubeSet R ⊆ openCubeSet Q) : (restrictH1ToSubcube u hRQ).grad = u.grad

noncomputable def HCPolySupport.Book.Ch03.ABK26.localSymmetricEnergyENorm {d : ℕ} (R : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain R)) (u : H1Function (openCubeSet R)) : ENNReal

The normalized symmetric local energy.

Equations

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

noncomputable def HCPolySupport.Book.Ch03.ABK26.weightedLocalSymmetricEnergyLp {d : ℕ} (Q : TriadicCube d) (n : ℤ) (hn : n ≤ Q.scale) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (u : H1Function (openCubeSet Q)) (s1 s : ↑FractionalOrder) (p : FiniteLpExponent) : ENNReal

The weighted descendant ell^p aggregation of local symmetric energies.

Equations

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

noncomputable def HCPolySupport.Book.Ch03.ABK26.localFluxDefectL2Field {d : ℕ} {Q R : TriadicCube d} (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (hRQ : openCubeSet R ⊆ openCubeSet Q) (sigma0 : ℝ) (u : H1Function (openCubeSet Q)) : CubeEuclideanLpField R FiniteLpExponent.two

The local scalar-comparator flux defect on a subcube.

Equations

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

noncomputable def HCPolySupport.Book.Ch03.ABK26.localFluxDefectNegativeBesovLpAverage {d : ℕ} (Q : TriadicCube d) (n : ℤ) (hn : n ≤ Q.scale) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (sigma0 : ℝ) (u : H1Function (openCubeSet Q)) (s : ↑FractionalOrder) (p : FiniteLpExponent) : ENNReal

The normalized ell^p average of descendant negative Besov flux defects.

Equations

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

noncomputable def HCPolySupport.Book.Ch03.ABK26.localCoarseGrainingLpRHS {d : ℕ} (C : ENNReal) (Q : TriadicCube d) (n : ℤ) (hn : n ≤ Q.scale) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (sigma0 : ℝ) (hsigma0 : 0 < sigma0) (g : Vec d → Vec d) (u : H1Function (openCubeSet Q)) (s1 s s2 : ↑FractionalOrder) (p : FiniteLpExponent) : ENNReal

The exact right-hand side of the local finite-p coarse-graining bound.

Equations

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