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

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

Global wrapper layer for the cube Besov duality package.

This file keeps the new global objects deliberately minimal:

• a depth-uniform local MemLp predicate for dual tests;
• global dual test predicates, using the finite-depth comparison norms as the test data;
• global value sets and sSup wrappers for the dual pairing bounds;
• a global circ wrapper built from the finite circ branch.

The comparison theorems themselves are still deferred to the later projection-limit layer.

noncomputable def HCPolySupport.CubeBesovDualLocalMemLpGlobal {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (g : Vec d → ℝ) : Prop

Membership of fluctuations on every descendant cube in normalized Lᵖ', at every depth.

Equations

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

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

The real supremum over depths of the conjugate positive Besov test norms.

Equations

• HCPolySupport.cubeBesovDualFullTestNorm Q s p q g = sSup (Set.range fun (N : ℕ) => HCPolySupport.cubeBesovDualTestNorm Q s p q N g)

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

The real supremum over depths of the conjugate positive Besov test seminorms.

Equations

• HCPolySupport.cubeBesovDualMeanZeroTestSeminorm Q s p q g = sSup (Set.range fun (N : ℕ) => HCPolySupport.cubeBesovDualTestSeminorm Q s p q N g)

def HCPolySupport.CubeBesovDualFullTest {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (g : Vec d → ℝ) : Prop

A test function whose conjugate Besov norms are at most one at every depth, with locally Lᵖ' fluctuations on all descendant cubes.

Equations

• HCPolySupport.CubeBesovDualFullTest Q s p q g = ((∀ (N : ℕ), HCPolySupport.cubeBesovDualTestNorm Q s p q N g ≤ 1) ∧ HCPolySupport.CubeBesovDualLocalMemLpGlobal Q p g)

def HCPolySupport.CubeBesovDualMeanZeroTestGlobal {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (g : Vec d → ℝ) : Prop

A mean-zero test function whose conjugate Besov seminorms are at most one at every depth, with locally Lᵖ' fluctuations on all descendant cubes.

Equations

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

theorem HCPolySupport.CubeBesovDualFullTest.to_dual_test {d : ℕ} {Q : TriadicCube d} {s : ℝ} {p q : ENNReal} {g : Vec d → ℝ} (hg : CubeBesovDualFullTest Q s p q g) (N : ℕ) : CubeBesovDualTest Q s p q N g

theorem HCPolySupport.CubeBesovDualMeanZeroTestGlobal.to_dual_test {d : ℕ} {Q : TriadicCube d} {s : ℝ} {p q : ENNReal} {g : Vec d → ℝ} (hg : CubeBesovDualMeanZeroTestGlobal Q s p q g) (N : ℕ) : CubeBesovDualTest Q s p q N g

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

Absolute normalized pairings with tests satisfying the Besov norm bound at every depth.

Equations

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

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

Absolute normalized pairings with mean-zero tests satisfying the Besov seminorm bound at every depth.

Equations

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

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

The real supremum of absolute pairings against global Besov norm tests.

Equations

• HCPolySupport.cubeBesovDualFullNorm Q s p q f = sSup (HCPolySupport.cubeBesovDualFullNormValueSet Q s p q f)

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

The real supremum of absolute pairings against global mean-zero Besov tests.

Equations

• HCPolySupport.cubeBesovDualMeanZeroSeminorm Q s p q f = sSup (HCPolySupport.cubeBesovDualMeanZeroSeminormValueSet Q s p q f)

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

The circ norm truncated at depth N + 1, using the maximum branch when q = ∞.

Equations

• HCPolySupport.cubeBesovCircNormEntry Q s p q N u = if q = ⊤ then HCPolySupport.cubeBesovCircPartialNormTop Q s p (N + 1) u else HCPolySupport.cubeBesovCircPartialNorm Q s p q (N + 1) u

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

The set of circ norm truncations at all positive depths.

Equations

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

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

The real supremum of the circ norm truncations at all positive depths.

Equations

• HCPolySupport.cubeBesovCircNorm Q s p q u = sSup (HCPolySupport.cubeBesovCircNormValueSet Q s p q u)

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

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

theorem HCPolySupport.cubeBesovDualFullNormValueSet_nonempty {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (f : Vec d → ℝ) (hp0 : cubeBesovConjExponent p ≠ 0) (hpTop : cubeBesovConjExponent p ≠ ⊤) : (cubeBesovDualFullNormValueSet Q s p q f).Nonempty

theorem HCPolySupport.zero_mem_cubeBesovDualFullNormValueSet {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (f : Vec d → ℝ) (hp0 : cubeBesovConjExponent p ≠ 0) (hpTop : cubeBesovConjExponent p ≠ ⊤) : 0 ∈ cubeBesovDualFullNormValueSet Q s p q f

theorem HCPolySupport.cubeBesovDualMeanZeroSeminormValueSet_nonempty {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (f : Vec d → ℝ) (hp0 : cubeBesovConjExponent p ≠ 0) (hpTop : cubeBesovConjExponent p ≠ ⊤) : (cubeBesovDualMeanZeroSeminormValueSet Q s p q f).Nonempty

theorem HCPolySupport.zero_mem_cubeBesovDualMeanZeroSeminormValueSet {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (f : Vec d → ℝ) (hp0 : cubeBesovConjExponent p ≠ 0) (hpTop : cubeBesovConjExponent p ≠ ⊤) : 0 ∈ cubeBesovDualMeanZeroSeminormValueSet Q s p q f

theorem HCPolySupport.cubeBesovDualMeanZeroSeminorm_nonneg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (f : Vec d → ℝ) (hp0 : cubeBesovConjExponent p ≠ 0) (hpTop : cubeBesovConjExponent p ≠ ⊤) : 0 ≤ cubeBesovDualMeanZeroSeminorm Q s p q f

theorem HCPolySupport.cubeBesovDualFullNorm_nonneg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (f : Vec d → ℝ) (hp0 : cubeBesovConjExponent p ≠ 0) (hpTop : cubeBesovConjExponent p ≠ ⊤) : 0 ≤ cubeBesovDualFullNorm Q s p q f

theorem HCPolySupport.cubeBesovDualFullNorm_le_of_forall_fullTest_pairing_le {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (f : Vec d → ℝ) {B : ℝ} (hp0 : cubeBesovConjExponent p ≠ 0) (hpTop : cubeBesovConjExponent p ≠ ⊤) (hB : ∀ (g : Vec d → ℝ), CubeBesovDualFullTest Q s p q g → |cubeBesovPairing Q f g| ≤ B) : cubeBesovDualFullNorm Q s p q f ≤ B

Bound a full dual negative Besov norm by bounding its pairing against all unit full-dual tests. This is the formal supremum step used in duality arguments.

@[simp]

theorem HCPolySupport.cubeBesovDualMeanZeroSeminormValueSet_const {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (c : ℝ) (hp0 : cubeBesovConjExponent p ≠ 0) (hpTop : cubeBesovConjExponent p ≠ ⊤) : (cubeBesovDualMeanZeroSeminormValueSet Q s p q fun (x : Vec d) => c) = {0}

@[simp]

theorem HCPolySupport.cubeBesovDualMeanZeroSeminorm_const {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (c : ℝ) (hp0 : cubeBesovConjExponent p ≠ 0) (hpTop : cubeBesovConjExponent p ≠ ⊤) : (cubeBesovDualMeanZeroSeminorm Q s p q fun (x : Vec d) => c) = 0

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

theorem HCPolySupport.abs_cubeBesovPairing_le_cubeBesovDualFullNorm_of_full_test {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (f g : Vec d → ℝ) (hBdd : BddAbove (cubeBesovDualFullNormValueSet Q s p q f)) (hg : CubeBesovDualFullTest Q s p q g) : |cubeBesovPairing Q f g| ≤ cubeBesovDualFullNorm Q s p q f

theorem HCPolySupport.abs_cubeBesovPairing_le_cubeBesovDualMeanZeroSeminorm_of_mean_zero_test {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (f g : Vec d → ℝ) (hBdd : BddAbove (cubeBesovDualMeanZeroSeminormValueSet Q s p q f)) (hg : CubeBesovDualMeanZeroTestGlobal Q s p q g) : |cubeBesovPairing Q f g| ≤ cubeBesovDualMeanZeroSeminorm Q s p q f

theorem HCPolySupport.cubeBesovCircNormEntry_le_cubeBesovCircNorm {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (u : Vec d → ℝ) (hBdd : BddAbove (cubeBesovCircNormValueSet Q s p q u)) (N : ℕ) : cubeBesovCircNormEntry Q s p q N u ≤ cubeBesovCircNorm Q s p q u

theorem HCPolySupport.cubeBesovCircPartialNorm_le_cubeBesovCircNorm {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (u : Vec d → ℝ) (hq : q ≠ ⊤) (hBdd : BddAbove (cubeBesovCircNormValueSet Q s p q u)) (N : ℕ) : cubeBesovCircPartialNorm Q s p q (N + 1) u ≤ cubeBesovCircNorm Q s p q u

theorem HCPolySupport.cubeBesovCircPartialNormTop_le_cubeBesovCircNorm {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (u : Vec d → ℝ) (hq : q = ⊤) (hBdd : BddAbove (cubeBesovCircNormValueSet Q s p q u)) (N : ℕ) : cubeBesovCircPartialNormTop Q s p (N + 1) u ≤ cubeBesovCircNorm Q s p q u

theorem HCPolySupport.cubeBesovCircNorm_le_of_forall_entry_le {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (u : Vec d → ℝ) {B : ℝ} (hB : ∀ (N : ℕ), cubeBesovCircNormEntry Q s p q N u ≤ B) : cubeBesovCircNorm Q s p q u ≤ B

Bound the full circ norm by a uniform bound on all entries in its defining value set.

theorem HCPolySupport.cubeBesovCircNorm_le_of_forall_partialNorm_le {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (u : Vec d → ℝ) {B : ℝ} (hq : q ≠ ⊤) (hB : ∀ (N : ℕ), cubeBesovCircPartialNorm Q s p q N u ≤ B) : cubeBesovCircNorm Q s p q u ≤ B

For finite q, the full circ norm is bounded by any uniform bound on all finite partial circ norms.