Coarse-graining support: #
Support.Deterministic.CoarseCaccioppoli.CutoffProduct.SplitPairing.Centered
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.abs_cubeAverage_vecDot_centered_scalar_smul_le_collapsed_note_terms_of_contDiff_component_bound
{d : ℕ}
(Q : TriadicCube d)
(s : ℝ)
(flux : Vec d → Vec d)
(u g : Vec d → ℝ)
(ξ : Vec d → Vec d)
{Bu Bavg Bcirc1 BcircS B C Bg : ℝ}
(hB : 0 ≤ B)
(hs0 : 0 < s)
(hs1 : s < 1)
(hflux : MeasureTheory.MemLp flux 2 (normalizedCubeMeasure Q))
(hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
(hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q))
(hξLp : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q))
(hBg : 0 ≤ Bg)
(hBavg : 0 ≤ Bavg)
(hC : 0 ≤ C)
(havg : ‖cubeAverageVec Q flux‖ ≤ Bavg)
(hneg : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q s N flux ≤ Bu)
(hproj : ∀ (N : ℕ), CubeDescendantProjectedDualMeanZeroPoincareEstimate Q C (cubeFluctuation Q u) g N)
(hξ : ∀ (i : Fin d), ContDiff ℝ ↑⊤ fun (x : Vec d) => ξ x i)
(hderiv : ∀ (i : Fin d), ∀ z ∈ cubeSet Q, ‖fderiv ℝ (fun (x : Vec d) => ξ x i) z‖ ≤ B)
(hneg1 : ∀ (N : ℕ), cubeBesovCircPartialNorm Q 1 2 1 N g ≤ Bcirc1)
(hnegS : ∀ (N : ℕ), cubeBesovCircPartialNorm Q (1 - s) 2 1 N g ≤ BcircS)
(hBg_bound :
2 * (cubeScaleFactor Q * B * (√(1 - Real.rpow 3 (2 * (s - 1)))⁻¹ * (3 / 2 * C * 3 ^ (↑d + 1) * Bcirc1)) + cubeLpNorm Q ⊤ ξ * (cubeBesovScaleWeight (-s) Q * (3 / 2 * C * 3 ^ (↑d + 1) * (1 - 3 ^ (-s))⁻¹ * BcircS))) ≤ Bg)
:
theorem
HCPolySupport.abs_cubeAverage_vectorDot_centered_scalar_smul_le_collapsed_sharp_note_terms
{d : ℕ}
(Q : TriadicCube d)
(s : ℝ)
(flux : Vec d → Vec d)
(u g : Vec d → ℝ)
(ξ : Vec d → Vec d)
{Bu Bavg Bcirc1 BcircS B C Bg : ℝ}
(hB : 0 ≤ B)
(hs0 : 0 < s)
(hs1 : s < 1)
(hflux : MeasureTheory.MemLp flux 2 (normalizedCubeMeasure Q))
(hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
(hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q))
(hξLp : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q))
(hBg : 0 ≤ Bg)
(hBavg : 0 ≤ Bavg)
(hC : 0 ≤ C)
(havg : ‖cubeAverageVec Q flux‖ ≤ Bavg)
(hneg : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q s N flux ≤ Bu)
(hproj : ∀ (N : ℕ), CubeDescendantProjectedDualMeanZeroPoincareEstimate Q C (cubeFluctuation Q u) g N)
(hξ : ∀ (i : Fin d), ContDiff ℝ ↑⊤ fun (x : Vec d) => ξ x i)
(hderiv : ∀ (i : Fin d), ∀ z ∈ cubeSet Q, ‖fderiv ℝ (fun (x : Vec d) => ξ x i) z‖ ≤ B)
(hneg1 : ∀ (N : ℕ), cubeBesovCircPartialNorm Q 1 2 1 N g ≤ Bcirc1)
(hnegS : ∀ (N : ℕ), cubeBesovCircPartialNorm Q (1 - s) 2 1 N g ≤ BcircS)
(hBg_bound :
2 * (cubeScaleFactor Q * B * (√(1 - Real.rpow 3 (2 * (s - 1)))⁻¹ * (3 / 2 * C * 3 ^ (↑d + 1) * Bcirc1)) + cubeLpNorm Q ⊤ ξ * (cubeBesovScaleWeight (-s) Q * (3 / 2 * C * 3 ^ (↑d + 1) * (1 - 3 ^ (-s))⁻¹ * BcircS))) ≤ Bg)
:
theorem
HCPolySupport.abs_cubeAverage_vectorDot_centered_scalar_smul_le_collapsed_note_terms
{d : ℕ}
(Q : TriadicCube d)
(s : ℝ)
(flux : Vec d → Vec d)
(u : Vec d → ℝ)
(G ξ : Vec d → Vec d)
{Bu Bavg Bcirc1 BcircS B C Bg : ℝ}
(hB : 0 ≤ B)
(hs0 : 0 < s)
(hs1 : s < 1)
(hflux : MeasureTheory.MemLp flux 2 (normalizedCubeMeasure Q))
(hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
(hG : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => G x i) 2 (normalizedCubeMeasure Q))
(hξLp : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q))
(hBg : 0 ≤ Bg)
(hBavg : 0 ≤ Bavg)
(hC : 0 ≤ C)
(hBcircS : 0 ≤ BcircS)
(havg : ‖cubeAverageVec Q flux‖ ≤ Bavg)
(hneg : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q s N flux ≤ Bu)
(hproj : ∀ (N : ℕ), CubeDescendantProjectedDualMeanZeroVectorPoincareEstimate Q C (cubeFluctuation Q u) G N)
(hξ : ∀ (i : Fin d), ContDiff ℝ ↑⊤ fun (x : Vec d) => ξ x i)
(hderiv : ∀ (i : Fin d), ∀ z ∈ cubeSet Q, ‖fderiv ℝ (fun (x : Vec d) => ξ x i) z‖ ≤ B)
(hGcirc1 : ∀ (i : Fin d) (N : ℕ), (cubeBesovCircPartialNorm Q 1 2 1 N fun (x : Vec d) => G x i) ≤ Bcirc1)
(hGcircS : ∀ (i : Fin d) (N : ℕ), (cubeBesovCircPartialNorm Q (1 - s) 2 1 N fun (x : Vec d) => G x i) ≤ BcircS)
(hBg_bound :
2 * (cubeScaleFactor Q * B * (√(1 - Real.rpow 3 (2 * (s - 1)))⁻¹ * (3 / 2 * C * 3 ^ (↑d + 1) * (↑(Fintype.card (Fin d)) * Bcirc1))) + cubeLpNorm Q ⊤ ξ * (cubeBesovScaleWeight (-s) Q * (3 / 2 * C * 3 ^ (↑d + 1) * (1 - 3 ^ (-s))⁻¹ * (↑(Fintype.card (Fin d)) * BcircS)))) ≤ Bg)
:
|cubeAverage Q fun (x : Vec d) => vecDot (flux x) ((u x - cubeAverage Q u) • ξ x)| ≤ ↑d * (Bavg * (cubeLpNorm Q ⊤ ξ * (3 / 2 * C * 3 ^ (↑d + 1) * (↑(Fintype.card (Fin d)) * Bcirc1)))) + ↑d * ((3 ^ (↑d + s) * (cubeBesovScaleWeight (-s) Q * Bu) + cubeBesovScaleWeight s Q * Bavg) * (cubeBesovScaleWeight s Q * Bg))
theorem
HCPolySupport.abs_cubeAverage_vectorDot_centered_scalar_smul_le_collapsed_sharp_note_of_vector
{d : ℕ}
(Q : TriadicCube d)
(s : ℝ)
(flux : Vec d → Vec d)
(u : Vec d → ℝ)
(G ξ : Vec d → Vec d)
{Bu Bavg Bcirc1 BcircS B C Bg : ℝ}
(hB : 0 ≤ B)
(hs0 : 0 < s)
(hs1 : s < 1)
(hflux : MeasureTheory.MemLp flux 2 (normalizedCubeMeasure Q))
(hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
(hG : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => G x i) 2 (normalizedCubeMeasure Q))
(hξLp : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q))
(hBg : 0 ≤ Bg)
(hBavg : 0 ≤ Bavg)
(hC : 0 ≤ C)
(hBcircS : 0 ≤ BcircS)
(havg : ‖cubeAverageVec Q flux‖ ≤ Bavg)
(hneg : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q s N flux ≤ Bu)
(hproj : ∀ (N : ℕ), CubeDescendantProjectedDualMeanZeroVectorPoincareEstimate Q C (cubeFluctuation Q u) G N)
(hξ : ∀ (i : Fin d), ContDiff ℝ ↑⊤ fun (x : Vec d) => ξ x i)
(hderiv : ∀ (i : Fin d), ∀ z ∈ cubeSet Q, ‖fderiv ℝ (fun (x : Vec d) => ξ x i) z‖ ≤ B)
(hGcirc1 : ∀ (i : Fin d) (N : ℕ), (cubeBesovCircPartialNorm Q 1 2 1 N fun (x : Vec d) => G x i) ≤ Bcirc1)
(hGcircS : ∀ (i : Fin d) (N : ℕ), (cubeBesovCircPartialNorm Q (1 - s) 2 1 N fun (x : Vec d) => G x i) ≤ BcircS)
(hBg_bound :
2 * (cubeScaleFactor Q * B * (√(1 - Real.rpow 3 (2 * (s - 1)))⁻¹ * (3 / 2 * C * 3 ^ (↑d + 1) * (↑(Fintype.card (Fin d)) * Bcirc1))) + cubeLpNorm Q ⊤ ξ * (cubeBesovScaleWeight (-s) Q * (3 / 2 * C * 3 ^ (↑d + 1) * (1 - 3 ^ (-s))⁻¹ * (↑(Fintype.card (Fin d)) * BcircS)))) ≤ Bg)
: