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

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

Finite-p forcing aggregation for local coarse graining

This module isolates the source forcing term before it is combined with the PDE or response estimates. Its physical-scale index is written as n - j: thus j is exactly the source depth below the prescribed scale n.

noncomputable def HCPolySupport.Book.Ch03.ABK26.localCoarseGrainingForcingPowerEnergy {d : ℕ} (Q : TriadicCube d) (n : ℤ) (s1 s : ↑FractionalOrder) (p : FiniteLpExponent) (g : Vec d → Vec d) : ENNReal

The unrooted finite-p forcing aggregation. At outer depth j, this uses the normalized average of the legacy local positive q = 2 seminorms over cubes at physical scale n - j; the coefficient is the manuscript's 3^((s₁-s) p j).

Equations

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

noncomputable def HCPolySupport.Book.Ch03.ABK26.localCoarseGrainingForcingLp {d : ℕ} (Q : TriadicCube d) (n : ℤ) (s1 s : ↑FractionalOrder) (p : FiniteLpExponent) (g : Vec d → Vec d) : ENNReal

The source normalized ell^p forcing aggregation, obtained by taking the single outer finite-p root of localCoarseGrainingForcingPowerEnergy.

Equations

• HCPolySupport.Book.Ch03.ABK26.localCoarseGrainingForcingLp Q n s1 s p g = HCPolySupport.Book.Ch03.ABK26.localCoarseGrainingForcingPowerEnergy Q n s1 s p g ^ p.exponent.toReal⁻¹

theorem HCPolySupport.Book.Ch03.ABK26.localCoarseGrainingForcingLp_rpow_eq_powerEnergy {d : ℕ} (Q : TriadicCube d) (n : ℤ) (s1 s : ↑FractionalOrder) (p : FiniteLpExponent) (g : Vec d → Vec d) : localCoarseGrainingForcingLp Q n s1 s p g ^ p.exponent.toReal = localCoarseGrainingForcingPowerEnergy Q n s1 s p g

Raising the rooted forcing carrier back to the finite exponent recovers its literal unrooted physical-scale series.

The next finite-sum estimate is the Hölder core of the local L²-to-Lᵖ conversion. It is deliberately stated before any cube geometry: the cube-specific proof will instantiate w with the fractional-order gap discount and a with local oscillation averages.

theorem HCPolySupport.Book.Ch03.ABK26.MemCubeEuclideanFullWsp.memLpTwo {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} {g : Vec d → Vec d} (hp : 2 ≤ p.exponent) (hg : MemCubeEuclideanFullWsp Q s p g) : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)

The finite Euclidean carrier supplies the legacy normalized cube L² membership used by the existing one-cube weak-flux theorem. This is a carrier conversion only: it does not make any pointwise choice of a representative.

theorem HCPolySupport.Book.Ch03.ABK26.cubeBesovPositiveVectorSeminormTwo_le_five_mul_gap_inv_mul_scale_mul_disjointRoot {d : ℕ} (Q : TriadicCube d) (s s2 : ↑FractionalOrder) (hss2 : ↑s < ↑s2) (p : FiniteLpExponent) (hp : 2 ≤ p.exponent) (g : Vec d → Vec d) (hg : MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (g x)) p.exponent (normalizedCubeMeasure Q)) : ENNReal.ofReal (cubeBesovPositiveVectorSeminormTwo Q (↑s) g) ≤ 5 * ENNReal.ofReal (↑s2 - ↑s)⁻¹ * ENNReal.ofReal (Real.rpow 3 (↑s2 * ↑Q.scale)) * cubeEuclideanPositiveBesovDisjointPowerEnergy Q s2 p g ^ p.exponent.toReal⁻¹

The source-facing positive-Besov bridge from the legacy finite-2 seminorm to the internal disjoint finite-p energy. No boundedness or summability premise is exposed: the infinite-energy case is discharged in ENNReal, and the finite case uses uniform finite partial bounds.

theorem HCPolySupport.Book.Ch03.ABK26.cubeBesovPositiveVectorPartialSeminormTwo_bddAbove_of_memLp_finiteP {d : ℕ} [NeZero d] (Q : TriadicCube d) (s s2 : ↑FractionalOrder) (hss2 : ↑s < ↑s2) (p : FiniteLpExponent) (hp : 2 ≤ p.exponent) (g : Vec d → Vec d) (hgFull : MemCubeEuclideanFullWsp Q s2 p g) : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q (↑s) N g)

The finite Euclidean source carrier makes the legacy finite partial positive-Besov seminorms uniformly bounded. The finite-energy conclusion is derived from the source-facing full W^{s₂,p} hypothesis, rather than being silently assumed as a bare MemLp consequence.

theorem HCPolySupport.Book.Ch03.ABK26.localCoarseGrainingForcingLp_le_five_mul_gap_inv_mul_scale_mul_overlap {d : ℕ} [NeZero d] (Q : TriadicCube d) (n : ℤ) (hn : n ≤ Q.scale) (s1 s s2 : ↑FractionalOrder) (hs1s : ↑s1 < ↑s) (hss2 : ↑s < ↑s2) (p : FiniteLpExponent) (hp : 2 ≤ p.exponent) (g : Vec d → Vec d) (hg : MemCubeEuclideanFullWsp Q s2 p g) : localCoarseGrainingForcingLp Q n s1 s p g ≤ 5 * 3 ^ d * ENNReal.ofReal (↑s2 - ↑s)⁻¹ * ENNReal.ofReal (Real.rpow 3 (↑s2 * ↑n)) * cubeEuclideanPositiveBesovOverlapESeminorm Q s2 p g

The global finite-p forcing aggregation has exactly one inverse fractional gap. The calculation is internalized through disjoint descendant energies, then returned to the source-facing exact-overlap seminorm.