Coarse-graining support: Support.Besov.Positive.ExactOverlap

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

Exact overlapping positive-order Besov kernel

This module is the extended-norm realization of the Chapter 1 positive Besov definition. A natural depth j represents the manuscript scale n = Q.scale - j; thus all n ∈ (-∞, Q.scale] occur exactly once. The overlapping centers are ScalarOverlap.centersAtDepth Q j.

def HCPolySupport.ExactOverlapFiniteAdmissible (s p q : ℝ) : Prop

Admissible finite-q positive Besov parameters. The real-valued exponents are finite by construction, and their ENNReal embeddings are used only where eLpNorm requires an extended exponent.

Equations

• HCPolySupport.ExactOverlapFiniteAdmissible s p q = (0 < s ∧ s < 1 ∧ 1 ≤ p ∧ 1 ≤ q)

def HCPolySupport.ExactOverlapTopAdmissible (s p : ℝ) : Prop

Admissible q = ∞ positive Besov parameters.

Equations

• HCPolySupport.ExactOverlapTopAdmissible s p = (0 < s ∧ s ≤ 1 ∧ 1 ≤ p)

structure HCPolySupport.ExactOverlapFiniteParameters : Type

Finite-q parameters for the exact Chapter 1 overlap Besov kernel.

• s : ℝ

  The positive regularity exponent.

• p : ℝ

  The finite local-integrability exponent.

• q : ℝ

  The finite depth-aggregation exponent.

• admissible : ExactOverlapFiniteAdmissible self.s self.p self.q

structure HCPolySupport.ExactOverlapTopParameters : Type

q = ∞ parameters for the exact Chapter 1 overlap Besov kernel.

• s : ℝ

  The positive regularity exponent.

• p : ℝ

  The finite local-integrability exponent.

• admissible : ExactOverlapTopAdmissible self.s self.p

theorem HCPolySupport.ExactOverlapFiniteParameters.s_pos (P : ExactOverlapFiniteParameters) : 0 < P.s

theorem HCPolySupport.ExactOverlapFiniteParameters.s_lt_one (P : ExactOverlapFiniteParameters) : P.s < 1

theorem HCPolySupport.ExactOverlapFiniteParameters.p_one_le (P : ExactOverlapFiniteParameters) : 1 ≤ P.p

theorem HCPolySupport.ExactOverlapFiniteParameters.q_one_le (P : ExactOverlapFiniteParameters) : 1 ≤ P.q

noncomputable def HCPolySupport.ExactOverlapFiniteParameters.pExponent (P : ExactOverlapFiniteParameters) : ENNReal

The finite real p exponent as an ENNReal exponent for eLpNorm.

Equations

• P.pExponent = ENNReal.ofReal P.p

noncomputable def HCPolySupport.ExactOverlapFiniteParameters.qExponent (P : ExactOverlapFiniteParameters) : ENNReal

The finite real q exponent as an ENNReal exponent.

Equations

• P.qExponent = ENNReal.ofReal P.q

theorem HCPolySupport.ExactOverlapFiniteParameters.pExponent_ne_top (P : ExactOverlapFiniteParameters) : P.pExponent ≠ ⊤

theorem HCPolySupport.ExactOverlapFiniteParameters.qExponent_ne_top (P : ExactOverlapFiniteParameters) : P.qExponent ≠ ⊤

theorem HCPolySupport.ExactOverlapFiniteParameters.one_le_pExponent (P : ExactOverlapFiniteParameters) : 1 ≤ P.pExponent

theorem HCPolySupport.ExactOverlapFiniteParameters.one_le_qExponent (P : ExactOverlapFiniteParameters) : 1 ≤ P.qExponent

theorem HCPolySupport.ExactOverlapTopParameters.s_pos (P : ExactOverlapTopParameters) : 0 < P.s

theorem HCPolySupport.ExactOverlapTopParameters.s_le_one (P : ExactOverlapTopParameters) : P.s ≤ 1

theorem HCPolySupport.ExactOverlapTopParameters.p_one_le (P : ExactOverlapTopParameters) : 1 ≤ P.p

noncomputable def HCPolySupport.ExactOverlapTopParameters.pExponent (P : ExactOverlapTopParameters) : ENNReal

The finite real p exponent as an ENNReal exponent for eLpNorm.

Equations

• P.pExponent = ENNReal.ofReal P.p

