Coarse-graining support: Support.Deterministic.CoarseCaccioppoli.CutoffProduct.CenteredProduct

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

theorem HCPolySupport.cubeL2ScalarPartialSeminormTwo_le_note_rhs_of_meanZero_projectedDualMeanZeroPoincareEstimate {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (v g : Vec d → ℝ) {C : ℝ} (hv : MeasureTheory.MemLp v 2 (normalizedCubeMeasure Q)) (hproj : CubeDescendantProjectedDualMeanZeroPoincareEstimate Q C v g N) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (havg : cubeAverage Q v = 0) (hs : s < 1) (hC : 0 ≤ C) : cubeL2ScalarPartialSeminormTwo Q (s - 1) N v ≤ √(1 - Real.rpow 3 (2 * (s - 1)))⁻¹ * (3 / 2 * C * 3 ^ (↑d + 1) * cubeBesovCircPartialNorm Q 1 2 1 N g)

theorem HCPolySupport.cubeL2ScalarPartialSeminormTwo_fluctuation_le_note_rhs_of_projectedDualMeanZeroPoincareEstimate {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (u g : Vec d → ℝ) {C : ℝ} (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hproj : CubeDescendantProjectedDualMeanZeroPoincareEstimate Q C (cubeFluctuation Q u) g N) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (hs : s < 1) (hC : 0 ≤ C) : cubeL2ScalarPartialSeminormTwo Q (s - 1) N (cubeFluctuation Q u) ≤ √(1 - Real.rpow 3 (2 * (s - 1)))⁻¹ * (3 / 2 * C * 3 ^ (↑d + 1) * cubeBesovCircPartialNorm Q 1 2 1 N g)

theorem HCPolySupport.cubeLpNorm_two_le_note_rhs_of_meanZero_projectedDualMeanZeroVectorPoincareEstimate {d : ℕ} (Q : TriadicCube d) (N : ℕ) (v : Vec d → ℝ) (G : Vec d → Vec d) {C Bcirc : ℝ} (hproj : CubeDescendantProjectedDualMeanZeroVectorPoincareEstimate Q C v G N) (hG : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => G x i) 2 (normalizedCubeMeasure Q)) (havg : cubeAverage Q v = 0) (hC : 0 ≤ C) (hGcirc : ∀ (i : Fin d), (cubeBesovCircPartialNorm Q 1 2 1 N fun (x : Vec d) => G x i) ≤ Bcirc) : cubeLpNorm Q 2 v ≤ 3 / 2 * C * 3 ^ (↑d + 1) * (↑(Fintype.card (Fin d)) * Bcirc)

theorem HCPolySupport.cubeLpNorm_two_le_note_rhs_of_meanZero_dualFullVectorPoincareEstimate {d : ℕ} (Q : TriadicCube d) (N : ℕ) (v : Vec d → ℝ) (G : Vec d → Vec d) {C Bcirc : ℝ} (hfull : CubeDescendantDualFullVectorPoincareEstimate Q C v G N) (hG : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => G x i) 2 (normalizedCubeMeasure Q)) (havg : cubeAverage Q v = 0) (hC : 0 ≤ C) (hBcirc : 0 ≤ Bcirc) (hGcirc : ∀ (i : Fin d) (M : ℕ), (cubeBesovCircPartialNorm Q 1 2 1 M fun (x : Vec d) => G x i) ≤ Bcirc) : cubeLpNorm Q 2 v ≤ 3 / 2 * C * 3 ^ (↑d + 1) * (↑(Fintype.card (Fin d)) * Bcirc)

Full-dual replacement for cubeLpNorm_two_le_note_rhs_of_meanZero_projectedDualMeanZeroVectorPoincareEstimate.

The corrected full-dual Poincare estimate controls constant gradient modes. Uniform finite-depth circ bounds turn the full circ norm into the same note-shaped component budget used by the projected corridor.

theorem HCPolySupport.cubeL2ScalarPartialSeminormTwo_fluctuation_le_note_rhs {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (u : Vec d → ℝ) (G : Vec d → Vec d) {C Bcirc : ℝ} (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hproj : CubeDescendantProjectedDualMeanZeroVectorPoincareEstimate Q C (cubeFluctuation Q u) G N) (hG : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => G x i) 2 (normalizedCubeMeasure Q)) (hs : s < 1) (hC : 0 ≤ C) (hGcirc : ∀ (i : Fin d), (cubeBesovCircPartialNorm Q 1 2 1 N fun (x : Vec d) => G x i) ≤ Bcirc) : cubeL2ScalarPartialSeminormTwo Q (s - 1) N (cubeFluctuation Q u) ≤ √(1 - Real.rpow 3 (2 * (s - 1)))⁻¹ * (3 / 2 * C * 3 ^ (↑d + 1) * (↑(Fintype.card (Fin d)) * Bcirc))

