Coarse-graining support: Support.Besov.PositiveOverlapBridge

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

Disjoint-to-overlap positive Besov bridge

The basic geometric input is that every ordinary depth-j descendant cube is the scalar-overlap cube of its middle child. This gives the one useful bridge direction: the disjoint depth average is controlled by the overlapping depth average, with only the cardinality loss from the extra generation of centers.

theorem HCPolySupport.ScalarOverlap.centersAtDepth_card_le_three_pow_mul_descendantsAtDepth_card {d : ℕ} (Q : TriadicCube d) (j : ℕ) : (centersAtDepth Q j).card ≤ 3 ^ d * (descendantsAtDepth Q j).card

theorem HCPolySupport.cubeBesovDepthAverage_le_three_pow_mul_overlapDepthAverage {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (u : Vec d → ℝ) (j : ℕ) : cubeBesovDepthAverage Q p u j ≤ 3 ^ d * cubeBesovOverlapDepthAverage Q p u j

theorem HCPolySupport.cubeBesovDepthSeminorm_le_three_rpow_mul_overlapDepthSeminorm {d : ℕ} (Q : TriadicCube d) (s : ℝ) {p : ENNReal} (hp : 0 < p.toReal) (u : Vec d → ℝ) (j : ℕ) : cubeBesovDepthSeminorm Q s p u j ≤ 3 ^ (↑d / p.toReal) * cubeBesovOverlapDepthSeminorm Q s p u j

theorem HCPolySupport.cubeBesovPartialSeminorm_le_three_rpow_mul_overlapPartialSeminorm {d : ℕ} (Q : TriadicCube d) (s : ℝ) {p q : ENNReal} (hp : 0 < p.toReal) (hq : 1 ≤ q.toReal) (N : ℕ) (u : Vec d → ℝ) : cubeBesovPartialSeminorm Q s p q N u ≤ 3 ^ (↑d / p.toReal) * cubeBesovOverlapPartialSeminorm Q s p q N u

theorem HCPolySupport.cubeBesovPartialSeminormTop_le_three_rpow_mul_overlapPartialSeminormTop {d : ℕ} (Q : TriadicCube d) (s : ℝ) {p : ENNReal} (hp : 0 < p.toReal) (N : ℕ) (u : Vec d → ℝ) : cubeBesovPartialSeminormTop Q s p N u ≤ 3 ^ (↑d / p.toReal) * cubeBesovOverlapPartialSeminormTop Q s p N u

theorem HCPolySupport.cubeBesovPartialNorm_le_three_rpow_mul_overlapPartialNorm {d : ℕ} (Q : TriadicCube d) (s : ℝ) {p q : ENNReal} (hp : 0 < p.toReal) (hq : 1 ≤ q.toReal) (N : ℕ) (u : Vec d → ℝ) : cubeBesovPartialNorm Q s p q N u ≤ 3 ^ (↑d / p.toReal) * cubeBesovOverlapPartialNorm Q s p q N u

theorem HCPolySupport.cubeBesovPartialNormTop_le_three_rpow_mul_overlapPartialNormTop {d : ℕ} (Q : TriadicCube d) (s : ℝ) {p : ENNReal} (hp : 0 < p.toReal) (N : ℕ) (u : Vec d → ℝ) : cubeBesovPartialNormTop Q s p N u ≤ 3 ^ (↑d / p.toReal) * cubeBesovOverlapPartialNormTop Q s p N u

theorem HCPolySupport.cubeBesovDisjointSeminorm_le_three_rpow_mul_overlapSeminorm_of_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) {p q : ENNReal} (hp : 0 < p.toReal) (hq : 1 ≤ q.toReal) (u : Vec d → ℝ) (hBddOverlap : BddAbove (cubeBesovOverlapSeminormValueSet Q s p q u)) : cubeBesovDisjointSeminorm Q s p q u ≤ 3 ^ (↑d / p.toReal) * cubeBesovOverlapSeminorm Q s p q u

theorem HCPolySupport.cubeBesovDisjointSeminormTop_le_three_rpow_mul_overlapSeminormTop_of_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) {p : ENNReal} (hp : 0 < p.toReal) (u : Vec d → ℝ) (hBddOverlap : BddAbove (cubeBesovOverlapSeminormTopValueSet Q s p u)) : cubeBesovDisjointSeminormTop Q s p u ≤ 3 ^ (↑d / p.toReal) * cubeBesovOverlapSeminormTop Q s p u

theorem HCPolySupport.cubeBesovDisjointNorm_le_three_rpow_mul_overlapNorm_of_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) {p q : ENNReal} (hp : 0 < p.toReal) (hq : 1 ≤ q.toReal) (u : Vec d → ℝ) (hBddOverlap : BddAbove (cubeBesovOverlapSeminormValueSet Q s p q u)) : cubeBesovDisjointNorm Q s p q u ≤ 3 ^ (↑d / p.toReal) * cubeBesovOverlapNorm Q s p q u

theorem HCPolySupport.cubeBesovDisjointNormTop_le_three_rpow_mul_overlapNormTop_of_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) {p : ENNReal} (hp : 0 < p.toReal) (u : Vec d → ℝ) (hBddOverlap : BddAbove (cubeBesovOverlapSeminormTopValueSet Q s p u)) : cubeBesovDisjointNormTop Q s p u ≤ 3 ^ (↑d / p.toReal) * cubeBesovOverlapNormTop Q s p u

theorem HCPolySupport.cubeBesovDisjointSeminorm_le_three_rpow_mul_overlapSeminorm_of_overlapRegularity {d : ℕ} (Q : TriadicCube d) (s : ℝ) {p q : ENNReal} (hp : 0 < p.toReal) (hq : 1 ≤ q.toReal) (u : Vec d → ℝ) (hu : CubeBesovOverlapRegularity Q s p q u) : cubeBesovDisjointSeminorm Q s p q u ≤ 3 ^ (↑d / p.toReal) * cubeBesovOverlapSeminorm Q s p q u

theorem HCPolySupport.cubeBesovDisjointSeminormTop_le_three_rpow_mul_overlapSeminormTop_of_overlapRegularity {d : ℕ} (Q : TriadicCube d) (s : ℝ) {p : ENNReal} (hp : 0 < p.toReal) (u : Vec d → ℝ) (hu : CubeBesovOverlapRegularityTop Q s p u) : cubeBesovDisjointSeminormTop Q s p u ≤ 3 ^ (↑d / p.toReal) * cubeBesovOverlapSeminormTop Q s p u

theorem HCPolySupport.cubeBesovDisjointNorm_le_three_rpow_mul_overlapNorm_of_overlapRegularity {d : ℕ} (Q : TriadicCube d) (s : ℝ) {p q : ENNReal} (hp : 0 < p.toReal) (hq : 1 ≤ q.toReal) (u : Vec d → ℝ) (hu : CubeBesovOverlapRegularity Q s p q u) : cubeBesovDisjointNorm Q s p q u ≤ 3 ^ (↑d / p.toReal) * cubeBesovOverlapNorm Q s p q u

theorem HCPolySupport.cubeBesovDisjointNormTop_le_three_rpow_mul_overlapNormTop_of_overlapRegularity {d : ℕ} (Q : TriadicCube d) (s : ℝ) {p : ENNReal} (hp : 0 < p.toReal) (u : Vec d → ℝ) (hu : CubeBesovOverlapRegularityTop Q s p u) : cubeBesovDisjointNormTop Q s p u ≤ 3 ^ (↑d / p.toReal) * cubeBesovOverlapNormTop Q s p u