Coarse-graining support: Support.Besov.Poincare.HarmonicGradient.FullCirc #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Full-Circ Vector Poincare Estimates #
theorem
HCPolySupport.CubeDescendantDualFullVectorPoincareEstimate.to_localFullCircEstimate
{d : ℕ}
{Q : TriadicCube d}
{C : ℝ}
{u : Vec d → ℝ}
{G : Vec d → Vec d}
{M : ℕ}
(hfull : CubeDescendantDualFullVectorPoincareEstimate Q C u G M)
(hG : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => G x i) 2 (normalizedCubeMeasure Q))
(hC : 0 ≤ C)
:
CubeLocalFullCircPoincareVectorEstimate Q (C * 3 ^ (↑d + 1)) u G M
A descendant full-dual vector Poincare estimate gives a descendant local full-circ estimate after applying circ domination componentwise.
theorem
HCPolySupport.tendsto_cubeBesovCircPartialNorm_one_succ_to_cubeBesovCircNorm
{d : ℕ}
(Q : TriadicCube d)
(s : ℝ)
(p : ENNReal)
(u : Vec d → ℝ)
(hBdd : BddAbove (cubeBesovCircNormValueSet Q s p 1 u))
:
Filter.Tendsto (fun (N : ℕ) => cubeBesovCircPartialNorm Q s p 1 (N + 1) u) Filter.atTop
(nhds (cubeBesovCircNorm Q s p 1 u))
For q = 1, finite circ partial norms increase to the full circ norm.
theorem
HCPolySupport.cubeBesovDepthWeight_mul_L2_descendantsAverage_sum_components_circPartialNorm_le_sum_circNorm
{d : ℕ}
(Q : TriadicCube d)
(s : ℝ)
(G : Vec d → Vec d)
(j N : ℕ)
(hs0 : 0 ≤ s)
(hs1 : s < 1)
(hG : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => G x i) 2 (normalizedCubeMeasure Q))
:
cubeBesovDepthWeight Q s j * (descendantsAverage Q j fun (R : TriadicCube d) =>
(∑ i : Fin d, cubeBesovCircPartialNorm R 1 2 1 (N + 1) fun (x : Vec d) => G x i) ^ 2) ^ (1 / 2) ≤ ∑ i : Fin d, cubeBesovCircNorm Q (1 - s) 2 1 fun (x : Vec d) => G x i
Finite local circ partial sums, averaged over descendants and shifted to the parent, are controlled by the full parent circ norm.
theorem
HCPolySupport.tendsto_depthWeight_L2_descendantCircPartial_toCircNorm
{d : ℕ}
(Q : TriadicCube d)
(s : ℝ)
(G : Vec d → Vec d)
(j : ℕ)
(hG : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => G x i) 2 (normalizedCubeMeasure Q))
:
Filter.Tendsto
(fun (N : ℕ) =>
cubeBesovDepthWeight Q s j * (descendantsAverage Q j fun (R : TriadicCube d) =>
(∑ i : Fin d, cubeBesovCircPartialNorm R 1 2 1 (N + 1) fun (x : Vec d) => G x i) ^ 2) ^ (1 / 2))
Filter.atTop
(nhds
(cubeBesovDepthWeight Q s j * (descendantsAverage Q j fun (R : TriadicCube d) =>
(∑ i : Fin d, cubeBesovCircNorm R 1 2 1 fun (x : Vec d) => G x i) ^ 2) ^ (1 / 2)))
The finite local partial-sum averages converge to the corresponding full local circ averages.
theorem
HCPolySupport.cubeBesovDepthWeight_mul_L2_descendantsAverage_sum_components_circNorm_le_sum_circNorm
{d : ℕ}
(Q : TriadicCube d)
(s : ℝ)
(G : Vec d → Vec d)
(j : ℕ)
(hs0 : 0 ≤ s)
(hs1 : s < 1)
(hG : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => G x i) 2 (normalizedCubeMeasure Q))
:
cubeBesovDepthWeight Q s j * (descendantsAverage Q j fun (R : TriadicCube d) =>
(∑ i : Fin d, cubeBesovCircNorm R 1 2 1 fun (x : Vec d) => G x i) ^ 2) ^ (1 / 2) ≤ ∑ i : Fin d, cubeBesovCircNorm Q (1 - s) 2 1 fun (x : Vec d) => G x i
The full local circ averages over descendants are controlled by the full parent circ norm.
theorem
HCPolySupport.cubeBesovDepthSeminorm_two_le_sum_circNorm_of_vector_local_full_circ_bound
{d : ℕ}
(Q : TriadicCube d)
(s C : ℝ)
(u : Vec d → ℝ)
(G : Vec d → Vec d)
(j : ℕ)
(hs0 : 0 ≤ s)
(hs1 : s < 1)
(hC : 0 ≤ C)
(hG : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => G x i) 2 (normalizedCubeMeasure Q))
(hlocal :
∀ R ∈ descendantsAtDepth Q j,
cubeBesovOscillation R 2 u ≤ C * ∑ i : Fin d, cubeBesovCircNorm R 1 2 1 fun (x : Vec d) => G x i)
:
cubeBesovDepthSeminorm Q s 2 u j ≤ C * ∑ i : Fin d, cubeBesovCircNorm Q (1 - s) 2 1 fun (x : Vec d) => G x i
Depthwise positive Besov control from a vector local full-circ Poincare bound.
theorem
HCPolySupport.CubeLocalFullCircPoincareVectorEstimate.partialSeminormTop_two_le_sum_circNorm
{d : ℕ}
{Q : TriadicCube d}
{s C : ℝ}
{u : Vec d → ℝ}
{G : Vec d → Vec d}
{M : ℕ}
(hlocal : CubeLocalFullCircPoincareVectorEstimate Q C u G M)
(hG : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => G x i) 2 (normalizedCubeMeasure Q))
(hs0 : 0 ≤ s)
(hs1 : s < 1)
(hC : 0 ≤ C)
:
cubeBesovPartialSeminormTop Q s 2 M u ≤ C * ∑ i : Fin d, cubeBesovCircNorm Q (1 - s) 2 1 fun (x : Vec d) => G x i
Finite-depth q = ∞ positive Besov control from vector local full-circ
Poincare.
theorem
HCPolySupport.CubeLocalFullCircPoincareVectorEstimate.fluctuationPartialTop_le_sumCircNorm
{d : ℕ}
{Q : TriadicCube d}
{s C : ℝ}
{u : Vec d → ℝ}
{G : Vec d → Vec d}
{M : ℕ}
(hlocal : CubeLocalFullCircPoincareVectorEstimate Q C (cubeFluctuation Q u) G M)
(hG : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => G x i) 2 (normalizedCubeMeasure Q))
(hs0 : 0 ≤ s)
(hs1 : s < 1)
(hC : 0 ≤ C)
:
cubeBesovPartialNormTop Q s 2 M (cubeFluctuation Q u) ≤ C * ∑ i : Fin d, cubeBesovCircNorm Q (1 - s) 2 1 fun (x : Vec d) => G x i
Fluctuation form of the finite-depth full-circ Poincare-to-Besov bound.