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

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

Finite disjoint duality scaffolding for cube Besov norms.

This checkpoint freezes the normalized cube pairing together with the test-function conventions that define the two dual negative-order Besov seminorms used later:

• the full dual seminorm, tested against positive Besov norms;
• the mean-zero-tested dual seminorm, matching the hat-seminorm in the notes.

At this stage we package the disjoint finite-depth definitions and the cheap zero-function API. Overlap finite dual tests live in HCPolySupport.Besov.Duality.OverlapDefinitions.

noncomputable def HCPolySupport.cubeBesovPairing {d : ℕ} (Q : TriadicCube d) (f g : Vec d → ℝ) : ℝ

The normalized cube average of the product of two scalar functions.

Equations

• HCPolySupport.cubeBesovPairing Q f g = HCPolySupport.cubeAverage Q fun (x : HCPolySupport.Vec d) => f x * g x

noncomputable def HCPolySupport.cubeBesovConjExponent (p : ENNReal) : ENNReal

The Hölder conjugate of an extended nonnegative exponent.

Equations

• HCPolySupport.cubeBesovConjExponent p = p.conjExponent

theorem HCPolySupport.cubeBesovConjExponent_ne_zero (p : ENNReal) : cubeBesovConjExponent p ≠ 0

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

The finite positive Besov norm at conjugate exponents, using the maximum branch when q' = ∞.

Equations

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

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

The finite positive Besov seminorm at conjugate exponents, using the maximum branch when q' = ∞.

Equations

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

@[simp]

