Coarse-graining support: #
Support.Deterministic.CoarseCaccioppoli.CutoffProduct.PositiveSeminorms.Bounds
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.cubeBesovScaleWeight_neg_mul_cubeBesovDepthWeight_eq_rpow_three_weight
{d : ℕ}
(Q : TriadicCube d)
(s : ℝ)
(j : ℕ)
:
theorem
HCPolySupport.cubeBesovPositiveScalarDepthSeminorm_eq_scaleWeight_neg_mul_cubeBesovDepthSeminorm_two
{d : ℕ}
(Q : TriadicCube d)
(s : ℝ)
(v : Vec d → ℝ)
(j : ℕ)
:
cubeBesovPositiveScalarDepthSeminorm Q s v j = cubeBesovScaleWeight (-s) Q * cubeBesovDepthSeminorm Q s 2 v j
theorem
HCPolySupport.cubeBesovPositiveScalarPartialTwo_eq_weightedPartialTwo
{d : ℕ}
(Q : TriadicCube d)
(s : ℝ)
(N : ℕ)
(v : Vec d → ℝ)
:
cubeBesovPositiveScalarPartialSeminormTwo Q s N v = cubeBesovScaleWeight (-s) Q * cubeBesovPartialSeminorm Q s 2 2 N v
theorem
HCPolySupport.CubeMultiscalePoincareInput.partialSeminorm_two_two_le_geometric_mul_cubeBesovCircPartialNorm
{d : ℕ}
{Q : TriadicCube d}
{s C : ℝ}
{u g : Vec d → ℝ}
{M : ℕ}
(hinput : CubeMultiscalePoincareInput Q C u g M)
(hs : 0 < s)
(hC : 0 ≤ C)
:
cubeBesovPartialSeminorm Q s 2 2 M u ≤ C * (1 - 3 ^ (-s))⁻¹ * cubeBesovCircPartialNorm Q (1 - s) 2 1 M g
theorem
HCPolySupport.depthBesovSeminorm_two_le_weighted_circComponents_of_localBound
{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)
theorem
HCPolySupport.CubeLocalMultiscalePoincareVectorEstimate.partialBesov_two_two_le_bound
{d : ℕ}
{Q : TriadicCube d}
{s C Bcirc : ℝ}
{u : Vec d → ℝ}
{G : Vec d → Vec d}
{M : ℕ}
(hlocal : CubeLocalMultiscalePoincareVectorEstimate Q C u G M)
(hs : 0 < s)
(hC : 0 ≤ C)
(hBcirc : 0 ≤ Bcirc)
(hcirc : ∀ (i : Fin d), (cubeBesovCircPartialNorm Q (1 - s) 2 1 M fun (x : Vec d) => G x i) ≤ Bcirc)
:
theorem
HCPolySupport.CubeLocalMultiscalePoincareVectorEstimate.fluctuationScalarBesov_le_bound
{d : ℕ}
{Q : TriadicCube d}
{s C Bcirc : ℝ}
{u : Vec d → ℝ}
{G : Vec d → Vec d}
{M : ℕ}
(hlocal : CubeLocalMultiscalePoincareVectorEstimate Q C (cubeFluctuation Q u) G M)
(hs : 0 < s)
(hC : 0 ≤ C)
(hBcirc : 0 ≤ Bcirc)
(hcirc : ∀ (i : Fin d), (cubeBesovCircPartialNorm Q (1 - s) 2 1 M fun (x : Vec d) => G x i) ≤ Bcirc)
:
cubeBesovPositiveScalarPartialSeminormTwo Q s M (cubeFluctuation Q u) ≤ cubeBesovScaleWeight (-s) Q * (C * (1 - 3 ^ (-s))⁻¹ * (↑(Fintype.card (Fin d)) * Bcirc))
theorem
HCPolySupport.CubeDescendantProjectedDualMeanZeroVectorPoincareEstimate.fluctuationScalarBesov_le_bound
{d : ℕ}
{Q : TriadicCube d}
{s C Bcirc : ℝ}
{u : Vec d → ℝ}
{G : Vec d → Vec d}
{M : ℕ}
(hproj : CubeDescendantProjectedDualMeanZeroVectorPoincareEstimate Q C (cubeFluctuation Q u) G M)
(hG : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => G x i) 2 (normalizedCubeMeasure Q))
(hs : 0 < s)
(hC : 0 ≤ C)
(hBcirc : 0 ≤ Bcirc)
(hcirc : ∀ (i : Fin d), (cubeBesovCircPartialNorm Q (1 - s) 2 1 M fun (x : Vec d) => G x i) ≤ Bcirc)
:
cubeBesovPositiveScalarPartialSeminormTwo Q s M (cubeFluctuation Q u) ≤ cubeBesovScaleWeight (-s) Q * (3 / 2 * C * 3 ^ (↑d + 1) * (1 - 3 ^ (-s))⁻¹ * (↑(Fintype.card (Fin d)) * Bcirc))
theorem
HCPolySupport.CubeDescendantProjectedDualMeanZeroPoincareEstimate.projectedFluctuation_scalarBesov_le_bound
{d : ℕ}
{Q : TriadicCube d}
{s C : ℝ}
{u g : Vec d → ℝ}
{M : ℕ}
(hproj : CubeDescendantProjectedDualMeanZeroPoincareEstimate Q C (cubeFluctuation Q u) g M)
(hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q))
(hs : 0 < s)
(hC : 0 ≤ C)
:
cubeBesovPositiveScalarPartialSeminormTwo Q s M (cubeFluctuation Q u) ≤ cubeBesovScaleWeight (-s) Q * (3 / 2 * C * 3 ^ (↑d + 1) * (1 - 3 ^ (-s))⁻¹ * cubeBesovCircPartialNorm Q (1 - s) 2 1 M g)