theorem HCPolySupport.ExactOverlapTopParameters.pExponent_ne_top (P : ExactOverlapTopParameters) : P.pExponent ≠ ⊤

theorem HCPolySupport.ExactOverlapTopParameters.one_le_pExponent (P : ExactOverlapTopParameters) : 1 ≤ P.pExponent

structure HCPolySupport.ExactOverlapIntegrable {d : ℕ} (Q : TriadicCube d) (u : Vec d → ℝ) : Prop

The integrability data needed to form the source-style root mean and every overlap-local mean. The two measures are kept explicit to prevent the native small cube of a center from being confused with its enlarged overlap cube.

• root : MeasureTheory.Integrable u (normalizedCubeMeasure Q)
• overlap (j : ℕ) (S : TriadicCube d) : S ∈ ScalarOverlap.centersAtDepth Q j → MeasureTheory.Integrable u (ScalarOverlap.normalizedCubeMeasure S)

theorem HCPolySupport.exactOverlapZeroIntegrable {d : ℕ} (Q : TriadicCube d) : ExactOverlapIntegrable Q fun (x : Vec d) => 0

Canonical root and overlap-local integrability data for the zero function.

def HCPolySupport.exactOverlapSourceDepth {d : ℕ} (Q : TriadicCube d) (j : ℕ) : ℤ

The manuscript depth index represented by a natural overlap depth.

Equations

• HCPolySupport.exactOverlapSourceDepth Q j = Q.scale - ↑j

theorem HCPolySupport.exactOverlapSourceDepth_le_scale {d : ℕ} (Q : TriadicCube d) (j : ℕ) : exactOverlapSourceDepth Q j ≤ Q.scale

theorem HCPolySupport.exactOverlapCenters_nonempty {d : ℕ} (Q : TriadicCube d) (j : ℕ) : (ScalarOverlap.centersAtDepth Q j).Nonempty

theorem HCPolySupport.exists_exactOverlapDepth_of_le_scale {d : ℕ} (Q : TriadicCube d) {n : ℤ} (hn : n ≤ Q.scale) : ∃ (j : ℕ), exactOverlapSourceDepth Q j = n

noncomputable def HCPolySupport.exactOverlapDepthWeight {d : ℕ} (Q : TriadicCube d) (s : ℝ) (j : ℕ) : ENNReal

The exact source factor 3^(-n s) at natural depth j, where n = Q.scale - j.

Equations

• HCPolySupport.exactOverlapDepthWeight Q s j = 3 ^ (-↑(HCPolySupport.exactOverlapSourceDepth Q j) * s)

noncomputable def HCPolySupport.exactOverlapRootWeight {d : ℕ} (Q : TriadicCube d) (s : ℝ) : ENNReal

The source root-scale factor 3^(-s m), where m = Q.scale.

Equations

• HCPolySupport.exactOverlapRootWeight Q s = 3 ^ (-↑Q.scale * s)

theorem HCPolySupport.exactOverlapDepthWeight_zero {d : ℕ} (Q : TriadicCube d) (s : ℝ) : exactOverlapDepthWeight Q s 0 = exactOverlapRootWeight Q s

noncomputable def HCPolySupport.exactOverlapRootMean {d : ℕ} (Q : TriadicCube d) (u : Vec d → ℝ) (_hu : MeasureTheory.Integrable u (normalizedCubeMeasure Q)) : ℝ

The source root mean on the ordinary normalized root cube.

Equations

• HCPolySupport.exactOverlapRootMean Q u _hu = ∫ (x : HCPolySupport.Vec d), u x ∂HCPolySupport.normalizedCubeMeasure Q

noncomputable def HCPolySupport.exactOverlapLocalMean {d : ℕ} (S : TriadicCube d) (u : Vec d → ℝ) (_hu : MeasureTheory.Integrable u (ScalarOverlap.normalizedCubeMeasure S)) : ℝ

The source local mean on the enlarged scalar-overlap cube associated to a center. Its integrability certificate prevents any undefined-mean fallback.

Equations

• HCPolySupport.exactOverlapLocalMean S u _hu = ∫ (x : HCPolySupport.Vec d), u x ∂HCPolySupport.ScalarOverlap.normalizedCubeMeasure S

noncomputable def HCPolySupport.exactOverlapLocalOscillation {d : ℕ} (S : TriadicCube d) (p : ENNReal) (u : Vec d → ℝ) (hu : MeasureTheory.Integrable u (ScalarOverlap.normalizedCubeMeasure S)) : ENNReal