theorem HCPolySupport.cubeL2ScalarPartialSeminormTwo_fluctuation_le_note_rhs_of_dualFullVectorPoincareEstimate {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (u : Vec d → ℝ) (G : Vec d → Vec d) {C Bcirc : ℝ} (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hfull : CubeDescendantDualFullVectorPoincareEstimate Q C (cubeFluctuation Q u) G N) (hG : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => G x i) 2 (normalizedCubeMeasure Q)) (hs : s < 1) (hC : 0 ≤ C) (hBcirc : 0 ≤ Bcirc) (hGcirc : ∀ (i : Fin d) (M : ℕ), (cubeBesovCircPartialNorm Q 1 2 1 M fun (x : Vec d) => G x i) ≤ Bcirc) : cubeL2ScalarPartialSeminormTwo Q (s - 1) N (cubeFluctuation Q u) ≤ √(1 - Real.rpow 3 (2 * (s - 1)))⁻¹ * (3 / 2 * C * 3 ^ (↑d + 1) * (↑(Fintype.card (Fin d)) * Bcirc))

Full-dual replacement for the L² partial-seminorm estimate used in the centered cutoff-product term.

theorem HCPolySupport.abs_cubeAverage_vectorDot_centered_scalar_smul_le_noteTerms_of_partialBounds {d : ℕ} (Q : TriadicCube d) (s : ℝ) (flux : Vec d → Vec d) (u g : Vec d → ℝ) (ξ : Vec d → Vec d) {Bu Bg Bavg Bcirc1 C : ℝ} (hs : 0 < s) (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) (hpos : ∀ (N : ℕ), (cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : Vec d) => (u x - cubeAverage Q u) • ξ x) ≤ Bg) (hproj : ∀ (N : ℕ), CubeDescendantProjectedDualMeanZeroPoincareEstimate Q C (cubeFluctuation Q u) g N) (hneg1 : ∀ (N : ℕ), cubeBesovCircPartialNorm Q 1 2 1 N g ≤ Bcirc1) : |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) * 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_of_partialBounds {d : ℕ} (Q : TriadicCube d) (s : ℝ) (flux : Vec d → Vec d) (u g : Vec d → ℝ) (ξ : Vec d → Vec d) {Bu Bg Bavg Bcirc1 C : ℝ} (hs : 0 < s) (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) (hpos : ∀ (N : ℕ), (cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : Vec d) => (u x - cubeAverage Q u) • ξ x) ≤ Bg) (hproj : ∀ (N : ℕ), CubeDescendantProjectedDualMeanZeroPoincareEstimate Q C (cubeFluctuation Q u) g N) (hneg1 : ∀ (N : ℕ), cubeBesovCircPartialNorm Q 1 2 1 N g ≤ Bcirc1) : |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) * Bcirc1))) + ↑d * (3 ^ (↑d + s) * (cubeBesovScaleWeight (-s) Q * Bu) * (cubeBesovScaleWeight s Q * Bg))

theorem HCPolySupport.abs_cubeAverage_vectorDot_centered_scalar_smul_le_partialPoincareBounds {d : ℕ} (Q : TriadicCube d) (s : ℝ) (flux : Vec d → Vec d) (u : Vec d → ℝ) (G ξ : Vec d → Vec d) {Bu Bg Bavg Bcirc1 C : ℝ} (hs : 0 < s) (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) (havg : ‖cubeAverageVec Q flux‖ ≤ Bavg) (hneg : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q s N flux ≤ Bu) (hpos : ∀ (N : ℕ), (cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : Vec d) => (u x - cubeAverage Q u) • ξ x) ≤ Bg) (hproj : ∀ (N : ℕ), CubeDescendantProjectedDualMeanZeroVectorPoincareEstimate Q C (cubeFluctuation Q u) G N) (hGcirc1 : ∀ (i : Fin d) (N : ℕ), (cubeBesovCircPartialNorm Q 1 2 1 N fun (x : Vec d) => G x i) ≤ Bcirc1) : |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_sharpPartialPoincareBounds {d : ℕ} (Q : TriadicCube d) (s : ℝ) (flux : Vec d → Vec d) (u : Vec d → ℝ) (G ξ : Vec d → Vec d) {Bu Bg Bavg Bcirc1 C : ℝ} (hs : 0 < s) (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) (havg : ‖cubeAverageVec Q flux‖ ≤ Bavg) (hneg : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q s N flux ≤ Bu) (hpos : ∀ (N : ℕ), (cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : Vec d) => (u x - cubeAverage Q u) • ξ x) ≤ Bg) (hproj : ∀ (N : ℕ), CubeDescendantProjectedDualMeanZeroVectorPoincareEstimate Q C (cubeFluctuation Q u) G N) (hGcirc1 : ∀ (i : Fin d) (N : ℕ), (cubeBesovCircPartialNorm Q 1 2 1 N fun (x : Vec d) => G x i) ≤ Bcirc1) : |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 * Bg))

