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

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

One-cube local coarse-graining bridge

This file packages the source weak equation in the half-open cube carrier required by the legacy corrected weak-flux apex. Its source-facing theorem will consume the strict finite-p regularity bridge, while the response-series summability remains internal to the canonical root coefficient family.

theorem HCPolySupport.Book.Ch03.ABK26.ENNReal_ofReal_norm_cubeAverageVec_le_cubeBesovNegativeVectorSeminormTwo {d : ℕ} (R : TriadicCube d) {s : ℝ} (hs : 0 < s) (F : Vec d → Vec d) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure R)) : ENNReal.ofReal ‖cubeAverageVec R F‖ ≤ ENNReal.ofReal (cubeBesovNegativeVectorSeminormTwo R s F)

The norm of a cube average is bounded by the full finite q = 2 negative Besov seminorm whenever the field is locally L².

theorem HCPolySupport.Book.Ch03.ABK26.cubeAverageVec_fluxDefect_eq_of_ae_eq_on_cubeSet {d : ℕ} (R : TriadicCube d) (a b : CoeffField d) (a0 : Mat d) (gradU : Vec d → Vec d) (hab : a =ᵐ[MeasureTheory.volume.restrict (cubeSet R)] b) : cubeAverageVec R (fluxDefect a a0 gradU) = cubeAverageVec R (fluxDefect b a0 gradU)

Replacing a coefficient representative almost everywhere on a cube leaves the average flux defect unchanged.

theorem HCPolySupport.Book.Ch03.ABK26.ENNReal_ofReal_coarseFluxResponseRHSBound_eq_components_of_bddAbove {d : ℕ} (R : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {s : ℝ} (gradU g : Vec d → Vec d) (hs : 0 < s) (hgBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R s N g)) : ENNReal.ofReal (coarseFluxResponseRHSBound R a a0 s gradU g) = ENNReal.ofReal (coarseFluxResponseRHSEnergyBound R a a0 s gradU) + ENNReal.ofReal (coarseFluxResponseRHSResponseCorrectionBound R a a0 s g) + ENNReal.ofReal (coarseFluxResponseRHSWeakFluxCorrectionBound R a s g) + ENNReal.ofReal (coarseFluxResponseRHSPoincareCorrectionBound R a a0 s g)

Expand the nonnegative one-cube response RHS in ℝ≥0∞. This makes its local energy term, q = 1 response-error term, and the two finite-q = 2 forcing/ellipticity terms separately available to a later positive-norm aggregation argument.

noncomputable def HCPolySupport.Book.Ch03.ABK26.localCoarseGrainingOneCubeConstant (d : ℕ) : ℝ

A single explicit dimension-only envelope for the four one-cube terms. The deterministic apex constant is evaluated at the fixed endpoint 1, so this quantity is uniform in every local fractional order.

Equations

• HCPolySupport.Book.Ch03.ABK26.localCoarseGrainingOneCubeConstant d = 64 * ↑d ^ 3 * (HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceFluxApexConstant d 1 + 1)

theorem HCPolySupport.Book.Ch03.ABK26.ENNReal_ofReal_norm_cubeAverageVec_source_fluxDefect_le_legacyApex_of_memCubeEuclideanFullWsp {d : ℕ} [NeZero d] {R : TriadicCube d} {a : Ch02.CoeffOn (Ch02.cubeDomain R)} {u : H1Function (openCubeSet R)} {g : Vec d → Vec d} (sigma0 : ℝ) (hsigma0 : 0 < sigma0) (s s2 : ↑FractionalOrder) (p : FiniteLpExponent) (hp : 2 ≤ p.exponent) (hss2 : ↑s < ↑s2) (hg : MemCubeEuclideanFullWsp R s2 p g) (h : IsForcedEquation R a u g) : ENNReal.ofReal ‖cubeAverageVec R (fluxDefect a.toCoeffField (scalarMatrix sigma0) u.toCubeSet.grad)‖ ≤ ENNReal.ofReal (2 * ZeroTraceDirichletCorrectorData.zeroTraceFluxApexConstant d ↑s * coarseFluxResponseRHSBound R (publicCoeffField R (rootPointwiseCoeffFamily R a)) (scalarMatrix sigma0) (↑s) u.toCubeSet.grad fun (x : Vec d) => -g x)

