Coarse-graining support: Support.Besov.Duality.ProjectedPairing.MainBounds #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.abs_cubeBesovPairing_projection_le_max_mul_cubeBesovPartialNorm_cubeBesovCircPartialNorm
{d : ℕ}
(Q : TriadicCube d)
(s : ℝ)
(p q : ENNReal)
(f g : Vec d → ℝ)
(N : ℕ)
(hgInt : MeasureTheory.IntegrableOn g (cubeSet Q) MeasureTheory.volume)
(hp : 1 ≤ p)
(hpTop : p ≠ ⊤)
(hpConjTop : cubeBesovConjExponent p ≠ ⊤)
(hq : 1 ≤ q)
(hqTop : q ≠ ⊤)
(hqConjTop : cubeBesovConjExponent q ≠ ⊤)
(hf : ∀ j < N + 1, ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.MemLp (cubeFluctuation R f) p (normalizedCubeMeasure R))
(hg :
∀ j < N + 1,
∀ R ∈ descendantsAtDepth Q j,
MeasureTheory.MemLp (cubeProjection Q (j + 1) g) (cubeBesovConjExponent p) (normalizedCubeMeasure R))
:
|cubeBesovPairing Q f (cubeProjection Q (N + 1) g)| ≤ max 1 (3 ^ s) * cubeBesovPartialNorm Q s p q N f * cubeBesovCircPartialNorm Q s (cubeBesovConjExponent p) (cubeBesovConjExponent q) (N + 1) g
theorem
HCPolySupport.abs_cubeBesovPairing_projection_le_max_partialTop_circOne
{d : ℕ}
(Q : TriadicCube d)
(s : ℝ)
(p : ENNReal)
(f g : Vec d → ℝ)
(N : ℕ)
(hgInt : MeasureTheory.IntegrableOn g (cubeSet Q) MeasureTheory.volume)
(hp : 1 ≤ p)
(hpTop : p ≠ ⊤)
(hpConjTop : cubeBesovConjExponent p ≠ ⊤)
(hf : ∀ j < N + 1, ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.MemLp (cubeFluctuation R f) p (normalizedCubeMeasure R))
(hg :
∀ j < N + 1,
∀ R ∈ descendantsAtDepth Q j,
MeasureTheory.MemLp (cubeProjection Q (j + 1) g) (cubeBesovConjExponent p) (normalizedCubeMeasure R))
:
|cubeBesovPairing Q f (cubeProjection Q (N + 1) g)| ≤ max 1 (3 ^ s) * cubeBesovPartialNormTop Q s p N f * cubeBesovCircPartialNorm Q s (cubeBesovConjExponent p) 1 (N + 1) g
theorem
HCPolySupport.abs_cubeBesovPairing_projection_le_max_partialOne_circTop
{d : ℕ}
(Q : TriadicCube d)
(s : ℝ)
(p : ENNReal)
(f g : Vec d → ℝ)
(N : ℕ)
(hgInt : MeasureTheory.IntegrableOn g (cubeSet Q) MeasureTheory.volume)
(hp : 1 ≤ p)
(hpTop : p ≠ ⊤)
(hpConjTop : cubeBesovConjExponent p ≠ ⊤)
(hf : ∀ j < N + 1, ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.MemLp (cubeFluctuation R f) p (normalizedCubeMeasure R))
(hg :
∀ j < N + 1,
∀ R ∈ descendantsAtDepth Q j,
MeasureTheory.MemLp (cubeProjection Q (j + 1) g) (cubeBesovConjExponent p) (normalizedCubeMeasure R))
:
|cubeBesovPairing Q f (cubeProjection Q (N + 1) g)| ≤ max 1 (3 ^ s) * cubeBesovPartialNorm Q s p 1 N f * cubeBesovCircPartialNormTop Q s (cubeBesovConjExponent p) (N + 1) g