Coarse-graining support: Support.Besov.Poincare.HarmonicGradient.LocalMultiscale

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Local Multiscale Vector Poincare Estimates

theorem HCPolySupport.cubeBesovDepthSeminorm_two_le_weighted_circSum_of_localPoincare {d : ℕ} (Q : TriadicCube d) (s C : ℝ) (u : Vec d → ℝ) (G : Vec d → Vec d) (j N : ℕ) (hC : 0 ≤ C) (hlocal : ∀ R ∈ descendantsAtDepth Q j, cubeBesovOscillation R 2 u ≤ C * ∑ i : Fin d, cubeBesovCircPartialNorm R 1 2 1 N fun (x : Vec d) => G x i) : cubeBesovDepthSeminorm Q s 2 u j ≤ C * ∑ i : Fin d, ∑ n ∈ Finset.range (N + 1), (3 ^ (-s)) ^ n * cubeBesovCircDepthSeminorm Q (1 - s) 2 (fun (x : Vec d) => G x i) (j + n)

Depthwise vector version of the multiscale Poincare-to-Besov bookkeeping.

The local input controls oscillation by a sum of componentwise local circ partial norms; after averaging over descendants, the component and depth sums shift to the parent cube.

theorem HCPolySupport.CubeLocalMultiscalePoincareVectorEstimate.partialSeminormTop_two_le_geometric_mul_sum {d : ℕ} {Q : TriadicCube d} {s C : ℝ} {u : Vec d → ℝ} {G : Vec d → Vec d} {M : ℕ} (hlocal : CubeLocalMultiscalePoincareVectorEstimate Q C u G M) (hs : 0 < s) (hC : 0 ≤ C) : cubeBesovPartialSeminormTop Q s 2 M u ≤ C * (1 - 3 ^ (-s))⁻¹ * ∑ i : Fin d, cubeBesovCircPartialNorm Q (1 - s) 2 1 M fun (x : Vec d) => G x i

Finite-depth q = ∞ vector local-multiscale Poincare-to-Besov bound.

theorem HCPolySupport.CubeLocalMultiscalePoincareVectorEstimate.fluctuation_partialNormTop_two_le_geometric_mul_sum {d : ℕ} {Q : TriadicCube d} {s C : ℝ} {u : Vec d → ℝ} {G : Vec d → Vec d} {M : ℕ} (hlocal : CubeLocalMultiscalePoincareVectorEstimate Q C (cubeFluctuation Q u) G M) (hs : 0 < s) (hC : 0 ≤ C) : cubeBesovPartialNormTop Q s 2 M (cubeFluctuation Q u) ≤ C * (1 - 3 ^ (-s))⁻¹ * ∑ i : Fin d, cubeBesovCircPartialNorm Q (1 - s) 2 1 M fun (x : Vec d) => G x i

Finite-depth fluctuation form of the vector local-multiscale Poincare-to-Besov bound.