Coarse-graining support: Support.Besov.Positive

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

Finite disjoint positive-order cube Besov seminorms.

This file intentionally contains only the descendant-based positive Besov core. Scalar overlap definitions and full sSup wrappers live in narrow downstream modules so ordinary importers of Besov.Positive do not pay for overlap geometry.

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

The average over depth-j descendants of normalized Lᵖ oscillations raised to p.toReal.

Equations

• HCPolySupport.cubeBesovDepthAverage Q p u j = HCPolySupport.descendantsAverage Q j fun (R : HCPolySupport.TriadicCube d) => HCPolySupport.cubeBesovOscillation R p u ^ p.toReal

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

The side length at depth j raised to -s.

Equations

• HCPolySupport.cubeBesovDepthWeight Q s j = (HCPolySupport.cubeScaleFactor Q / 3 ^ j) ^ (-s)

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

The p-power mean of descendant oscillations multiplied by the depth weight.

Equations

• HCPolySupport.cubeBesovDepthSeminorm Q s p u j = HCPolySupport.cubeBesovDepthWeight Q s j * HCPolySupport.cubeBesovDepthAverage Q p u j ^ (1 / p.toReal)

noncomputable def HCPolySupport.cubeBesovPartialSeminorm {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (u : Vec d → ℝ) : ℝ

The q-power sum of weighted oscillations at depths zero through N, to power 1/q.

Equations

• HCPolySupport.cubeBesovPartialSeminorm Q s p q N u = (∑ j ∈ Finset.range (N + 1), HCPolySupport.cubeBesovDepthSeminorm Q s p u j ^ q.toReal) ^ (1 / q.toReal)

noncomputable def HCPolySupport.cubeBesovPartialSeminormTop {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (N : ℕ) (u : Vec d → ℝ) : ℝ

The maximum of the weighted oscillations at depths zero through N.

Equations

• HCPolySupport.cubeBesovPartialSeminormTop Q s p N u = (Finset.range (N + 1)).sup' ⋯ fun (j : ℕ) => HCPolySupport.cubeBesovDepthSeminorm Q s p u j

noncomputable def HCPolySupport.cubeBesovPartialNorm {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (u : Vec d → ℝ) : ℝ

The finite Besov seminorm plus the absolute parent mean weighted by side length to -s.

Equations

• HCPolySupport.cubeBesovPartialNorm Q s p q N u = HCPolySupport.cubeBesovPartialSeminorm Q s p q N u + HCPolySupport.cubeBesovScaleWeight s Q * ‖HCPolySupport.cubeAverage Q u‖

noncomputable def HCPolySupport.cubeBesovPartialNormTop {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (N : ℕ) (u : Vec d → ℝ) : ℝ

The maximum-aggregation Besov seminorm plus the weighted absolute parent mean.

Equations

• HCPolySupport.cubeBesovPartialNormTop Q s p N u = HCPolySupport.cubeBesovPartialSeminormTop Q s p N u + HCPolySupport.cubeBesovScaleWeight s Q * ‖HCPolySupport.cubeAverage Q u‖

Explicit disjoint positive Besov names

These names disambiguate the legacy descendant-based positive Besov pieces from the overlap-based cubeBesovOverlap* family in downstream modules. The unqualified cubeBesov* names remain as compatibility aliases for existing theorem statements until the public API flip gate.

@[reducible, inline]

noncomputable abbrev HCPolySupport.cubeBesovDisjointDepthAverage {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (u : Vec d → ℝ) (j : ℕ) : ℝ

The disjoint-descendant average of normalized Lᵖ oscillations raised to p.toReal.

Equations

• HCPolySupport.cubeBesovDisjointDepthAverage Q p u j = HCPolySupport.cubeBesovDepthAverage Q p u j

@[reducible, inline]

noncomputable abbrev HCPolySupport.cubeBesovDisjointDepthWeight {d : ℕ} (Q : TriadicCube d) (s : ℝ) (j : ℕ) : ℝ

The disjoint depth weight, equal to the descendant side length raised to -s.

Equations

• HCPolySupport.cubeBesovDisjointDepthWeight Q s j = HCPolySupport.cubeBesovDepthWeight Q s j

@[reducible, inline]

noncomputable abbrev HCPolySupport.cubeBesovDisjointDepthSeminorm {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (u : Vec d → ℝ) (j : ℕ) : ℝ

The weighted p-power mean of disjoint-descendant oscillations at depth j.

Equations

• HCPolySupport.cubeBesovDisjointDepthSeminorm Q s p u j = HCPolySupport.cubeBesovDepthSeminorm Q s p u j

@[reducible, inline]

noncomputable abbrev HCPolySupport.cubeBesovDisjointPartialSeminorm {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (u : Vec d → ℝ) : ℝ

The q-power aggregation of disjoint depth oscillations through depth N.

Equations

• HCPolySupport.cubeBesovDisjointPartialSeminorm Q s p q N u = HCPolySupport.cubeBesovPartialSeminorm Q s p q N u

@[reducible, inline]

noncomputable abbrev HCPolySupport.cubeBesovDisjointPartialSeminormTop {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (N : ℕ) (u : Vec d → ℝ) : ℝ

The maximum of the disjoint depth oscillations through depth N.

Equations

• HCPolySupport.cubeBesovDisjointPartialSeminormTop Q s p N u = HCPolySupport.cubeBesovPartialSeminormTop Q s p N u

@[reducible, inline]

noncomputable abbrev HCPolySupport.cubeBesovDisjointPartialNorm {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (u : Vec d → ℝ) : ℝ

The disjoint finite seminorm plus the absolute parent mean weighted by side length to -s.

Equations

• HCPolySupport.cubeBesovDisjointPartialNorm Q s p q N u = HCPolySupport.cubeBesovPartialNorm Q s p q N u

@[reducible, inline]

noncomputable abbrev HCPolySupport.cubeBesovDisjointPartialNormTop {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (N : ℕ) (u : Vec d → ℝ) : ℝ

The disjoint maximum-aggregation seminorm plus the weighted absolute parent mean.

Equations

• HCPolySupport.cubeBesovDisjointPartialNormTop Q s p N u = HCPolySupport.cubeBesovPartialNormTop Q s p N u

@[simp]

theorem HCPolySupport.cubeBesovDepthAverage_depth_zero {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (u : Vec d → ℝ) : cubeBesovDepthAverage Q p u 0 = cubeBesovOscillation Q p u ^ p.toReal

@[simp]

theorem HCPolySupport.cubeBesovDepthWeight_depth_zero {d : ℕ} (Q : TriadicCube d) (s : ℝ) : cubeBesovDepthWeight Q s 0 = cubeBesovScaleWeight s Q

theorem HCPolySupport.cubeBesovDepthAverage_nonneg {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (u : Vec d → ℝ) (j : ℕ) : 0 ≤ cubeBesovDepthAverage Q p u j

theorem HCPolySupport.cubeBesovDepthWeight_nonneg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (j : ℕ) : 0 ≤ cubeBesovDepthWeight Q s j

theorem HCPolySupport.cubeBesovDepthSeminorm_nonneg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (u : Vec d → ℝ) (j : ℕ) : 0 ≤ cubeBesovDepthSeminorm Q s p u j

theorem HCPolySupport.cubeBesovPartialSeminorm_nonneg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (u : Vec d → ℝ) : 0 ≤ cubeBesovPartialSeminorm Q s p q N u

theorem HCPolySupport.cubeBesovPartialSeminormTop_nonneg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (N : ℕ) (u : Vec d → ℝ) : 0 ≤ cubeBesovPartialSeminormTop Q s p N u

theorem HCPolySupport.cubeBesovPartialNorm_nonneg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (u : Vec d → ℝ) : 0 ≤ cubeBesovPartialNorm Q s p q N u

theorem HCPolySupport.cubeBesovPartialNormTop_nonneg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (N : ℕ) (u : Vec d → ℝ) : 0 ≤ cubeBesovPartialNormTop Q s p N u

theorem HCPolySupport.cubeBesovPartialSeminorm_mono_N {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (u : Vec d → ℝ) (hq : 0 < q.toReal) : Monotone fun (N : ℕ) => cubeBesovPartialSeminorm Q s p q N u

theorem HCPolySupport.cubeBesovPartialSeminormTop_mono_N {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (u : Vec d → ℝ) : Monotone fun (N : ℕ) => cubeBesovPartialSeminormTop Q s p N u

theorem HCPolySupport.cubeBesovPartialNorm_mono_N {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (u : Vec d → ℝ) (hq : 0 < q.toReal) : Monotone fun (N : ℕ) => cubeBesovPartialNorm Q s p q N u

theorem HCPolySupport.cubeBesovPartialNormTop_mono_N {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (u : Vec d → ℝ) : Monotone fun (N : ℕ) => cubeBesovPartialNormTop Q s p N u

@[simp]

theorem HCPolySupport.cubeBesovDepthAverage_const {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (u : ℝ) (j : ℕ) (hp0 : p ≠ 0) (hpTop : p ≠ ⊤) : cubeBesovDepthAverage Q p (fun (x : Vec d) => u) j = 0

theorem HCPolySupport.cubeBesovDepthAverage_zero {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (j : ℕ) (hp0 : p ≠ 0) (hpTop : p ≠ ⊤) : cubeBesovDepthAverage Q p (fun (x : Vec d) => 0) j = 0

@[simp]

theorem HCPolySupport.cubeBesovDepthSeminorm_const {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (u : ℝ) (j : ℕ) (hp0 : p ≠ 0) (hpTop : p ≠ ⊤) : cubeBesovDepthSeminorm Q s p (fun (x : Vec d) => u) j = 0

theorem HCPolySupport.cubeBesovDepthSeminorm_zero {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (j : ℕ) (hp0 : p ≠ 0) (hpTop : p ≠ ⊤) : cubeBesovDepthSeminorm Q s p (fun (x : Vec d) => 0) j = 0

@[simp]

theorem HCPolySupport.cubeBesovPartialSeminorm_const {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (u : ℝ) (hp0 : p ≠ 0) (hpTop : p ≠ ⊤) (hq0 : q ≠ 0) (hqTop : q ≠ ⊤) : (cubeBesovPartialSeminorm Q s p q N fun (x : Vec d) => u) = 0

theorem HCPolySupport.cubeBesovPartialSeminorm_zero {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (hp0 : p ≠ 0) (hpTop : p ≠ ⊤) (hq0 : q ≠ 0) (hqTop : q ≠ ⊤) : (cubeBesovPartialSeminorm Q s p q N fun (x : Vec d) => 0) = 0

@[simp]

theorem HCPolySupport.cubeBesovPartialSeminormTop_const {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (N : ℕ) (u : ℝ) (hp0 : p ≠ 0) (hpTop : p ≠ ⊤) : (cubeBesovPartialSeminormTop Q s p N fun (x : Vec d) => u) = 0

theorem HCPolySupport.cubeBesovPartialSeminormTop_zero {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (N : ℕ) (hp0 : p ≠ 0) (hpTop : p ≠ ⊤) : (cubeBesovPartialSeminormTop Q s p N fun (x : Vec d) => 0) = 0

@[simp]

theorem HCPolySupport.cubeBesovPartialNorm_const {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (u : ℝ) (hp0 : p ≠ 0) (hpTop : p ≠ ⊤) (hq0 : q ≠ 0) (hqTop : q ≠ ⊤) : (cubeBesovPartialNorm Q s p q N fun (x : Vec d) => u) = cubeBesovScaleWeight s Q * ‖u‖

theorem HCPolySupport.cubeBesovPartialNorm_zero {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (hp0 : p ≠ 0) (hpTop : p ≠ ⊤) (hq0 : q ≠ 0) (hqTop : q ≠ ⊤) : (cubeBesovPartialNorm Q s p q N fun (x : Vec d) => 0) = 0

@[simp]

theorem HCPolySupport.cubeBesovPartialNormTop_const {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (N : ℕ) (u : ℝ) (hp0 : p ≠ 0) (hpTop : p ≠ ⊤) : (cubeBesovPartialNormTop Q s p N fun (x : Vec d) => u) = cubeBesovScaleWeight s Q * ‖u‖

theorem HCPolySupport.cubeBesovPartialNormTop_zero {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (N : ℕ) (hp0 : p ≠ 0) (hpTop : p ≠ ⊤) : (cubeBesovPartialNormTop Q s p N fun (x : Vec d) => 0) = 0