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

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

Finite overlap dual-test definitions for cube Besov duality.

This module is the overlap counterpart of Duality.Definitions: it keeps overlap-local measure and MemLp facts together with the finite-depth overlap dual test norms, leaving global sSup wrappers to Duality.OverlapFull.

theorem HCPolySupport.ScalarOverlap.normalizedCubeMeasure_eq_smul_restrict_of_mem_centersAtDepth {d : ℕ} {Q S : TriadicCube d} {j : ℕ} (hS : S ∈ centersAtDepth Q j) : normalizedCubeMeasure S = ENNReal.ofReal (HCPolySupport.cubeVolume Q / cubeVolume S) • (HCPolySupport.normalizedCubeMeasure Q).restrict (cubeSet S)

theorem HCPolySupport.ScalarOverlap.memLp_of_mem_centersAtDepth_of_memLp {d : ℕ} {Q S : TriadicCube d} {j : ℕ} {p : ENNReal} {f : Vec d → ℝ} (hS : S ∈ centersAtDepth Q j) (hf : MeasureTheory.MemLp f p (HCPolySupport.normalizedCubeMeasure Q)) : MeasureTheory.MemLp f p (normalizedCubeMeasure S)

theorem HCPolySupport.ScalarOverlap.memLp_sub_cubeAverage_of_mem_centersAtDepth_of_memLp {d : ℕ} {Q S : TriadicCube d} {j : ℕ} {p : ENNReal} {f : Vec d → ℝ} (hS : S ∈ centersAtDepth Q j) (hf : MeasureTheory.MemLp f p (HCPolySupport.normalizedCubeMeasure Q)) : MeasureTheory.MemLp (fun (x : Vec d) => f x - cubeAverage S f) p (normalizedCubeMeasure S)

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

The overlap Besov test norm through depth N at conjugate exponents, using a supremum when the conjugate of q is infinite.

Equations

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

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

The overlap Besov test seminorm through depth N at conjugate exponents, using a supremum when the conjugate of q is infinite.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Local Lᵖ integrability at the conjugate exponent of p for the mean-subtracted test on every overlap cube through depth N.

Equations

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

theorem HCPolySupport.CubeBesovOverlapDualLocalMemLp.of_memLp_parent {d : ℕ} {Q : TriadicCube d} {p : ENNReal} {N : ℕ} {g : Vec d → ℝ} (hg : MeasureTheory.MemLp g (cubeBesovConjExponent p) (normalizedCubeMeasure Q)) : CubeBesovOverlapDualLocalMemLp Q p N g

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

An overlap dual test with norm at most one and locally integrable fluctuations at the conjugate exponent of p.

Equations

• HCPolySupport.CubeBesovOverlapDualTest Q s p q N g = (HCPolySupport.cubeBesovOverlapDualTestNorm Q s p q N g ≤ 1 ∧ HCPolySupport.CubeBesovOverlapDualLocalMemLp Q p N g)

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

An overlap dual test of mean zero on Q, with seminorm at most one and locally integrable fluctuations at the conjugate exponent of p.

Equations

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

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

theorem HCPolySupport.CubeBesovOverlapDualTest.local_memLp {d : ℕ} {Q : TriadicCube d} {p : ENNReal} {N : ℕ} {g : Vec d → ℝ} (hg : CubeBesovOverlapDualLocalMemLp Q p N g) (j : ℕ) : j < N + 1 → ∀ S ∈ ScalarOverlap.centersAtDepth Q j, MeasureTheory.MemLp (fun (x : Vec d) => g x - ScalarOverlap.cubeAverage S g) (cubeBesovConjExponent p) (ScalarOverlap.normalizedCubeMeasure S)

theorem HCPolySupport.CubeBesovOverlapDualTest.memLp_admissible {d : ℕ} {Q : TriadicCube d} {s : ℝ} {p q : ENNReal} {N : ℕ} {g : Vec d → ℝ} (hg : CubeBesovOverlapDualTest Q s p q N g) (j : ℕ) : j < N + 1 → ∀ S ∈ ScalarOverlap.centersAtDepth Q j, MeasureTheory.MemLp (fun (x : Vec d) => g x - ScalarOverlap.cubeAverage S g) (cubeBesovConjExponent p) (ScalarOverlap.normalizedCubeMeasure S)

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

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

theorem HCPolySupport.CubeBesovOverlapDualMeanZeroTest.memLp_admissible {d : ℕ} {Q : TriadicCube d} {s : ℝ} {p q : ENNReal} {N : ℕ} {g : Vec d → ℝ} (hg : CubeBesovOverlapDualMeanZeroTest Q s p q N g) (j : ℕ) : j < N + 1 → ∀ S ∈ ScalarOverlap.centersAtDepth Q j, MeasureTheory.MemLp (fun (x : Vec d) => g x - ScalarOverlap.cubeAverage S g) (cubeBesovConjExponent p) (ScalarOverlap.normalizedCubeMeasure S)

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

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