theorem HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo_centered_scalar_smul_le_poincare_cutoff_terms {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (u g : Vec d → ℝ) (ξ : Vec d → Vec d) {B C : ℝ} (hB : 0 ≤ B) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hproj : CubeDescendantProjectedDualMeanZeroPoincareEstimate Q C (cubeFluctuation Q u) g N) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (hξLp : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q)) (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) (hs : s < 1) (hC : 0 ≤ C) : (cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : Vec d) => (u x - cubeAverage Q u) • ξ x) ≤ 2 * (cubeScaleFactor Q * B * (√(1 - Real.rpow 3 (2 * (s - 1)))⁻¹ * (3 / 2 * C * 3 ^ (↑d + 1) * cubeBesovCircPartialNorm Q 1 2 1 N g)) + cubeLpNorm Q ⊤ ξ * cubeBesovPositiveScalarPartialSeminormTwo Q s N (cubeFluctuation Q u))

theorem HCPolySupport.cubeBesovPositiveVectorSeminormTwo_centered_scalar_smul_le_poincare_cutoff_terms {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u g : Vec d → ℝ) (ξ : Vec d → Vec d) {B C Bcirc Bpos : ℝ} (hB : 0 ≤ B) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hproj : ∀ (N : ℕ), CubeDescendantProjectedDualMeanZeroPoincareEstimate Q C (cubeFluctuation Q u) g N) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (hξLp : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q)) (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) (hs : s < 1) (hC : 0 ≤ C) (hneg : ∀ (N : ℕ), cubeBesovCircPartialNorm Q 1 2 1 N g ≤ Bcirc) (hpos : ∀ (N : ℕ), cubeBesovPositiveScalarPartialSeminormTwo Q s N (cubeFluctuation Q u) ≤ Bpos) : (cubeBesovPositiveVectorSeminormTwo Q s fun (x : Vec d) => (u x - cubeAverage Q u) • ξ x) ≤ 2 * (cubeScaleFactor Q * B * (√(1 - Real.rpow 3 (2 * (s - 1)))⁻¹ * (3 / 2 * C * 3 ^ (↑d + 1) * Bcirc)) + cubeLpNorm Q ⊤ ξ * Bpos)

theorem HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo_centered_scalar_smul_le_note_poincare_cutoff_terms {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (u g : Vec d → ℝ) (ξ : Vec d → Vec d) {B C : ℝ} (hB : 0 ≤ B) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hproj : CubeDescendantProjectedDualMeanZeroPoincareEstimate Q C (cubeFluctuation Q u) g N) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (hξLp : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q)) (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) (hs0 : 0 < s) (hs1 : s < 1) (hC : 0 ≤ C) : (cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : Vec d) => (u x - cubeAverage Q u) • ξ x) ≤ 2 * (cubeScaleFactor Q * B * (√(1 - Real.rpow 3 (2 * (s - 1)))⁻¹ * (3 / 2 * C * 3 ^ (↑d + 1) * cubeBesovCircPartialNorm Q 1 2 1 N g)) + cubeLpNorm Q ⊤ ξ * (cubeBesovScaleWeight (-s) Q * (3 / 2 * C * 3 ^ (↑d + 1) * (1 - 3 ^ (-s))⁻¹ * cubeBesovCircPartialNorm Q (1 - s) 2 1 N g)))

theorem HCPolySupport.cubeBesovPositiveVectorPartial_centered_smul_le_poincareCutoff {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (u : Vec d → ℝ) (G ξ : Vec d → Vec d) {B C Bcirc1 BcircS : ℝ} (hB : 0 ≤ B) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hproj : CubeDescendantProjectedDualMeanZeroVectorPoincareEstimate Q C (cubeFluctuation Q u) G N) (hG : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => G x i) 2 (normalizedCubeMeasure Q)) (hξLp : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q)) (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) (hs0 : 0 < s) (hs1 : s < 1) (hC : 0 ≤ C) (hBcircS : 0 ≤ BcircS) (hGcirc1 : ∀ (i : Fin d), (cubeBesovCircPartialNorm Q 1 2 1 N fun (x : Vec d) => G x i) ≤ Bcirc1) (hGcircS : ∀ (i : Fin d), (cubeBesovCircPartialNorm Q (1 - s) 2 1 N fun (x : Vec d) => G x i) ≤ BcircS) : (cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : Vec d) => (u x - cubeAverage Q u) • ξ x) ≤ 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))))

theorem HCPolySupport.cubeBesovPositiveVectorSeminormTwo_centered_scalar_smul_le_note_poincare_cutoff_terms {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u g : Vec d → ℝ) (ξ : Vec d → Vec d) {B C Bcirc1 BcircS : ℝ} (hB : 0 ≤ B) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hproj : ∀ (N : ℕ), CubeDescendantProjectedDualMeanZeroPoincareEstimate Q C (cubeFluctuation Q u) g N) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (hξLp : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q)) (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) (hs0 : 0 < s) (hs1 : s < 1) (hC : 0 ≤ C) (hneg1 : ∀ (N : ℕ), cubeBesovCircPartialNorm Q 1 2 1 N g ≤ Bcirc1) (hnegS : ∀ (N : ℕ), cubeBesovCircPartialNorm Q (1 - s) 2 1 N g ≤ BcircS) : (cubeBesovPositiveVectorSeminormTwo Q s fun (x : Vec d) => (u x - cubeAverage Q u) • ξ x) ≤ 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)))