Coarse-graining support: Support.Besov.Negative.ExactFiniteBridge

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

Finite projected-pairing bridges for the exact Chapter 1 kernels

These lemmas isolate the pieces of the exact kernels that agree literally with the finite projected-pairing infrastructure: normalized cube averages, ordinary descendant-block means, and parent-to-block integrability transport. They deliberately do not identify the extended exact aggregations with the legacy real-valued partial norms.

theorem HCPolySupport.exactOverlapDepthWeight_eq_ofReal_legacy {d : ℕ} (Q : TriadicCube d) (s : ℝ) (j : ℕ) : exactOverlapDepthWeight Q s j = ENNReal.ofReal (cubeBesovOverlapDepthWeight Q s j)

The exact overlap scale weight is the extended embedding of the legacy overlap weight at the same source depth.

theorem HCPolySupport.exactOverlapRootWeight_eq_ofReal_legacy {d : ℕ} (Q : TriadicCube d) (s : ℝ) : exactOverlapRootWeight Q s = ENNReal.ofReal (cubeBesovScaleWeight s Q)

The exact root weight is the extended embedding of the legacy root-scale weight.

theorem HCPolySupport.exactCircDepthWeight_eq_ofReal_legacy {d : ℕ} (Q : TriadicCube d) (s : ℝ) (j : ℕ) : exactCircDepthWeight Q s j = ENNReal.ofReal (cubeBesovCircDepthWeight Q s j)

The exact circ scale weight is the extended embedding of the legacy circ weight at the same source depth.

theorem HCPolySupport.exactCircIntegrable_of_memLp {d : ℕ} (Q : TriadicCube d) (p : ℝ) (hp : 1 ≤ p) {f : Vec d → ℝ} (hf : MeasureTheory.MemLp f (ENNReal.ofReal p) (normalizedCubeMeasure Q)) : ExactCircIntegrable Q f

Parent MemLp data at an admissible finite source exponent gives the certified ordinary descendant-block integrals needed by the exact circ kernel.

theorem HCPolySupport.cubeFluctuation_memLp_of_parent_memLp {d : ℕ} (Q : TriadicCube d) (p : ℝ) {f : Vec d → ℝ} (hf : MeasureTheory.MemLp f (ENNReal.ofReal p) (normalizedCubeMeasure Q)) (j : ℕ) (R : TriadicCube d) (hR : R ∈ descendantsAtDepth Q j) : MeasureTheory.MemLp (cubeFluctuation R f) (ENNReal.ofReal p) (normalizedCubeMeasure R)

Parent MemLp data supplies the local fluctuation premise used by the finite projected-pairing bound on every ordinary descendant block.

theorem HCPolySupport.cubeProjection_memLp_of_parent_descendant {d : ℕ} (Q : TriadicCube d) (p : ℝ) (f : Vec d → ℝ) (k j : ℕ) (R : TriadicCube d) (hR : R ∈ descendantsAtDepth Q j) : MeasureTheory.MemLp (cubeProjection Q k f) (ENNReal.ofReal p) (normalizedCubeMeasure R)

Every finite projection has the local MemLp premise required by the projected-pairing bound after restricting it to an ordinary descendant block.

theorem HCPolySupport.exactDualNormalizedPairing_eq_of_cubeBesovPairing {d : ℕ} (Q : TriadicCube d) (f g : Vec d → ℝ) (hfg : MeasureTheory.Integrable (fun (x : Vec d) => f x * g x) (normalizedCubeMeasure Q)) : exactDualNormalizedPairing Q f g hfg = ENNReal.ofReal |cubeBesovPairing Q f g|

The exact proof-carrying pairing is the absolute value of the legacy cube pairing, embedded in ENNReal; its supplied product-integrability proof rules out any undefined-integral interpretation.

theorem HCPolySupport.exactCircBlockMean_eq_cubeAverage {d : ℕ} (R : TriadicCube d) (f : Vec d → ℝ) (hf : MeasureTheory.Integrable f (normalizedCubeMeasure R)) : exactCircBlockMean R f hf = cubeAverage R f

A certified exact circ block mean is the ordinary normalized cube average used by the finite projected-pairing development.

theorem HCPolySupport.exactOverlapRootMean_eq_cubeAverage {d : ℕ} (Q : TriadicCube d) (u : Vec d → ℝ) (hu : MeasureTheory.Integrable u (normalizedCubeMeasure Q)) : exactOverlapRootMean Q u hu = cubeAverage Q u

The exact positive root mean is the ordinary normalized cube average used by the finite projected-pairing development.

theorem HCPolySupport.exactOverlapLocalMean_eq_scalarOverlapCubeAverage {d : ℕ} (S : TriadicCube d) (u : Vec d → ℝ) (hu : MeasureTheory.Integrable u (ScalarOverlap.normalizedCubeMeasure S)) : exactOverlapLocalMean S u hu = ScalarOverlap.cubeAverage S u

A certified exact overlap mean is the normalized scalar-overlap cube average used by the finite overlap definitions.