theorem HCPolySupport.cubeBesovDualTestNorm_of_conjExponent_eq_top {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (g : Vec d → ℝ) (hq : cubeBesovConjExponent q = ⊤) : cubeBesovDualTestNorm Q s p q N g = cubeBesovPartialNormTop Q s (cubeBesovConjExponent p) N g

@[simp]

theorem HCPolySupport.cubeBesovDualTestNorm_of_conjExponent_ne_top {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (g : Vec d → ℝ) (hq : cubeBesovConjExponent q ≠ ⊤) : cubeBesovDualTestNorm Q s p q N g = cubeBesovPartialNorm Q s (cubeBesovConjExponent p) (cubeBesovConjExponent q) N g

@[simp]

theorem HCPolySupport.cubeBesovDualTestSeminorm_of_conjExponent_eq_top {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (g : Vec d → ℝ) (hq : cubeBesovConjExponent q = ⊤) : cubeBesovDualTestSeminorm Q s p q N g = cubeBesovPartialSeminormTop Q s (cubeBesovConjExponent p) N g

@[simp]

theorem HCPolySupport.cubeBesovDualTestSeminorm_of_conjExponent_ne_top {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (g : Vec d → ℝ) (hq : cubeBesovConjExponent q ≠ ⊤) : cubeBesovDualTestSeminorm Q s p q N g = cubeBesovPartialSeminorm Q s (cubeBesovConjExponent p) (cubeBesovConjExponent q) N g

theorem HCPolySupport.cubeBesovDualTestNorm_eq_cubeBesovDualTestSeminorm_of_cubeAverage_eq_zero {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (g : Vec d → ℝ) (havg : cubeAverage Q g = 0) : cubeBesovDualTestNorm Q s p q N g = cubeBesovDualTestSeminorm Q s p q N g

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

Membership of every descendant fluctuation through depth N in normalized Lᵖ'.

Equations

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

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

A test function with conjugate Besov norm at most one and local Lᵖ' fluctuations.

Equations

• HCPolySupport.CubeBesovDualTest Q s p q N g = (HCPolySupport.cubeBesovDualTestNorm Q s p q N g ≤ 1 ∧ HCPolySupport.CubeBesovDualLocalMemLp Q p N g)

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

A mean-zero test function with conjugate Besov seminorm at most one and local Lᵖ' fluctuations.

Equations

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

theorem HCPolySupport.CubeBesovDualTest.norm_le_one {d : ℕ} {Q : TriadicCube d} {s : ℝ} {p q : ENNReal} {N : ℕ} {g : Vec d → ℝ} (hg : CubeBesovDualTest Q s p q N g) : cubeBesovDualTestNorm Q s p q N g ≤ 1

theorem HCPolySupport.CubeBesovDualTest.local_memLp {d : ℕ} {Q : TriadicCube d} {p : ENNReal} {N : ℕ} {g : Vec d → ℝ} (hg : CubeBesovDualLocalMemLp Q p N g) (j : ℕ) : j < N + 1 → ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.MemLp (cubeFluctuation R g) (cubeBesovConjExponent p) (normalizedCubeMeasure R)

theorem HCPolySupport.CubeBesovDualTest.memLp_admissible {d : ℕ} {Q : TriadicCube d} {s : ℝ} {p q : ENNReal} {N : ℕ} {g : Vec d → ℝ} (hg : CubeBesovDualTest Q s p q N g) (j : ℕ) : j < N + 1 → ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.MemLp (cubeFluctuation R g) (cubeBesovConjExponent p) (normalizedCubeMeasure R)

theorem HCPolySupport.CubeBesovDualMeanZeroTest.seminorm_le_one {d : ℕ} {Q : TriadicCube d} {s : ℝ} {p q : ENNReal} {N : ℕ} {g : Vec d → ℝ} (hg : CubeBesovDualMeanZeroTest Q s p q N g) : cubeBesovDualTestSeminorm Q s p q N g ≤ 1

theorem HCPolySupport.CubeBesovDualMeanZeroTest.cubeAverage_eq_zero {d : ℕ} {Q : TriadicCube d} {s : ℝ} {p q : ENNReal} {N : ℕ} {g : Vec d → ℝ} (hg : CubeBesovDualMeanZeroTest Q s p q N g) : cubeAverage Q g = 0

theorem HCPolySupport.CubeBesovDualMeanZeroTest.memLp_admissible {d : ℕ} {Q : TriadicCube d} {s : ℝ} {p q : ENNReal} {N : ℕ} {g : Vec d → ℝ} (hg : CubeBesovDualMeanZeroTest Q s p q N g) (j : ℕ) : j < N + 1 → ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.MemLp (cubeFluctuation R g) (cubeBesovConjExponent p) (normalizedCubeMeasure R)

theorem HCPolySupport.cubeBesovDualLocalMemLp_const {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (N : ℕ) (c : ℝ) : CubeBesovDualLocalMemLp Q p N fun (x : Vec d) => c

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

Absolute normalized pairings with all admissible finite-depth Besov norm tests.

Equations

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

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

Absolute normalized pairings with all admissible finite-depth mean-zero Besov tests.

Equations

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

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

The real supremum of absolute pairings against admissible finite-depth Besov norm tests.

Equations

• HCPolySupport.cubeBesovDualPartialNorm Q s p q N f = sSup (HCPolySupport.cubeBesovDualPartialNormValueSet Q s p q N f)

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

The real supremum of absolute pairings against admissible finite-depth mean-zero Besov tests.

Equations

• HCPolySupport.cubeBesovDualPartialSeminorm Q s p q N f = sSup (HCPolySupport.cubeBesovDualPartialSeminormValueSet Q s p q N f)

theorem HCPolySupport.cubeBesovScaleWeight_mul_norm_cubeAverage_le_cubeBesovDualTestNorm {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (g : Vec d → ℝ) : cubeBesovScaleWeight s Q * ‖cubeAverage Q g‖ ≤ cubeBesovDualTestNorm Q s p q N g

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

theorem HCPolySupport.CubeBesovDualTest.scaleWeight_mul_norm_cubeAverage_le_one {d : ℕ} {Q : TriadicCube d} {s : ℝ} {p q : ENNReal} {N : ℕ} {g : Vec d → ℝ} (hg : CubeBesovDualTest Q s p q N g) : cubeBesovScaleWeight s Q * ‖cubeAverage Q g‖ ≤ 1

theorem HCPolySupport.cubeBesovScaleWeight_neg_mul_cubeBesovScaleWeight {d : ℕ} (Q : TriadicCube d) (s : ℝ) : cubeBesovScaleWeight (-s) Q * cubeBesovScaleWeight s Q = 1

theorem HCPolySupport.cubeBesovDualPartialSeminormValueSet_subset_cubeBesovDualPartialNormValueSet {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (f : Vec d → ℝ) : cubeBesovDualPartialSeminormValueSet Q s p q N f ⊆ cubeBesovDualPartialNormValueSet Q s p q N f

theorem HCPolySupport.cubeBesovDualPartialSeminorm_le_cubeBesovDualPartialNorm_of_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (f : Vec d → ℝ) (hp0 : cubeBesovConjExponent p ≠ 0) (hpTop : cubeBesovConjExponent p ≠ ⊤) (hBdd : BddAbove (cubeBesovDualPartialNormValueSet Q s p q N f)) : cubeBesovDualPartialSeminorm Q s p q N f ≤ cubeBesovDualPartialNorm Q s p q N f

theorem HCPolySupport.abs_cubeBesovPairing_le_cubeBesovDualPartialNorm_of_dual_test {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (f g : Vec d → ℝ) (hBdd : BddAbove (cubeBesovDualPartialNormValueSet Q s p q N f)) (hg : CubeBesovDualTest Q s p q N g) : |cubeBesovPairing Q f g| ≤ cubeBesovDualPartialNorm Q s p q N f

theorem HCPolySupport.abs_cubeBesovPairing_le_cubeBesovDualPartialSeminorm_of_dual_mean_zero_test {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (f g : Vec d → ℝ) (hBdd : BddAbove (cubeBesovDualPartialSeminormValueSet Q s p q N f)) (hg : CubeBesovDualMeanZeroTest Q s p q N g) : |cubeBesovPairing Q f g| ≤ cubeBesovDualPartialSeminorm Q s p q N f

theorem HCPolySupport.abs_cubeBesovPairing_le_mul_cubeLpNorm_of_holderConjugate {d : ℕ} (Q : TriadicCube d) (p q : ENNReal) (f g : Vec d → ℝ) [p.HolderConjugate q] (hf : MeasureTheory.MemLp f p (normalizedCubeMeasure Q)) (hg : MeasureTheory.MemLp g q (normalizedCubeMeasure Q)) : |cubeBesovPairing Q f g| ≤ cubeLpNorm Q p f * cubeLpNorm Q q g

theorem HCPolySupport.abs_cubeBesovPairing_le_mul_cubeLpNorm_conjExponent {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (f g : Vec d → ℝ) (hf : MeasureTheory.MemLp f p (normalizedCubeMeasure Q)) (hg : MeasureTheory.MemLp g (cubeBesovConjExponent p) (normalizedCubeMeasure Q)) (hp : 1 ≤ p) : |cubeBesovPairing Q f g| ≤ cubeLpNorm Q p f * cubeLpNorm Q (cubeBesovConjExponent p) g