Coarse-graining support: Support.Besov.Poincare.Bounds #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.cubeBesovDepthWeight_mul_cubeBesovCircDepthSeminorm_shift_eq_geom_mul
{d : ℕ}
(Q : TriadicCube d)
(s : ℝ)
(p : ENNReal)
(u : Vec d → ℝ)
(j n : ℕ)
:
cubeBesovDepthWeight Q s j * cubeBesovCircDepthSeminorm Q 1 p u (j + n) = (3 ^ (-s)) ^ n * cubeBesovCircDepthSeminorm Q (1 - s) p u (j + n)
theorem
HCPolySupport.cubeBesovDepthSeminorm_two_le_weighted_shifted_of_local_circ_bound
{d : ℕ}
(Q : TriadicCube d)
(s C : ℝ)
(u g : Vec d → ℝ)
(j N : ℕ)
(hC : 0 ≤ C)
(hlocal :
∀ R ∈ descendantsAtDepth Q j,
cubeBesovOscillation R 2 u ≤ C * ∑ n ∈ Finset.range (N + 1), cubeBesovCircDepthSeminorm R 1 2 g n)
:
cubeBesovDepthSeminorm Q s 2 u j ≤ C * ∑ n ∈ Finset.range (N + 1), (3 ^ (-s)) ^ n * cubeBesovCircDepthSeminorm Q (1 - s) 2 g (j + n)
theorem
HCPolySupport.cubeBesovDepthWeight_mul_sum_shifted_cubeBesovCircDepthSeminorm_one_le
{d : ℕ}
(Q : TriadicCube d)
(s : ℝ)
(p : ENNReal)
(g : Vec d → ℝ)
(j N : ℕ)
(hs : 0 ≤ s)
:
cubeBesovDepthWeight Q s j * ∑ n ∈ Finset.range (N + 1), cubeBesovCircDepthSeminorm Q 1 p g (j + n) ≤ ∑ n ∈ Finset.range (N + 1), cubeBesovCircDepthSeminorm Q (1 - s) p g (j + n)
theorem
HCPolySupport.cubeBesovDepthSeminorm_two_le_geometric_mul_cubeBesovCircPartialNorm_of_local_circ_bound
{d : ℕ}
(Q : TriadicCube d)
(s C : ℝ)
(u g : Vec d → ℝ)
(j N : ℕ)
(hs : 0 < s)
(hC : 0 ≤ C)
(hlocal :
∀ R ∈ descendantsAtDepth Q j,
cubeBesovOscillation R 2 u ≤ C * ∑ n ∈ Finset.range (N + 1), cubeBesovCircDepthSeminorm R 1 2 g n)
:
theorem
HCPolySupport.cubeBesovDepthSeminorm_two_le_cubeBesovCircPartialNorm_of_local_circ_bound
{d : ℕ}
(Q : TriadicCube d)
(s C : ℝ)
(u g : Vec d → ℝ)
(j N : ℕ)
(hs : 0 ≤ s)
(hC : 0 ≤ C)
(hlocal :
∀ R ∈ descendantsAtDepth Q j,
cubeBesovOscillation R 2 u ≤ C * ∑ n ∈ Finset.range (N + 1), cubeBesovCircDepthSeminorm R 1 2 g n)
:
theorem
HCPolySupport.cubeBesovPartialSeminormTop_two_le_geometric_mul_cubeBesovCircPartialNorm_of_local_circ_bound
{d : ℕ}
(Q : TriadicCube d)
(s C : ℝ)
(u g : Vec d → ℝ)
(M : ℕ)
(hs : 0 < s)
(hC : 0 ≤ C)
(hlocal :
∀ j ∈ Finset.range (M + 1),
∀ R ∈ descendantsAtDepth Q j,
cubeBesovOscillation R 2 u ≤ C * ∑ n ∈ Finset.range (M - j + 1), cubeBesovCircDepthSeminorm R 1 2 g n)
:
cubeBesovPartialSeminormTop Q s 2 M u ≤ C * (1 - 3 ^ (-s))⁻¹ * cubeBesovCircPartialNorm Q (1 - s) 2 1 M g
theorem
HCPolySupport.cubeBesovPartialSeminormTop_two_le_cubeBesovCircPartialNorm_of_local_circ_bound
{d : ℕ}
(Q : TriadicCube d)
(s C : ℝ)
(u g : Vec d → ℝ)
(M : ℕ)
(hs : 0 ≤ s)
(hC : 0 ≤ C)
(hlocal :
∀ j ∈ Finset.range (M + 1),
∀ R ∈ descendantsAtDepth Q j,
cubeBesovOscillation R 2 u ≤ C * ∑ n ∈ Finset.range (M - j + 1), cubeBesovCircDepthSeminorm R 1 2 g n)
:
theorem
HCPolySupport.cubeBesovPartialNormTop_eq_cubeBesovPartialSeminormTop_of_cubeAverage_eq_zero
{d : ℕ}
(Q : TriadicCube d)
(s : ℝ)
(p : ENNReal)
(N : ℕ)
(u : Vec d → ℝ)
(havg : cubeAverage Q u = 0)
:
theorem
HCPolySupport.CubeMultiscalePoincareInput.partialSeminormTop_le_circPartialNorm
{d : ℕ}
{Q : TriadicCube d}
{s C : ℝ}
{u g : Vec d → ℝ}
{M : ℕ}
(hinput : CubeMultiscalePoincareInput Q C u g M)
(hs : 0 ≤ s)
(hC : 0 ≤ C)
:
theorem
HCPolySupport.CubeMultiscalePoincareInput.partialSeminorm_le_geometricCircNorm
{d : ℕ}
{Q : TriadicCube d}
{s C : ℝ}
{u g : Vec d → ℝ}
{M : ℕ}
(hinput : CubeMultiscalePoincareInput Q C u g M)
(hs : 0 < s)
(hC : 0 ≤ C)
:
cubeBesovPartialSeminormTop Q s 2 M u ≤ C * (1 - 3 ^ (-s))⁻¹ * cubeBesovCircPartialNorm Q (1 - s) 2 1 M g
theorem
HCPolySupport.CubeMultiscalePoincareInput.partialNormTop_two_le_cubeBesovCircPartialNorm
{d : ℕ}
{Q : TriadicCube d}
{s C : ℝ}
{u g : Vec d → ℝ}
{M : ℕ}
(hinput : CubeMultiscalePoincareInput Q C u g M)
(havg : cubeAverage Q u = 0)
(hs : 0 ≤ s)
(hC : 0 ≤ C)
:
theorem
HCPolySupport.CubeMultiscalePoincareInput.partialNormTop_le_geometricCircNorm
{d : ℕ}
{Q : TriadicCube d}
{s C : ℝ}
{u g : Vec d → ℝ}
{M : ℕ}
(hinput : CubeMultiscalePoincareInput Q C u g M)
(havg : cubeAverage Q u = 0)
(hs : 0 < s)
(hC : 0 ≤ C)
:
cubeBesovPartialNormTop Q s 2 M u ≤ C * (1 - 3 ^ (-s))⁻¹ * cubeBesovCircPartialNorm Q (1 - s) 2 1 M g
theorem
HCPolySupport.CubeLocalMultiscalePoincareEstimate.partialSeminormTop_le_circPartialNorm
{d : ℕ}
{Q : TriadicCube d}
{s C : ℝ}
{u g : Vec d → ℝ}
{M : ℕ}
(hlocal : CubeLocalMultiscalePoincareEstimate Q C u g M)
(hs : 0 ≤ s)
(hC : 0 ≤ C)
:
theorem
HCPolySupport.CubeLocalMultiscalePoincareEstimate.partialSeminorm_le_geometricCircNorm
{d : ℕ}
{Q : TriadicCube d}
{s C : ℝ}
{u g : Vec d → ℝ}
{M : ℕ}
(hlocal : CubeLocalMultiscalePoincareEstimate Q C u g M)
(hs : 0 < s)
(hC : 0 ≤ C)
:
cubeBesovPartialSeminormTop Q s 2 M u ≤ C * (1 - 3 ^ (-s))⁻¹ * cubeBesovCircPartialNorm Q (1 - s) 2 1 M g
theorem
HCPolySupport.CubeLocalMultiscalePoincareEstimate.partialNormTop_two_le_cubeBesovCircPartialNorm
{d : ℕ}
{Q : TriadicCube d}
{s C : ℝ}
{u g : Vec d → ℝ}
{M : ℕ}
(hlocal : CubeLocalMultiscalePoincareEstimate Q C u g M)
(havg : cubeAverage Q u = 0)
(hs : 0 ≤ s)
(hC : 0 ≤ C)
:
theorem
HCPolySupport.CubeLocalMultiscalePoincareEstimate.partialNormTop_le_geometricCircNorm
{d : ℕ}
{Q : TriadicCube d}
{s C : ℝ}
{u g : Vec d → ℝ}
{M : ℕ}
(hlocal : CubeLocalMultiscalePoincareEstimate Q C u g M)
(havg : cubeAverage Q u = 0)
(hs : 0 < s)
(hC : 0 ≤ C)
:
cubeBesovPartialNormTop Q s 2 M u ≤ C * (1 - 3 ^ (-s))⁻¹ * cubeBesovCircPartialNorm Q (1 - s) 2 1 M g
theorem
HCPolySupport.CubeLocalMultiscalePoincareEstimate.fluctuationNormTop_le_circPartialNorm
{d : ℕ}
{Q : TriadicCube d}
{s C : ℝ}
{u g : Vec d → ℝ}
{M : ℕ}
(hlocal : CubeLocalMultiscalePoincareEstimate Q C (cubeFluctuation Q u) g M)
(hs : 0 ≤ s)
(hC : 0 ≤ C)
:
cubeBesovPartialNormTop Q s 2 M (cubeFluctuation Q u) ≤ C * cubeBesovCircPartialNorm Q (1 - s) 2 1 M g
theorem
HCPolySupport.CubeLocalMultiscalePoincareEstimate.fluctuationNormTop_le_geometricCircNorm
{d : ℕ}
{Q : TriadicCube d}
{s C : ℝ}
{u g : Vec d → ℝ}
{M : ℕ}
(hlocal : CubeLocalMultiscalePoincareEstimate 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))⁻¹ * cubeBesovCircPartialNorm Q (1 - s) 2 1 M g
theorem
HCPolySupport.CubeDescendantProjectedDualMeanZeroPoincareEstimate.partialSeminormTop_le_circPartialNorm
{d : ℕ}
{Q : TriadicCube d}
{s C : ℝ}
{u g : Vec d → ℝ}
{M : ℕ}
(hproj : CubeDescendantProjectedDualMeanZeroPoincareEstimate Q C u g M)
(hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q))
(hs : 0 ≤ s)
(hC : 0 ≤ C)
:
cubeBesovPartialSeminormTop Q s 2 M u ≤ 3 / 2 * C * 3 ^ (↑d + 1) * cubeBesovCircPartialNorm Q (1 - s) 2 1 M g
theorem
HCPolySupport.CubeDescendantProjectedDualMeanZeroPoincareEstimate.partialSeminorm_le_geometricCircNorm
{d : ℕ}
{Q : TriadicCube d}
{s C : ℝ}
{u g : Vec d → ℝ}
{M : ℕ}
(hproj : CubeDescendantProjectedDualMeanZeroPoincareEstimate Q C u g M)
(hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q))
(hs : 0 < s)
(hC : 0 ≤ C)
:
theorem
HCPolySupport.CubeDescendantProjectedDualMeanZeroPoincareEstimate.partialNormTop_two_le_cubeBesovCircPartialNorm
{d : ℕ}
{Q : TriadicCube d}
{s C : ℝ}
{u g : Vec d → ℝ}
{M : ℕ}
(hproj : CubeDescendantProjectedDualMeanZeroPoincareEstimate Q C u g M)
(hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q))
(havg : cubeAverage Q u = 0)
(hs : 0 ≤ s)
(hC : 0 ≤ C)
:
cubeBesovPartialNormTop Q s 2 M u ≤ 3 / 2 * C * 3 ^ (↑d + 1) * cubeBesovCircPartialNorm Q (1 - s) 2 1 M g
theorem
HCPolySupport.CubeDescendantProjectedDualMeanZeroPoincareEstimate.partialNormTop_le_geometricCircNorm
{d : ℕ}
{Q : TriadicCube d}
{s C : ℝ}
{u g : Vec d → ℝ}
{M : ℕ}
(hproj : CubeDescendantProjectedDualMeanZeroPoincareEstimate Q C u g M)
(hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q))
(havg : cubeAverage Q u = 0)
(hs : 0 < s)
(hC : 0 ≤ C)
:
theorem
HCPolySupport.CubeDescendantProjectedDualMeanZeroPoincareEstimate.fluctuationNormTop_le_circPartialNorm
{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)
:
cubeBesovPartialNormTop Q s 2 M (cubeFluctuation Q u) ≤ 3 / 2 * C * 3 ^ (↑d + 1) * cubeBesovCircPartialNorm Q (1 - s) 2 1 M g
theorem
HCPolySupport.CubeDescendantProjectedDualMeanZeroPoincareEstimate.fluctuationNormTop_le_geometricCircNorm
{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)
:
cubeBesovPartialNormTop Q s 2 M (cubeFluctuation Q u) ≤ 3 / 2 * C * 3 ^ (↑d + 1) * (1 - 3 ^ (-s))⁻¹ * cubeBesovCircPartialNorm Q (1 - s) 2 1 M g
theorem
HCPolySupport.CubeDescendantProjectedDualMeanZeroPoincareEstimate.fluctuationPartialNorm_le_scaledCircNorm
{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)
:
cubeBesovPartialNormTop Q s 2 M (cubeFluctuation Q u) ≤ 3 / 2 * C * 3 ^ (↑d + 1) * cubeBesovCircPartialNorm Q (1 - s) 2 1 M g
theorem
HCPolySupport.CubeDescendantProjectedDualMeanZeroPoincareEstimate.fluctuation_partialNormTop_two_le_note_rhs
{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)
:
cubeBesovPartialNormTop Q s 2 M (cubeFluctuation Q u) ≤ 3 / 2 * C * 3 ^ (↑d + 1) * (1 - 3 ^ (-s))⁻¹ * cubeBesovCircPartialNorm Q (1 - s) 2 1 M g