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

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

Exact carriers for the Chapter 3 flux-comparison estimate

This module owns the literal fields and quantities in the frozen Armstrong--Kuusi--Loher flux-defect duality statement. In particular, the coefficient argument remains the public a.e. CoeffOn object; pointwise representatives are used only privately to establish the L² certificates.

theorem HCPolySupport.Book.Ch03.ABK26.memLp_hilbertify_normalizedCube_of_memVectorL2_fluxComparisonDefinitions {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_fluxComparisonDefinitions {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_fluxComparisonDefinitions {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.HasCenteredCubeH10Difference {d : ℕ} (m : ℤ) (u v : H1Function (openCubeSet (originCube d m))) : Prop

Function-level zero-trace difference on the centered cube.

Equations

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

def HCPolySupport.Book.Ch03.ABK26.IsCenteredCubeFluxBalanced {d : ℕ} (m : ℤ) (a : Ch02.CoeffOn (Ch02.cubeDomain (originCube d m))) (sigma0 : ℝ) (u v : H1Function (openCubeSet (originCube d m))) : Prop

The flux difference is weakly divergence-free against zero-trace tests.

Equations

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

noncomputable def HCPolySupport.Book.Ch03.ABK26.centeredCubeGradientDifferenceL2Field {d : ℕ} (m : ℤ) (u v : H1Function (openCubeSet (originCube d m))) : CubeEuclideanLpField (originCube d m) FiniteLpExponent.two

The centered-cube gradient difference, bundled with its genuine L² certificate.

Equations

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

noncomputable def HCPolySupport.Book.Ch03.ABK26.centeredCubeFluxDifferenceL2Field {d : ℕ} (m : ℤ) (a : Ch02.CoeffOn (Ch02.cubeDomain (originCube d m))) (sigma0 : ℝ) (u v : H1Function (openCubeSet (originCube d m))) : CubeEuclideanLpField (originCube d m) FiniteLpExponent.two

The centered-cube coefficient/scalar flux difference, bundled with its genuine L² certificate.

Equations

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

noncomputable def HCPolySupport.Book.Ch03.ABK26.centeredCubeLocalFluxDefectL2Field {d : ℕ} (m n : ℤ) (hnm : n < m) (a : Ch02.CoeffOn (Ch02.cubeDomain (originCube d m))) (sigma0 : ℝ) (u : H1Function (openCubeSet (originCube d m))) (R : TriadicCube d) (hR : R ∈ descendantsAtScale (originCube d m) n) : CubeEuclideanLpField R FiniteLpExponent.two

The local scalar-comparator flux defect on a descendant.

Equations

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

noncomputable def HCPolySupport.Book.Ch03.ABK26.centeredCubeLocalFluxDefectSmoothDualLpAverage {d : ℕ} (m n : ℤ) (hnm : n < m) (a : Ch02.CoeffOn (Ch02.cubeDomain (originCube d m))) (sigma0 : ℝ) (u : H1Function (openCubeSet (originCube d m))) (s : ↑FractionalOrder) (p : FiniteLpExponent) : ENNReal

The normalized descendant ell^p average of local smooth-dual flux defects.

Equations

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

noncomputable def HCPolySupport.Book.Ch03.ABK26.centeredCubeFluxComparisonSmoothDualLHS {d : ℕ} (m : ℤ) (a : Ch02.CoeffOn (Ch02.cubeDomain (originCube d m))) (sigma0 : ℝ) (u v : H1Function (openCubeSet (originCube d m))) (s : ↑FractionalOrder) (p : FiniteLpExponent) : ENNReal

The exact left hand side of the centered-cube flux-comparison estimate.

Equations

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