theorem HCPolySupport.exactOverlapLocalOscillation_eq_ofReal_cubeBesovOverlapOscillation {d : ℕ} (S : TriadicCube d) (p : ℝ) (u : Vec d → ℝ) (hu : MeasureTheory.Integrable u (ScalarOverlap.normalizedCubeMeasure S)) (hmem : MeasureTheory.MemLp u (ENNReal.ofReal p) (ScalarOverlap.normalizedCubeMeasure S)) : exactOverlapLocalOscillation S (ENNReal.ofReal p) u hu = ENNReal.ofReal (cubeBesovOverlapOscillation S (ENNReal.ofReal p) u)

At a finite exponent, parent/local MemLp makes the exact extended oscillation precisely the ENNReal embedding of its legacy real counterpart.

theorem HCPolySupport.exactOverlapDepthAverage_eq_ofReal_cubeBesovOverlapDepthAverage {d : ℕ} (Q : TriadicCube d) (p : ℝ) (hp : 1 ≤ p) (u : Vec d → ℝ) (hmem : MeasureTheory.MemLp u (ENNReal.ofReal p) (normalizedCubeMeasure Q)) (j : ℕ) : exactOverlapDepthAverage Q p u ⋯ j = ENNReal.ofReal (cubeBesovOverlapDepthAverage Q (ENNReal.ofReal p) u j)

At a finite source exponent, the certified exact overlap depth average is the ENNReal embedding of the legacy finite overlap average.

theorem HCPolySupport.exactOverlapDepthTerm_eq_ofReal_cubeBesovOverlapDepthSeminorm {d : ℕ} (Q : TriadicCube d) (s p : ℝ) (hp : 1 ≤ p) (u : Vec d → ℝ) (hmem : MeasureTheory.MemLp u (ENNReal.ofReal p) (normalizedCubeMeasure Q)) (j : ℕ) : exactOverlapDepthTerm Q s p u ⋯ j = ENNReal.ofReal (cubeBesovOverlapDepthSeminorm Q s (ENNReal.ofReal p) u j)

At a finite source exponent, the certified exact overlap depth term is the ENNReal embedding of the legacy weighted overlap term.

theorem HCPolySupport.exactCircDepthAverage_eq_cubeAverage {d : ℕ} (Q : TriadicCube d) (p : ℝ) (f : Vec d → ℝ) (hf : ExactCircIntegrable Q f) (j : ℕ) : exactCircDepthAverage Q p f hf j = (↑(descendantsAtDepth Q j).card)⁻¹ * ∑ R ∈ (descendantsAtDepth Q j).attach, ENNReal.ofReal |cubeAverage (↑R) f| ^ p

The exact circ depth average has the finite descendant-average formula with legacy normalized cube averages, while retaining its extended value.

theorem HCPolySupport.exactCircDepthAverage_eq_ofReal_cubeBesovCircDepthAverage {d : ℕ} (Q : TriadicCube d) (p : ℝ) (hp : 1 ≤ p) (f : Vec d → ℝ) (hmem : MeasureTheory.MemLp f (ENNReal.ofReal p) (normalizedCubeMeasure Q)) (j : ℕ) : exactCircDepthAverage Q p f ⋯ j = ENNReal.ofReal (cubeBesovCircDepthAverage Q (ENNReal.ofReal p) f j)

At a finite source exponent, the certified exact circ depth average is the ENNReal embedding of the legacy finite circ average.

theorem HCPolySupport.exactCircDepthTerm_eq_ofReal_cubeBesovCircDepthSeminorm {d : ℕ} (Q : TriadicCube d) (s p : ℝ) (hp : 1 ≤ p) (f : Vec d → ℝ) (hmem : MeasureTheory.MemLp f (ENNReal.ofReal p) (normalizedCubeMeasure Q)) (j : ℕ) : exactCircDepthTerm Q s p f ⋯ j = ENNReal.ofReal (cubeBesovCircDepthSeminorm Q s (ENNReal.ofReal p) f j)

At a finite source exponent, the certified exact circ depth term is the ENNReal embedding of the legacy weighted circ term.

theorem HCPolySupport.exactOverlapFiniteNorm_eq_rootCubeAverage {d : ℕ} (P : ExactOverlapFiniteParameters) (Q : TriadicCube d) (u : Vec d → ℝ) (hu : ExactOverlapIntegrable Q u) : exactOverlapFiniteNorm P Q u hu = exactOverlapFiniteSeminorm P Q u hu + exactOverlapRootWeight Q P.s * ENNReal.ofReal |cubeAverage Q u|

The exact finite positive norm has the same root term as the finite projected-pairing norm, with the exact extended seminorm left unchanged.

theorem HCPolySupport.exactOverlapTopNorm_eq_rootCubeAverage {d : ℕ} (P : ExactOverlapTopParameters) (Q : TriadicCube d) (u : Vec d → ℝ) (hu : ExactOverlapIntegrable Q u) : exactOverlapTopNorm P Q u hu = exactOverlapTopSeminorm P Q u hu + exactOverlapRootWeight Q P.s * ENNReal.ofReal |cubeAverage Q u|

The exact positive top norm has the same root term as the finite projected-pairing norm, with the exact extended seminorm left unchanged.