The source finite-p fractional-Sobolev datum supplies every regularity input of the deterministic one-cube flux estimate. In particular, this public bridge has no auxiliary boundedness, summability, weak-solution, or ellipticity hypotheses: each is constructed internally from CoeffOn and IsForcedEquation.

theorem HCPolySupport.Book.Ch03.ABK26.ENNReal_ofReal_norm_cubeAverageVec_source_fluxDefect_le_legacyApex_components {d : ℕ} [NeZero d] {R : TriadicCube d} {a : Ch02.CoeffOn (Ch02.cubeDomain R)} {u : H1Function (openCubeSet R)} {g : Vec d → Vec d} (sigma0 : ℝ) (hsigma0 : 0 < sigma0) (s s2 : ↑FractionalOrder) (p : FiniteLpExponent) (hp : 2 ≤ p.exponent) (hss2 : ↑s < ↑s2) (hg : MemCubeEuclideanFullWsp R s2 p g) (h : IsForcedEquation R a u g) : ENNReal.ofReal ‖cubeAverageVec R (fluxDefect a.toCoeffField (scalarMatrix sigma0) u.toCubeSet.grad)‖ ≤ ENNReal.ofReal (2 * ZeroTraceDirichletCorrectorData.zeroTraceFluxApexConstant d ↑s) * (ENNReal.ofReal (coarseFluxResponseRHSEnergyBound R (publicCoeffField R (rootPointwiseCoeffFamily R a)) (scalarMatrix sigma0) (↑s) u.toCubeSet.grad) + ENNReal.ofReal (coarseFluxResponseRHSResponseCorrectionBound R (publicCoeffField R (rootPointwiseCoeffFamily R a)) (scalarMatrix sigma0) ↑s fun (x : Vec d) => -g x) + ENNReal.ofReal (coarseFluxResponseRHSWeakFluxCorrectionBound R (publicCoeffField R (rootPointwiseCoeffFamily R a)) ↑s fun (x : Vec d) => -g x) + ENNReal.ofReal (coarseFluxResponseRHSPoincareCorrectionBound R (publicCoeffField R (rootPointwiseCoeffFamily R a)) (scalarMatrix sigma0) ↑s fun (x : Vec d) => -g x))

Exact four-component form of the source one-cube estimate. This is the direct handoff for the finite-p aggregation: the legacy boundedness witness needed to expand the RHS is constructed from the strict source Sobolev carrier, and is not exposed as a public premise.

theorem HCPolySupport.Book.Ch03.ABK26.ENNReal_ofReal_norm_cubeAverageVec_source_fluxDefect_le_localCoarseGrainingOneCube {d : ℕ} [NeZero d] {R : TriadicCube d} {a : Ch02.CoeffOn (Ch02.cubeDomain R)} {u : H1Function (openCubeSet R)} {g : Vec d → Vec d} (sigma0 : ℝ) (hsigma0 : 0 < sigma0) (s s2 : ↑FractionalOrder) (p : FiniteLpExponent) (hp : 2 ≤ p.exponent) (hss2 : ↑s < ↑s2) (hg : MemCubeEuclideanFullWsp R s2 p g) (h : IsForcedEquation R a u g) : ENNReal.ofReal ‖cubeAverageVec R (fluxDefect a.toCoeffField (scalarMatrix sigma0) u.toCubeSet.grad)‖ ≤ ENNReal.ofReal (localCoarseGrainingOneCubeConstant d) * (ENNReal.ofReal (↑s)⁻¹ * ENNReal.ofReal √sigma0 * ENNReal.ofReal (Ch02.HomogenizationErrorOnCube R (↑s) Ch02.MultiscaleExponent.infinity (Ch02.MultiscaleExponent.finite 1) (rootPointwiseCoeffFamily R a) (scalarMatrix sigma0)) * localSymmetricEnergyENorm R a u + ENNReal.ofReal ((↑s).rpow (-(9 / 2))) * (1 + ENNReal.ofReal (Ch02.HomogenizationErrorOnCube R (↑s / 2) Ch02.MultiscaleExponent.infinity (Ch02.MultiscaleExponent.finite 2) (rootPointwiseCoeffFamily R a) (scalarMatrix sigma0)) ^ 2) * ENNReal.ofReal (cubeBesovPositiveVectorSeminormTwo R (↑s) g))

Fully absorbed source-facing one-cube estimate. The q=1 response term and all three ellipticity corrections are internal consequences of the canonical root family; the displayed forcing seminorm has the manuscript sign convention.