Coarse-graining support: Support.Besov.Duality.ProjectedPairing.Projections #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.cubeProjection_one_memLp
{d : ℕ}
(Q : TriadicCube d)
(p : ENNReal)
(g : Vec d → ℝ)
:
MeasureTheory.MemLp (cubeProjection Q 1 g) p (normalizedCubeMeasure Q)
theorem
HCPolySupport.cubeProjection_succ_ae_eq_cubeProjection_one_of_mem_descendantsAtDepth
{d : ℕ}
{Q R : TriadicCube d}
{j : ℕ}
(g : Vec d → ℝ)
(hR : R ∈ descendantsAtDepth Q j)
:
cubeProjection Q (j + 1) g =ᵐ[normalizedCubeMeasure R] cubeProjection R 1 g
theorem
HCPolySupport.cubeProjection_succ_memLp_of_mem_descendantsAtDepth
{d : ℕ}
{Q R : TriadicCube d}
{j : ℕ}
(p : ENNReal)
(g : Vec d → ℝ)
(hR : R ∈ descendantsAtDepth Q j)
:
MeasureTheory.MemLp (cubeProjection Q (j + 1) g) p (normalizedCubeMeasure R)
theorem
HCPolySupport.descendantsAverage_cubeLpNorm_projection_succ_eq_cubeBesovCircDepthAverage
{d : ℕ}
(Q : TriadicCube d)
(p : ENNReal)
(g : Vec d → ℝ)
(j : ℕ)
(hp0 : p ≠ 0)
(hpTop : p ≠ ⊤)
(hg : ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.MemLp (cubeProjection Q (j + 1) g) p (normalizedCubeMeasure R))
:
(descendantsAverage Q j fun (R : TriadicCube d) => cubeLpNorm R p (cubeProjection Q (j + 1) g) ^ p.toReal) = cubeBesovCircDepthAverage Q p g (j + 1)
theorem
HCPolySupport.abs_cubeAverage_mul_projection_succ_projectionResidual_le_mul_cubeBesovCircDepthAverage
{d : ℕ}
(Q : TriadicCube d)
(p : ENNReal)
(f g : Vec d → ℝ)
(j : ℕ)
(hp : 1 ≤ p)
(_hp0 : p ≠ 0)
(hpTop : p ≠ ⊤)
(hpConjTop : cubeBesovConjExponent p ≠ ⊤)
(hf : ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.MemLp (cubeFluctuation R f) p (normalizedCubeMeasure R))
(hg :
∀ R ∈ descendantsAtDepth Q j,
MeasureTheory.MemLp (cubeProjection Q (j + 1) g) (cubeBesovConjExponent p) (normalizedCubeMeasure R))
:
|cubeAverage Q fun (x : Vec d) => cubeProjection Q (j + 1) g x * cubeProjectionResidual Q j f x| ≤ cubeBesovCircDepthAverage Q (cubeBesovConjExponent p) g (j + 1) ^ (1 / (cubeBesovConjExponent p).toReal) * cubeBesovDepthAverage Q p f j ^ (1 / p.toReal)