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

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

Explicit overlapping positive Besov seminorms

These definitions implement the scale-local overlapping positive Besov oscillation and the finite-depth overlapping truncations. The full infinite-depth wrappers are the manuscript-facing scalar objects under boundedness/regularity hypotheses, while the unqualified cubeBesov* names above remain the existing disjoint descendant definitions.

noncomputable def HCPolySupport.cubeBesovOverlapOscillation {d : ℕ} (S : TriadicCube d) (p : ENNReal) (u : Vec d → ℝ) : ℝ

The normalized Lᵖ oscillation about the mean on the overlapping cube attached to S.

Equations

• HCPolySupport.cubeBesovOverlapOscillation S p u = HCPolySupport.ScalarOverlap.cubeLpNorm S p fun (x : HCPolySupport.Vec d) => u x - HCPolySupport.ScalarOverlap.cubeAverage S u

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

The average over overlap centers at depth j of Lᵖ oscillations raised to p.toReal.

Equations

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

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

The overlap depth weight, equal to the depth-j side length raised to -s.

Equations

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

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

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

Equations

• HCPolySupport.cubeBesovOverlapDepthSeminorm Q s p u j = HCPolySupport.cubeBesovOverlapDepthWeight Q s j * HCPolySupport.cubeBesovOverlapDepthAverage Q p u j ^ (1 / p.toReal)

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

The q-power aggregation of weighted overlap oscillations at depths zero through N.

Equations

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

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

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

Equations

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

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

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

Equations

• HCPolySupport.cubeBesovOverlapPartialNorm Q s p q N u = HCPolySupport.cubeBesovOverlapPartialSeminorm Q s p q N u + HCPolySupport.cubeBesovScaleWeight s Q * ‖HCPolySupport.cubeAverage Q u‖

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

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

Equations

• HCPolySupport.cubeBesovOverlapPartialNormTop Q s p N u = HCPolySupport.cubeBesovOverlapPartialSeminormTop Q s p N u + HCPolySupport.cubeBesovScaleWeight s Q * ‖HCPolySupport.cubeAverage Q u‖

@[simp]

theorem HCPolySupport.cubeBesovOverlapOscillation_middleChildCube {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (u : Vec d → ℝ) : cubeBesovOverlapOscillation (ScalarOverlap.middleChildCube Q) p u = cubeBesovOscillation Q p u

theorem HCPolySupport.cubeBesovOverlapOscillation_nonneg {d : ℕ} (S : TriadicCube d) (p : ENNReal) (u : Vec d → ℝ) : 0 ≤ cubeBesovOverlapOscillation S p u

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

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

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

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

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

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

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

@[simp]

theorem HCPolySupport.cubeBesovOverlapOscillation_const {d : ℕ} (S : TriadicCube d) (p : ENNReal) (c : ℝ) (hp0 : p ≠ 0) : (cubeBesovOverlapOscillation S p fun (x : Vec d) => c) = 0

theorem HCPolySupport.cubeBesovOverlapOscillation_zero {d : ℕ} (S : TriadicCube d) (p : ENNReal) (hp0 : p ≠ 0) : (cubeBesovOverlapOscillation S p fun (x : Vec d) => 0) = 0

@[simp]

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

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

@[simp]

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

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

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

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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