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

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

Full positive Besov wrappers

The following value sets record all finite-depth truncations. The full seminorm wrappers use sSup; the overlap full norm wrappers are defined as full seminorm plus the fixed parent mean term. Since the codomain is ℝ, boundedness is recorded separately in regularity packages whenever a theorem needs these full wrappers to behave as finite norms.

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

The set of disjoint Besov seminorm truncations over all depths.

Equations

• HCPolySupport.cubeBesovDisjointSeminormValueSet Q s p q u = Set.range fun (N : ℕ) => HCPolySupport.cubeBesovDisjointPartialSeminorm Q s p q N u

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

The real supremum of all disjoint Besov seminorm truncations.

Equations

• HCPolySupport.cubeBesovDisjointSeminorm Q s p q u = sSup (HCPolySupport.cubeBesovDisjointSeminormValueSet Q s p q u)

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

The set of disjoint maximum-aggregation seminorm truncations over all depths.

Equations

• HCPolySupport.cubeBesovDisjointSeminormTopValueSet Q s p u = Set.range fun (N : ℕ) => HCPolySupport.cubeBesovDisjointPartialSeminormTop Q s p N u

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

The real supremum of all disjoint maximum-aggregation seminorm truncations.

Equations

• HCPolySupport.cubeBesovDisjointSeminormTop Q s p u = sSup (HCPolySupport.cubeBesovDisjointSeminormTopValueSet Q s p u)

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

The set of disjoint Besov norm truncations, including the weighted parent mean.

Equations

• HCPolySupport.cubeBesovDisjointNormValueSet Q s p q u = Set.range fun (N : ℕ) => HCPolySupport.cubeBesovDisjointPartialNorm Q s p q N u

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

The real supremum of all disjoint Besov norm truncations.

Equations

• HCPolySupport.cubeBesovDisjointNorm Q s p q u = sSup (HCPolySupport.cubeBesovDisjointNormValueSet Q s p q u)

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

The set of disjoint maximum-aggregation norm truncations over all depths.

Equations

• HCPolySupport.cubeBesovDisjointNormTopValueSet Q s p u = Set.range fun (N : ℕ) => HCPolySupport.cubeBesovDisjointPartialNormTop Q s p N u

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

The real supremum of all disjoint maximum-aggregation norm truncations.

Equations

• HCPolySupport.cubeBesovDisjointNormTop Q s p u = sSup (HCPolySupport.cubeBesovDisjointNormTopValueSet Q s p u)

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

The set of overlapping Besov seminorm truncations over all depths.

Equations

• HCPolySupport.cubeBesovOverlapSeminormValueSet Q s p q u = Set.range fun (N : ℕ) => HCPolySupport.cubeBesovOverlapPartialSeminorm Q s p q N u

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

The real supremum of all overlapping Besov seminorm truncations.

Equations

• HCPolySupport.cubeBesovOverlapSeminorm Q s p q u = sSup (HCPolySupport.cubeBesovOverlapSeminormValueSet Q s p q u)

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

The set of overlapping maximum-aggregation seminorm truncations over all depths.

Equations

• HCPolySupport.cubeBesovOverlapSeminormTopValueSet Q s p u = Set.range fun (N : ℕ) => HCPolySupport.cubeBesovOverlapPartialSeminormTop Q s p N u

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

The real supremum of all overlapping maximum-aggregation seminorm truncations.

Equations

• HCPolySupport.cubeBesovOverlapSeminormTop Q s p u = sSup (HCPolySupport.cubeBesovOverlapSeminormTopValueSet Q s p u)

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

The set of overlapping Besov norm truncations, including the weighted parent mean.

Equations

• HCPolySupport.cubeBesovOverlapNormValueSet Q s p q u = Set.range fun (N : ℕ) => HCPolySupport.cubeBesovOverlapPartialNorm Q s p q N u

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

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

Equations

• HCPolySupport.cubeBesovOverlapNorm Q s p q u = HCPolySupport.cubeBesovOverlapSeminorm Q s p q u + HCPolySupport.cubeBesovScaleWeight s Q * ‖HCPolySupport.cubeAverage Q u‖

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

The set of overlapping maximum-aggregation norm truncations over all depths.

Equations

• HCPolySupport.cubeBesovOverlapNormTopValueSet Q s p u = Set.range fun (N : ℕ) => HCPolySupport.cubeBesovOverlapPartialNormTop Q s p N u

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

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

Equations

• HCPolySupport.cubeBesovOverlapNormTop Q s p u = HCPolySupport.cubeBesovOverlapSeminormTop Q s p u + HCPolySupport.cubeBesovScaleWeight s Q * ‖HCPolySupport.cubeAverage Q u‖

structure HCPolySupport.CubeBesovDisjointRegularity {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (u : Vec d → ℝ) : Prop

Boundedness above of all disjoint Besov seminorm truncations.

• partialSeminorms_bddAbove : BddAbove (cubeBesovDisjointSeminormValueSet Q s p q u)

structure HCPolySupport.CubeBesovDisjointRegularityTop {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (u : Vec d → ℝ) : Prop

Boundedness above of all disjoint maximum-aggregation seminorm truncations.

• partialSeminorms_bddAbove : BddAbove (cubeBesovDisjointSeminormTopValueSet Q s p u)

structure HCPolySupport.CubeBesovOverlapRegularity {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (u : Vec d → ℝ) : Prop

Boundedness above of all overlapping Besov seminorm truncations.

• partialSeminorms_bddAbove : BddAbove (cubeBesovOverlapSeminormValueSet Q s p q u)

structure HCPolySupport.CubeBesovOverlapRegularityTop {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (u : Vec d → ℝ) : Prop

Boundedness above of all overlapping maximum-aggregation seminorm truncations.

• partialSeminorms_bddAbove : BddAbove (cubeBesovOverlapSeminormTopValueSet Q s p u)

theorem HCPolySupport.CubeBesovDisjointRegularity.seminormValueSet_bddAbove {d : ℕ} {Q : TriadicCube d} {s : ℝ} {p q : ENNReal} {u : Vec d → ℝ} (hu : CubeBesovDisjointRegularity Q s p q u) : BddAbove (cubeBesovDisjointSeminormValueSet Q s p q u)

theorem HCPolySupport.CubeBesovDisjointRegularityTop.seminormValueSet_bddAbove {d : ℕ} {Q : TriadicCube d} {s : ℝ} {p : ENNReal} {u : Vec d → ℝ} (hu : CubeBesovDisjointRegularityTop Q s p u) : BddAbove (cubeBesovDisjointSeminormTopValueSet Q s p u)

theorem HCPolySupport.CubeBesovOverlapRegularity.seminormValueSet_bddAbove {d : ℕ} {Q : TriadicCube d} {s : ℝ} {p q : ENNReal} {u : Vec d → ℝ} (hu : CubeBesovOverlapRegularity Q s p q u) : BddAbove (cubeBesovOverlapSeminormValueSet Q s p q u)

theorem HCPolySupport.CubeBesovOverlapRegularityTop.seminormValueSet_bddAbove {d : ℕ} {Q : TriadicCube d} {s : ℝ} {p : ENNReal} {u : Vec d → ℝ} (hu : CubeBesovOverlapRegularityTop Q s p u) : BddAbove (cubeBesovOverlapSeminormTopValueSet Q s p u)

theorem HCPolySupport.cubeBesovDisjointSeminormValueSet_nonempty {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (u : Vec d → ℝ) : (cubeBesovDisjointSeminormValueSet Q s p q u).Nonempty

theorem HCPolySupport.cubeBesovDisjointSeminormTopValueSet_nonempty {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (u : Vec d → ℝ) : (cubeBesovDisjointSeminormTopValueSet Q s p u).Nonempty

theorem HCPolySupport.cubeBesovDisjointNormValueSet_nonempty {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (u : Vec d → ℝ) : (cubeBesovDisjointNormValueSet Q s p q u).Nonempty

theorem HCPolySupport.cubeBesovDisjointNormTopValueSet_nonempty {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (u : Vec d → ℝ) : (cubeBesovDisjointNormTopValueSet Q s p u).Nonempty

theorem HCPolySupport.cubeBesovOverlapSeminormValueSet_nonempty {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (u : Vec d → ℝ) : (cubeBesovOverlapSeminormValueSet Q s p q u).Nonempty

theorem HCPolySupport.cubeBesovOverlapSeminormTopValueSet_nonempty {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (u : Vec d → ℝ) : (cubeBesovOverlapSeminormTopValueSet Q s p u).Nonempty

theorem HCPolySupport.cubeBesovOverlapNormValueSet_nonempty {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (u : Vec d → ℝ) : (cubeBesovOverlapNormValueSet Q s p q u).Nonempty

theorem HCPolySupport.cubeBesovOverlapNormTopValueSet_nonempty {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (u : Vec d → ℝ) : (cubeBesovOverlapNormTopValueSet Q s p u).Nonempty

theorem HCPolySupport.cubeBesovDisjointNormValueSet_bddAbove_of_seminormValueSet_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (u : Vec d → ℝ) (hBdd : BddAbove (cubeBesovDisjointSeminormValueSet Q s p q u)) : BddAbove (cubeBesovDisjointNormValueSet Q s p q u)

theorem HCPolySupport.cubeBesovDisjointNormTopValueSet_bddAbove_of_seminormValueSet_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (u : Vec d → ℝ) (hBdd : BddAbove (cubeBesovDisjointSeminormTopValueSet Q s p u)) : BddAbove (cubeBesovDisjointNormTopValueSet Q s p u)

theorem HCPolySupport.cubeBesovOverlapNormValueSet_bddAbove_of_seminormValueSet_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (u : Vec d → ℝ) (hBdd : BddAbove (cubeBesovOverlapSeminormValueSet Q s p q u)) : BddAbove (cubeBesovOverlapNormValueSet Q s p q u)

theorem HCPolySupport.cubeBesovOverlapNormTopValueSet_bddAbove_of_seminormValueSet_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (u : Vec d → ℝ) (hBdd : BddAbove (cubeBesovOverlapSeminormTopValueSet Q s p u)) : BddAbove (cubeBesovOverlapNormTopValueSet Q s p u)

theorem HCPolySupport.CubeBesovDisjointRegularity.normValueSet_bddAbove {d : ℕ} {Q : TriadicCube d} {s : ℝ} {p q : ENNReal} {u : Vec d → ℝ} (hu : CubeBesovDisjointRegularity Q s p q u) : BddAbove (cubeBesovDisjointNormValueSet Q s p q u)

theorem HCPolySupport.CubeBesovDisjointRegularityTop.normValueSet_bddAbove {d : ℕ} {Q : TriadicCube d} {s : ℝ} {p : ENNReal} {u : Vec d → ℝ} (hu : CubeBesovDisjointRegularityTop Q s p u) : BddAbove (cubeBesovDisjointNormTopValueSet Q s p u)

theorem HCPolySupport.CubeBesovOverlapRegularity.normValueSet_bddAbove {d : ℕ} {Q : TriadicCube d} {s : ℝ} {p q : ENNReal} {u : Vec d → ℝ} (hu : CubeBesovOverlapRegularity Q s p q u) : BddAbove (cubeBesovOverlapNormValueSet Q s p q u)

theorem HCPolySupport.CubeBesovOverlapRegularityTop.normValueSet_bddAbove {d : ℕ} {Q : TriadicCube d} {s : ℝ} {p : ENNReal} {u : Vec d → ℝ} (hu : CubeBesovOverlapRegularityTop Q s p u) : BddAbove (cubeBesovOverlapNormTopValueSet Q s p u)

theorem HCPolySupport.cubeBesovDisjointPartialSeminorm_le_cubeBesovDisjointSeminorm_of_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (u : Vec d → ℝ) (hBdd : BddAbove (cubeBesovDisjointSeminormValueSet Q s p q u)) (N : ℕ) : cubeBesovDisjointPartialSeminorm Q s p q N u ≤ cubeBesovDisjointSeminorm Q s p q u

theorem HCPolySupport.cubeBesovDisjointPartialSeminormTop_le_cubeBesovDisjointSeminormTop_of_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (u : Vec d → ℝ) (hBdd : BddAbove (cubeBesovDisjointSeminormTopValueSet Q s p u)) (N : ℕ) : cubeBesovDisjointPartialSeminormTop Q s p N u ≤ cubeBesovDisjointSeminormTop Q s p u

theorem HCPolySupport.cubeBesovDisjointPartialNorm_le_cubeBesovDisjointNorm_of_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (u : Vec d → ℝ) (hBdd : BddAbove (cubeBesovDisjointNormValueSet Q s p q u)) (N : ℕ) : cubeBesovDisjointPartialNorm Q s p q N u ≤ cubeBesovDisjointNorm Q s p q u

theorem HCPolySupport.cubeBesovDisjointPartialNormTop_le_cubeBesovDisjointNormTop_of_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (u : Vec d → ℝ) (hBdd : BddAbove (cubeBesovDisjointNormTopValueSet Q s p u)) (N : ℕ) : cubeBesovDisjointPartialNormTop Q s p N u ≤ cubeBesovDisjointNormTop Q s p u

theorem HCPolySupport.cubeBesovOverlapPartialSeminorm_le_cubeBesovOverlapSeminorm_of_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (u : Vec d → ℝ) (hBdd : BddAbove (cubeBesovOverlapSeminormValueSet Q s p q u)) (N : ℕ) : cubeBesovOverlapPartialSeminorm Q s p q N u ≤ cubeBesovOverlapSeminorm Q s p q u

theorem HCPolySupport.cubeBesovOverlapPartialSeminormTop_le_cubeBesovOverlapSeminormTop_of_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (u : Vec d → ℝ) (hBdd : BddAbove (cubeBesovOverlapSeminormTopValueSet Q s p u)) (N : ℕ) : cubeBesovOverlapPartialSeminormTop Q s p N u ≤ cubeBesovOverlapSeminormTop Q s p u

theorem HCPolySupport.cubeBesovOverlapPartialNorm_le_cubeBesovOverlapNorm_of_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (u : Vec d → ℝ) (hBdd : BddAbove (cubeBesovOverlapSeminormValueSet Q s p q u)) (N : ℕ) : cubeBesovOverlapPartialNorm Q s p q N u ≤ cubeBesovOverlapNorm Q s p q u

theorem HCPolySupport.cubeBesovOverlapPartialNormTop_le_cubeBesovOverlapNormTop_of_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (u : Vec d → ℝ) (hBdd : BddAbove (cubeBesovOverlapSeminormTopValueSet Q s p u)) (N : ℕ) : cubeBesovOverlapPartialNormTop Q s p N u ≤ cubeBesovOverlapNormTop Q s p u

theorem HCPolySupport.cubeBesovDisjointSeminorm_nonneg_of_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (u : Vec d → ℝ) (hBdd : BddAbove (cubeBesovDisjointSeminormValueSet Q s p q u)) : 0 ≤ cubeBesovDisjointSeminorm Q s p q u

theorem HCPolySupport.cubeBesovDisjointSeminormTop_nonneg_of_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (u : Vec d → ℝ) (hBdd : BddAbove (cubeBesovDisjointSeminormTopValueSet Q s p u)) : 0 ≤ cubeBesovDisjointSeminormTop Q s p u

theorem HCPolySupport.cubeBesovDisjointNorm_nonneg_of_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (u : Vec d → ℝ) (hBdd : BddAbove (cubeBesovDisjointNormValueSet Q s p q u)) : 0 ≤ cubeBesovDisjointNorm Q s p q u

theorem HCPolySupport.cubeBesovDisjointNormTop_nonneg_of_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (u : Vec d → ℝ) (hBdd : BddAbove (cubeBesovDisjointNormTopValueSet Q s p u)) : 0 ≤ cubeBesovDisjointNormTop Q s p u

theorem HCPolySupport.cubeBesovOverlapSeminorm_nonneg_of_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (u : Vec d → ℝ) (hBdd : BddAbove (cubeBesovOverlapSeminormValueSet Q s p q u)) : 0 ≤ cubeBesovOverlapSeminorm Q s p q u

theorem HCPolySupport.cubeBesovOverlapSeminormTop_nonneg_of_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (u : Vec d → ℝ) (hBdd : BddAbove (cubeBesovOverlapSeminormTopValueSet Q s p u)) : 0 ≤ cubeBesovOverlapSeminormTop Q s p u

theorem HCPolySupport.cubeBesovOverlapNorm_nonneg_of_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (u : Vec d → ℝ) (hBdd : BddAbove (cubeBesovOverlapSeminormValueSet Q s p q u)) : 0 ≤ cubeBesovOverlapNorm Q s p q u

theorem HCPolySupport.cubeBesovOverlapNormTop_nonneg_of_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (u : Vec d → ℝ) (hBdd : BddAbove (cubeBesovOverlapSeminormTopValueSet Q s p u)) : 0 ≤ cubeBesovOverlapNormTop Q s p u

theorem HCPolySupport.CubeBesovDisjointRegularity.partialSeminorm_le_seminorm {d : ℕ} {Q : TriadicCube d} {s : ℝ} {p q : ENNReal} {u : Vec d → ℝ} (hu : CubeBesovDisjointRegularity Q s p q u) (N : ℕ) : cubeBesovDisjointPartialSeminorm Q s p q N u ≤ cubeBesovDisjointSeminorm Q s p q u

theorem HCPolySupport.CubeBesovDisjointRegularityTop.partialSeminorm_le_seminorm {d : ℕ} {Q : TriadicCube d} {s : ℝ} {p : ENNReal} {u : Vec d → ℝ} (hu : CubeBesovDisjointRegularityTop Q s p u) (N : ℕ) : cubeBesovDisjointPartialSeminormTop Q s p N u ≤ cubeBesovDisjointSeminormTop Q s p u

theorem HCPolySupport.CubeBesovOverlapRegularity.partialSeminorm_le_seminorm {d : ℕ} {Q : TriadicCube d} {s : ℝ} {p q : ENNReal} {u : Vec d → ℝ} (hu : CubeBesovOverlapRegularity Q s p q u) (N : ℕ) : cubeBesovOverlapPartialSeminorm Q s p q N u ≤ cubeBesovOverlapSeminorm Q s p q u

theorem HCPolySupport.CubeBesovOverlapRegularityTop.partialSeminorm_le_seminorm {d : ℕ} {Q : TriadicCube d} {s : ℝ} {p : ENNReal} {u : Vec d → ℝ} (hu : CubeBesovOverlapRegularityTop Q s p u) (N : ℕ) : cubeBesovOverlapPartialSeminormTop Q s p N u ≤ cubeBesovOverlapSeminormTop Q s p u

theorem HCPolySupport.CubeBesovDisjointRegularity.partialNorm_le_norm {d : ℕ} {Q : TriadicCube d} {s : ℝ} {p q : ENNReal} {u : Vec d → ℝ} (hu : CubeBesovDisjointRegularity Q s p q u) (N : ℕ) : cubeBesovDisjointPartialNorm Q s p q N u ≤ cubeBesovDisjointNorm Q s p q u

theorem HCPolySupport.CubeBesovDisjointRegularityTop.partialNorm_le_norm {d : ℕ} {Q : TriadicCube d} {s : ℝ} {p : ENNReal} {u : Vec d → ℝ} (hu : CubeBesovDisjointRegularityTop Q s p u) (N : ℕ) : cubeBesovDisjointPartialNormTop Q s p N u ≤ cubeBesovDisjointNormTop Q s p u

theorem HCPolySupport.CubeBesovOverlapRegularity.partialNorm_le_norm {d : ℕ} {Q : TriadicCube d} {s : ℝ} {p q : ENNReal} {u : Vec d → ℝ} (hu : CubeBesovOverlapRegularity Q s p q u) (N : ℕ) : cubeBesovOverlapPartialNorm Q s p q N u ≤ cubeBesovOverlapNorm Q s p q u

theorem HCPolySupport.CubeBesovOverlapRegularityTop.partialNorm_le_norm {d : ℕ} {Q : TriadicCube d} {s : ℝ} {p : ENNReal} {u : Vec d → ℝ} (hu : CubeBesovOverlapRegularityTop Q s p u) (N : ℕ) : cubeBesovOverlapPartialNormTop Q s p N u ≤ cubeBesovOverlapNormTop Q s p u

theorem HCPolySupport.CubeBesovDisjointRegularity.seminorm_nonneg {d : ℕ} {Q : TriadicCube d} {s : ℝ} {p q : ENNReal} {u : Vec d → ℝ} (hu : CubeBesovDisjointRegularity Q s p q u) : 0 ≤ cubeBesovDisjointSeminorm Q s p q u

theorem HCPolySupport.CubeBesovDisjointRegularityTop.seminorm_nonneg {d : ℕ} {Q : TriadicCube d} {s : ℝ} {p : ENNReal} {u : Vec d → ℝ} (hu : CubeBesovDisjointRegularityTop Q s p u) : 0 ≤ cubeBesovDisjointSeminormTop Q s p u

theorem HCPolySupport.CubeBesovOverlapRegularity.seminorm_nonneg {d : ℕ} {Q : TriadicCube d} {s : ℝ} {p q : ENNReal} {u : Vec d → ℝ} (hu : CubeBesovOverlapRegularity Q s p q u) : 0 ≤ cubeBesovOverlapSeminorm Q s p q u

theorem HCPolySupport.CubeBesovOverlapRegularityTop.seminorm_nonneg {d : ℕ} {Q : TriadicCube d} {s : ℝ} {p : ENNReal} {u : Vec d → ℝ} (hu : CubeBesovOverlapRegularityTop Q s p u) : 0 ≤ cubeBesovOverlapSeminormTop Q s p u

theorem HCPolySupport.CubeBesovDisjointRegularity.norm_nonneg {d : ℕ} {Q : TriadicCube d} {s : ℝ} {p q : ENNReal} {u : Vec d → ℝ} (hu : CubeBesovDisjointRegularity Q s p q u) : 0 ≤ cubeBesovDisjointNorm Q s p q u

theorem HCPolySupport.CubeBesovDisjointRegularityTop.norm_nonneg {d : ℕ} {Q : TriadicCube d} {s : ℝ} {p : ENNReal} {u : Vec d → ℝ} (hu : CubeBesovDisjointRegularityTop Q s p u) : 0 ≤ cubeBesovDisjointNormTop Q s p u

theorem HCPolySupport.CubeBesovOverlapRegularity.norm_nonneg {d : ℕ} {Q : TriadicCube d} {s : ℝ} {p q : ENNReal} {u : Vec d → ℝ} (hu : CubeBesovOverlapRegularity Q s p q u) : 0 ≤ cubeBesovOverlapNorm Q s p q u

theorem HCPolySupport.CubeBesovOverlapRegularityTop.norm_nonneg {d : ℕ} {Q : TriadicCube d} {s : ℝ} {p : ENNReal} {u : Vec d → ℝ} (hu : CubeBesovOverlapRegularityTop Q s p u) : 0 ≤ cubeBesovOverlapNormTop Q s p u

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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