Coarse-graining support: Support.Besov.Duality.ProjectedPairing.Integrability #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.integrableOn_of_integrable_normalizedCubeMeasure
{d : ℕ}
(Q : TriadicCube d)
{f : Vec d → ℝ}
(hf : MeasureTheory.Integrable f (normalizedCubeMeasure Q))
:
theorem
HCPolySupport.integrableOn_mul_projectionResidual_projection_succ_of_mem_descendantsAtDepth
{d : ℕ}
{Q R : TriadicCube d}
{j : ℕ}
(p : ENNReal)
(f g : Vec d → ℝ)
(hR : R ∈ descendantsAtDepth Q j)
(hf : MeasureTheory.MemLp (cubeFluctuation R f) p (normalizedCubeMeasure R))
(hg : MeasureTheory.MemLp (cubeProjection Q (j + 1) g) (cubeBesovConjExponent p) (normalizedCubeMeasure R))
(hp : 1 ≤ p)
:
MeasureTheory.IntegrableOn (fun (x : Vec d) => cubeProjection Q (j + 1) g x * cubeProjectionResidual Q j f x)
(cubeSet R) MeasureTheory.volume
theorem
HCPolySupport.integrableOn_mul_projection_of_mem_descendantsAtDepth
{d : ℕ}
{Q R : TriadicCube d}
{j : ℕ}
(p : ENNReal)
(f g : Vec d → ℝ)
(hR : R ∈ descendantsAtDepth Q j)
(hf : MeasureTheory.MemLp (cubeFluctuation R f) p (normalizedCubeMeasure R))
(hp : 1 ≤ p)
:
MeasureTheory.IntegrableOn (fun (x : Vec d) => f x * cubeProjection Q j g x) (cubeSet R) MeasureTheory.volume
theorem
HCPolySupport.integrableOn_mul_projection_succ_of_mem_descendantsAtDepth
{d : ℕ}
{Q R : TriadicCube d}
{j : ℕ}
(p : ENNReal)
(f g : Vec d → ℝ)
(hR : R ∈ descendantsAtDepth Q j)
(hf : MeasureTheory.MemLp (cubeFluctuation R f) p (normalizedCubeMeasure R))
(hg : MeasureTheory.MemLp (cubeProjection Q (j + 1) g) (cubeBesovConjExponent p) (normalizedCubeMeasure R))
(hp : 1 ≤ p)
:
MeasureTheory.IntegrableOn (fun (x : Vec d) => f x * cubeProjection Q (j + 1) g x) (cubeSet R) MeasureTheory.volume
theorem
HCPolySupport.cubeAverage_cubeProjectionResidual_depth_zero_eq_zero_of_memLp
{d : ℕ}
(Q : TriadicCube d)
(p : ENNReal)
(f : Vec d → ℝ)
(hf : MeasureTheory.MemLp (cubeProjectionResidual Q 0 f) p (normalizedCubeMeasure Q))
(hp : 1 ≤ p)
: