Coarse-graining support: Support.Besov.Duality.ProjectedPairing.Averages #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.cubeAverage_cubeProjectionResidual_eq_zero_of_mem_descendantsAtDepth
{d : ℕ}
{Q R : TriadicCube d}
{j : ℕ}
(p : ENNReal)
(f : Vec d → ℝ)
(hR : R ∈ descendantsAtDepth Q j)
(hf : MeasureTheory.MemLp (cubeFluctuation R f) p (normalizedCubeMeasure R))
(hp : 1 ≤ p)
:
theorem
HCPolySupport.cubeAverage_mul_cubeProjection_cubeProjectionResidual_eq_zero_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)
:
theorem
HCPolySupport.cubeAverage_cubeProjection_eq_cubeAverage_of_mem_descendantsAtDepth
{d : ℕ}
{Q R : TriadicCube d}
{j : ℕ}
(g : Vec d → ℝ)
(hR : R ∈ descendantsAtDepth Q j)
:
theorem
HCPolySupport.integrableOn_cubeProjection_succ_of_mem_descendantsAtDepth
{d : ℕ}
{Q R : TriadicCube d}
{j : ℕ}
(g : Vec d → ℝ)
(hR : R ∈ descendantsAtDepth Q j)
:
MeasureTheory.IntegrableOn (cubeProjection Q (j + 1) g) (cubeSet R) MeasureTheory.volume
theorem
HCPolySupport.cubeAverage_cubeProjection_succ_eq_cubeAverage_of_mem_descendantsAtDepth_of_integrableOn
{d : ℕ}
{Q R : TriadicCube d}
{j : ℕ}
(g : Vec d → ℝ)
(hR : R ∈ descendantsAtDepth Q j)
(hg : MeasureTheory.IntegrableOn g (cubeSet R) MeasureTheory.volume)
:
theorem
HCPolySupport.cubeAverage_mul_projection_projection_succ_eq_mul_projection_projection
{d : ℕ}
{Q R : TriadicCube d}
{j : ℕ}
(f g : Vec d → ℝ)
(hR : R ∈ descendantsAtDepth Q j)
(hg : MeasureTheory.IntegrableOn g (cubeSet R) MeasureTheory.volume)
:
(cubeAverage R fun (x : Vec d) => cubeProjection Q j f x * cubeProjection Q (j + 1) g x) = cubeAverage R fun (x : Vec d) => cubeProjection Q j f x * cubeProjection Q j g x
theorem
HCPolySupport.cubeAverage_mul_projection_eq_mul_projection_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)
:
(cubeAverage R fun (x : Vec d) => f x * cubeProjection Q j g x) = cubeAverage R fun (x : Vec d) => cubeProjection Q j f x * cubeProjection Q j g x
theorem
HCPolySupport.cubeAverage_projectionSucc_eq_cubeAverageProjection_add_projectionResidual
{d : ℕ}
{Q R : TriadicCube d}
{j : ℕ}
(p : ENNReal)
(f g : Vec d → ℝ)
(hR : R ∈ descendantsAtDepth Q j)
(hgInt : MeasureTheory.IntegrableOn g (cubeSet R) MeasureTheory.volume)
(hf : MeasureTheory.MemLp (cubeFluctuation R f) p (normalizedCubeMeasure R))
(hg : MeasureTheory.MemLp (cubeProjection Q (j + 1) g) (cubeBesovConjExponent p) (normalizedCubeMeasure R))
(hp : 1 ≤ p)
:
(cubeAverage R fun (x : Vec d) => f x * cubeProjection Q (j + 1) g x) = (cubeAverage R fun (x : Vec d) => f x * cubeProjection Q j g x) + cubeAverage R fun (x : Vec d) => cubeProjection Q (j + 1) g x * cubeProjectionResidual Q j f x
theorem
HCPolySupport.cubeBesovPairing_projection_zero_eq_cubeAverage_mul_cubeAverage
{d : ℕ}
(Q : TriadicCube d)
(f g : Vec d → ℝ)
:
theorem
HCPolySupport.cubeBesovPairing_projection_succ_eq_projection_add_residual
{d : ℕ}
(Q : TriadicCube d)
(p : ENNReal)
(f g : Vec d → ℝ)
(j : ℕ)
(hgInt : MeasureTheory.IntegrableOn g (cubeSet Q) MeasureTheory.volume)
(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))
(hp : 1 ≤ p)
:
cubeBesovPairing Q f (cubeProjection Q (j + 1) g) = cubeBesovPairing Q f (cubeProjection Q j g) + cubeAverage Q fun (x : Vec d) => cubeProjection Q (j + 1) g x * cubeProjectionResidual Q j f x
theorem
HCPolySupport.cubeBesovPairing_projection_eq_cubeAverage_mul_cubeAverage_add_sum
{d : ℕ}
(Q : TriadicCube d)
(p : ENNReal)
(f g : Vec d → ℝ)
(N : ℕ)
(hgInt : MeasureTheory.IntegrableOn g (cubeSet Q) MeasureTheory.volume)
(hf : ∀ j < N, ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.MemLp (cubeFluctuation R f) p (normalizedCubeMeasure R))
(hg :
∀ j < N,
∀ R ∈ descendantsAtDepth Q j,
MeasureTheory.MemLp (cubeProjection Q (j + 1) g) (cubeBesovConjExponent p) (normalizedCubeMeasure R))
(hp : 1 ≤ p)
:
cubeBesovPairing Q f (cubeProjection Q N g) = cubeAverage Q f * cubeAverage Q g + ∑ j ∈ Finset.range N, cubeAverage Q fun (x : Vec d) => cubeProjection Q (j + 1) g x * cubeProjectionResidual Q j f x
theorem
HCPolySupport.cubeBesovDepthWeight_mul_cubeBesovCircDepthWeight_succ
{d : ℕ}
(Q : TriadicCube d)
(s : ℝ)
(j : ℕ)
:
theorem
HCPolySupport.cubeBesovCircDepthSeminorm_depth_zero_eq_scaleWeight_neg_mul_norm_cubeAverage
{d : ℕ}
(Q : TriadicCube d)
(s : ℝ)
(p : ENNReal)
(u : Vec d → ℝ)
(hp0 : p ≠ 0)
(hpTop : p ≠ ⊤)
:
theorem
HCPolySupport.shifted_cubeBesovCircPartialSeminorm_le_cubeBesovCircPartialNorm
{d : ℕ}
(Q : TriadicCube d)
(s : ℝ)
(p q : ENNReal)
(N : ℕ)
(u : Vec d → ℝ)
(_hq0 : q ≠ 0)
(_hqTop : q ≠ ⊤)
:
(∑ j ∈ Finset.range (N + 1), cubeBesovCircDepthSeminorm Q s p u (j + 1) ^ q.toReal) ^ (1 / q.toReal) ≤ cubeBesovCircPartialNorm Q s p q (N + 1) u
theorem
HCPolySupport.abs_cubeAverage_mul_projection_succ_projectionResidual_le_mul_cubeBesovDepthSeminorm
{d : ℕ}
(Q : TriadicCube d)
(s : ℝ)
(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| ≤ 3 ^ s * cubeBesovDepthSeminorm Q s p f j * cubeBesovCircDepthSeminorm Q s (cubeBesovConjExponent p) g (j + 1)