The extended normalized local L^p oscillation around the certified cube mean.

Equations

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

noncomputable def HCPolySupport.exactOverlapDepthAverage {d : ℕ} (Q : TriadicCube d) (p : ℝ) (u : Vec d → ℝ) (hu : ExactOverlapIntegrable Q u) (j : ℕ) : ENNReal

Exact finite normalized ℓ^p average of the local overlap oscillations.

Equations

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

noncomputable def HCPolySupport.exactOverlapDepthTerm {d : ℕ} (Q : TriadicCube d) (s p : ℝ) (u : Vec d → ℝ) (hu : ExactOverlapIntegrable Q u) (j : ℕ) : ENNReal

The weighted source depth term. The overlap centers at j encode the source scale n = Q.scale - j.

Equations

• HCPolySupport.exactOverlapDepthTerm Q s p u hu j = HCPolySupport.exactOverlapDepthWeight Q s j * HCPolySupport.exactOverlapDepthAverage Q p u hu j ^ p⁻¹

noncomputable def HCPolySupport.exactOverlapFiniteSeminorm {d : ℕ} (P : ExactOverlapFiniteParameters) (Q : TriadicCube d) (u : Vec d → ℝ) (hu : ExactOverlapIntegrable Q u) : ENNReal

The exact finite-q positive Besov seminorm: the infinite ℓ^q aggregation of the source depth terms, retaining the value ∞.

Equations

• HCPolySupport.exactOverlapFiniteSeminorm P Q u hu = (∑' (j : ℕ), HCPolySupport.exactOverlapDepthTerm Q P.s P.p u hu j ^ P.q) ^ P.q⁻¹

noncomputable def HCPolySupport.exactOverlapTopSeminorm {d : ℕ} (P : ExactOverlapTopParameters) (Q : TriadicCube d) (u : Vec d → ℝ) (hu : ExactOverlapIntegrable Q u) : ENNReal

The exact q = ∞ positive Besov seminorm.

Equations

• HCPolySupport.exactOverlapTopSeminorm P Q u hu = ⨆ (j : ℕ), HCPolySupport.exactOverlapDepthTerm Q P.s P.p u hu j

noncomputable def HCPolySupport.exactOverlapFiniteNorm {d : ℕ} (P : ExactOverlapFiniteParameters) (Q : TriadicCube d) (u : Vec d → ℝ) (hu : ExactOverlapIntegrable Q u) : ENNReal

The exact finite-q inhomogeneous positive Besov norm, including the source root mean term 3^(-s m) |(u)_Q|.

Equations

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

noncomputable def HCPolySupport.exactOverlapTopNorm {d : ℕ} (P : ExactOverlapTopParameters) (Q : TriadicCube d) (u : Vec d → ℝ) (hu : ExactOverlapIntegrable Q u) : ENNReal

The exact q = ∞ inhomogeneous positive Besov norm, including the source root mean term.

Equations

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

theorem HCPolySupport.exactOverlapLocalMean_eq {d : ℕ} (S : TriadicCube d) (u : Vec d → ℝ) (hu : MeasureTheory.Integrable u (ScalarOverlap.normalizedCubeMeasure S)) : exactOverlapLocalMean S u hu = ∫ (x : Vec d), u x ∂ScalarOverlap.normalizedCubeMeasure S

Evaluation of the certified local overlap mean on the enlarged overlap cube.

theorem HCPolySupport.exactOverlapRootMean_zero {d : ℕ} (Q : TriadicCube d) (hu : MeasureTheory.Integrable (fun (x : Vec d) => 0) (normalizedCubeMeasure Q)) : exactOverlapRootMean Q (fun (x : Vec d) => 0) hu = 0

theorem HCPolySupport.exactOverlapLocalOscillation_eq {d : ℕ} (S : TriadicCube d) (p : ENNReal) (u : Vec d → ℝ) (hu : MeasureTheory.Integrable u (ScalarOverlap.normalizedCubeMeasure S)) : exactOverlapLocalOscillation S p u hu = MeasureTheory.eLpNorm (fun (x : Vec d) => u x - exactOverlapLocalMean S u hu) p (ScalarOverlap.normalizedCubeMeasure S)

Evaluation of the certified local overlap oscillation.

theorem HCPolySupport.exactOverlapLocalMean_zero {d : ℕ} (S : TriadicCube d) (hu : MeasureTheory.Integrable (fun (x : Vec d) => 0) (ScalarOverlap.normalizedCubeMeasure S)) : exactOverlapLocalMean S (fun (x : Vec d) => 0) hu = 0

theorem HCPolySupport.exactOverlapLocalOscillation_zero {d : ℕ} (S : TriadicCube d) (p : ENNReal) (hu : MeasureTheory.Integrable (fun (x : Vec d) => 0) (ScalarOverlap.normalizedCubeMeasure S)) : exactOverlapLocalOscillation S p (fun (x : Vec d) => 0) hu = 0

theorem HCPolySupport.exactOverlapLocalOscillation_congr_ae {d : ℕ} (S : TriadicCube d) (p : ENNReal) {u v : Vec d → ℝ} (hu : MeasureTheory.Integrable u (ScalarOverlap.normalizedCubeMeasure S)) (hv : MeasureTheory.Integrable v (ScalarOverlap.normalizedCubeMeasure S)) (huv : u =ᵐ[ScalarOverlap.normalizedCubeMeasure S] v) : exactOverlapLocalOscillation S p u hu = exactOverlapLocalOscillation S p v hv

theorem HCPolySupport.exactOverlapRootMean_congr_ae {d : ℕ} (Q : TriadicCube d) {u v : Vec d → ℝ} (hu : MeasureTheory.Integrable u (normalizedCubeMeasure Q)) (hv : MeasureTheory.Integrable v (normalizedCubeMeasure Q)) (huv : u =ᵐ[normalizedCubeMeasure Q] v) : exactOverlapRootMean Q u hu = exactOverlapRootMean Q v hv

The certified normalized root mean depends only on the root-cube a.e. representative.

theorem HCPolySupport.exactOverlapDepthAverage_congr_ae {d : ℕ} (Q : TriadicCube d) (p : ℝ) {u v : Vec d → ℝ} (hu : ExactOverlapIntegrable Q u) (hv : ExactOverlapIntegrable Q v) (huv : ∀ (j : ℕ), ∀ S ∈ ScalarOverlap.centersAtDepth Q j, u =ᵐ[ScalarOverlap.normalizedCubeMeasure S] v) (j : ℕ) : exactOverlapDepthAverage Q p u hu j = exactOverlapDepthAverage Q p v hv j

A normalized overlap depth average depends only on the a.e. representatives on its enlarged overlap cubes.

theorem HCPolySupport.exactOverlapDepthTerm_congr_ae {d : ℕ} (Q : TriadicCube d) (s p : ℝ) {u v : Vec d → ℝ} (hu : ExactOverlapIntegrable Q u) (hv : ExactOverlapIntegrable Q v) (huv : ∀ (j : ℕ), ∀ S ∈ ScalarOverlap.centersAtDepth Q j, u =ᵐ[ScalarOverlap.normalizedCubeMeasure S] v) (j : ℕ) : exactOverlapDepthTerm Q s p u hu j = exactOverlapDepthTerm Q s p v hv j

A weighted overlap depth term depends only on the a.e. representatives on its enlarged overlap cubes.

theorem HCPolySupport.exactOverlapFiniteSeminorm_congr_ae {d : ℕ} (P : ExactOverlapFiniteParameters) (Q : TriadicCube d) {u v : Vec d → ℝ} (hu : ExactOverlapIntegrable Q u) (hv : ExactOverlapIntegrable Q v) (huv : ∀ (j : ℕ), ∀ S ∈ ScalarOverlap.centersAtDepth Q j, u =ᵐ[ScalarOverlap.normalizedCubeMeasure S] v) : exactOverlapFiniteSeminorm P Q u hu = exactOverlapFiniteSeminorm P Q v hv

The finite-q exact overlap seminorm depends only on the a.e. representatives on every enlarged overlap cube.

theorem HCPolySupport.exactOverlapTopSeminorm_congr_ae {d : ℕ} (P : ExactOverlapTopParameters) (Q : TriadicCube d) {u v : Vec d → ℝ} (hu : ExactOverlapIntegrable Q u) (hv : ExactOverlapIntegrable Q v) (huv : ∀ (j : ℕ), ∀ S ∈ ScalarOverlap.centersAtDepth Q j, u =ᵐ[ScalarOverlap.normalizedCubeMeasure S] v) : exactOverlapTopSeminorm P Q u hu = exactOverlapTopSeminorm P Q v hv

The q = ∞ exact overlap seminorm depends only on the a.e. representatives on every enlarged overlap cube.

theorem HCPolySupport.exactOverlapFiniteNorm_congr_ae {d : ℕ} (P : ExactOverlapFiniteParameters) (Q : TriadicCube d) {u v : Vec d → ℝ} (hu : ExactOverlapIntegrable Q u) (hv : ExactOverlapIntegrable Q v) (hroot : u =ᵐ[normalizedCubeMeasure Q] v) (hoverlap : ∀ (j : ℕ), ∀ S ∈ ScalarOverlap.centersAtDepth Q j, u =ᵐ[ScalarOverlap.normalizedCubeMeasure S] v) : exactOverlapFiniteNorm P Q u hu = exactOverlapFiniteNorm P Q v hv

The finite-q exact overlap norm depends only on the root and overlap-cube a.e. representatives.

theorem HCPolySupport.exactOverlapTopNorm_congr_ae {d : ℕ} (P : ExactOverlapTopParameters) (Q : TriadicCube d) {u v : Vec d → ℝ} (hu : ExactOverlapIntegrable Q u) (hv : ExactOverlapIntegrable Q v) (hroot : u =ᵐ[normalizedCubeMeasure Q] v) (hoverlap : ∀ (j : ℕ), ∀ S ∈ ScalarOverlap.centersAtDepth Q j, u =ᵐ[ScalarOverlap.normalizedCubeMeasure S] v) : exactOverlapTopNorm P Q u hu = exactOverlapTopNorm P Q v hv

The q = ∞ exact overlap norm depends only on the root and overlap-cube a.e. representatives.

theorem HCPolySupport.exactOverlapFiniteDepthAverage_zero {d : ℕ} (P : ExactOverlapFiniteParameters) (Q : TriadicCube d) (j : ℕ) : exactOverlapDepthAverage Q P.p (fun (x : Vec d) => 0) ⋯ j = 0

The local overlap depth average vanishes for zero data at every admissible finite-q exponent.

theorem HCPolySupport.exactOverlapTopDepthAverage_zero {d : ℕ} (P : ExactOverlapTopParameters) (Q : TriadicCube d) (j : ℕ) : exactOverlapDepthAverage Q P.p (fun (x : Vec d) => 0) ⋯ j = 0

The local overlap depth average vanishes for zero data at every admissible q = ∞ exponent.

theorem HCPolySupport.exactOverlapFiniteDepthTerm_zero {d : ℕ} (P : ExactOverlapFiniteParameters) (Q : TriadicCube d) (j : ℕ) : exactOverlapDepthTerm Q P.s P.p (fun (x : Vec d) => 0) ⋯ j = 0

The weighted overlap depth term vanishes for zero data at every admissible finite-q exponent.

theorem HCPolySupport.exactOverlapTopDepthTerm_zero {d : ℕ} (P : ExactOverlapTopParameters) (Q : TriadicCube d) (j : ℕ) : exactOverlapDepthTerm Q P.s P.p (fun (x : Vec d) => 0) ⋯ j = 0

The weighted overlap depth term vanishes for zero data at every admissible q = ∞ exponent.

theorem HCPolySupport.exactOverlapDepthAverage_eq {d : ℕ} (Q : TriadicCube d) (p : ℝ) (u : Vec d → ℝ) (hu : ExactOverlapIntegrable Q u) (j : ℕ) : exactOverlapDepthAverage Q p u hu j = (↑(ScalarOverlap.centersAtDepth Q j).card)⁻¹ * ∑ S ∈ (ScalarOverlap.centersAtDepth Q j).attach, exactOverlapLocalOscillation (↑S) (ENNReal.ofReal p) u ⋯ ^ p

Evaluation of the finite overlap-center average at one source depth.

theorem HCPolySupport.exactOverlapDepthTerm_eq {d : ℕ} (Q : TriadicCube d) (s p : ℝ) (u : Vec d → ℝ) (hu : ExactOverlapIntegrable Q u) (j : ℕ) : exactOverlapDepthTerm Q s p u hu j = exactOverlapDepthWeight Q s j * exactOverlapDepthAverage Q p u hu j ^ p⁻¹

Evaluation of the source-weighted depth term.

theorem HCPolySupport.exactOverlapFiniteSeminorm_eq {d : ℕ} (P : ExactOverlapFiniteParameters) (Q : TriadicCube d) (u : Vec d → ℝ) (hu : ExactOverlapIntegrable Q u) : exactOverlapFiniteSeminorm P Q u hu = (∑' (j : ℕ), exactOverlapDepthTerm Q P.s P.p u hu j ^ P.q) ^ P.q⁻¹

Evaluation of the infinite finite-q aggregation.

theorem HCPolySupport.exactOverlapTopSeminorm_eq {d : ℕ} (P : ExactOverlapTopParameters) (Q : TriadicCube d) (u : Vec d → ℝ) (hu : ExactOverlapIntegrable Q u) : exactOverlapTopSeminorm P Q u hu = ⨆ (j : ℕ), exactOverlapDepthTerm Q P.s P.p u hu j

Evaluation of the q = ∞ aggregation.

theorem HCPolySupport.exactOverlapFiniteNorm_eq {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 |exactOverlapRootMean Q u ⋯|

Evaluation of the finite-q inhomogeneous norm.

theorem HCPolySupport.exactOverlapTopNorm_eq {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 |exactOverlapRootMean Q u ⋯|

Evaluation of the q = ∞ inhomogeneous norm.

theorem HCPolySupport.exactOverlapFiniteSeminorm_zero {d : ℕ} (P : ExactOverlapFiniteParameters) (Q : TriadicCube d) : exactOverlapFiniteSeminorm P Q (fun (x : Vec d) => 0) ⋯ = 0

The exact finite-q overlap seminorm vanishes on the zero function.

theorem HCPolySupport.exactOverlapTopSeminorm_zero {d : ℕ} (P : ExactOverlapTopParameters) (Q : TriadicCube d) : exactOverlapTopSeminorm P Q (fun (x : Vec d) => 0) ⋯ = 0

The exact q = ∞ overlap seminorm vanishes on the zero function.

theorem HCPolySupport.exactOverlapFiniteNorm_zero {d : ℕ} (P : ExactOverlapFiniteParameters) (Q : TriadicCube d) : exactOverlapFiniteNorm P Q (fun (x : Vec d) => 0) ⋯ = 0

The exact finite-q inhomogeneous overlap norm vanishes on zero data.

theorem HCPolySupport.exactOverlapTopNorm_zero {d : ℕ} (P : ExactOverlapTopParameters) (Q : TriadicCube d) : exactOverlapTopNorm P Q (fun (x : Vec d) => 0) ⋯ = 0

The exact q = ∞ inhomogeneous overlap norm vanishes on zero data.

theorem HCPolySupport.exactOverlapLocalOscillation_nonneg {d : ℕ} (S : TriadicCube d) (p : ENNReal) (u : Vec d → ℝ) (hu : MeasureTheory.Integrable u (ScalarOverlap.normalizedCubeMeasure S)) : 0 ≤ exactOverlapLocalOscillation S p u hu

Every extended quantity in the exact overlap kernel is nonnegative.

theorem HCPolySupport.exactOverlapDepthAverage_nonneg {d : ℕ} (Q : TriadicCube d) (p : ℝ) (u : Vec d → ℝ) (hu : ExactOverlapIntegrable Q u) (j : ℕ) : 0 ≤ exactOverlapDepthAverage Q p u hu j

theorem HCPolySupport.exactOverlapFiniteSeminorm_nonneg {d : ℕ} (P : ExactOverlapFiniteParameters) (Q : TriadicCube d) (u : Vec d → ℝ) (hu : ExactOverlapIntegrable Q u) : 0 ≤ exactOverlapFiniteSeminorm P Q u hu

theorem HCPolySupport.exactOverlapTopSeminorm_nonneg {d : ℕ} (P : ExactOverlapTopParameters) (Q : TriadicCube d) (u : Vec d → ℝ) (hu : ExactOverlapIntegrable Q u) : 0 ≤ exactOverlapTopSeminorm P Q u hu

theorem HCPolySupport.exactOverlapFiniteNorm_nonneg {d : ℕ} (P : ExactOverlapFiniteParameters) (Q : TriadicCube d) (u : Vec d → ℝ) (hu : ExactOverlapIntegrable Q u) : 0 ≤ exactOverlapFiniteNorm P Q u hu

theorem HCPolySupport.exactOverlapTopNorm_nonneg {d : ℕ} (P : ExactOverlapTopParameters) (Q : TriadicCube d) (u : Vec d → ℝ) (hu : ExactOverlapIntegrable Q u) : 0 ≤ exactOverlapTopNorm P Q u hu