Coarse-graining support: Support.Book.Ch01.Theorems.CutoffProduct

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

Cutoff/product estimate

This file retains the legacy disjoint-positive, totalized-real, componentwise-circ compatibility surface for the cutoff/product Besov estimate used later in the coarse Caccioppoli argument. It is not the exact manuscript overlap/Euclidean statement. It is stated for a general smooth vector cutoff field ξ; in the notes this is applied to ξ = ∇φ.

theorem HCPolySupport.Book.Ch01.Legacy.cutoffProductPositiveBesov_partial {d : ℕ} (Q : Cube d) (s : ℝ) (N : ℕ) (u : Vec d → ℝ) (ξ : Vec d → Vec d) {B : ℝ} (hB : 0 ≤ B) (hu : MeasureTheory.MemLp u 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) : (cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : HCPolySupport.Vec d) => (u x - normalizedAverage Q u) • ξ x) ≤ 2 * (cubeScaleFactor Q * B * cubeL2ScalarPartialSeminormTwo Q (s - 1) N (cubeFluctuation Q u) + normalizedLpNorm Q ⊤ ξ * cubeBesovPositiveScalarPartialSeminormTwo Q s N (cubeFluctuation Q u))

Legacy finite-depth cutoff/product compatibility estimate in the disjoint-positive, totalized-real, componentwise-circ Besov convention; not an exact manuscript overlap/Euclidean statement.

This is the pure product estimate. Poincare, full-dual, and circ-budget inputs belong to downstream corollaries, not to the Chapter 1 product surface.

theorem HCPolySupport.Book.Ch01.Legacy.cutoffProduct_component_partialNormTop_le_gradient_rhs {d : ℕ} (Q : Cube d) (s : ℝ) (M : ℕ) (u : H1Function (openCubeSet Q)) (ξ : Vec d → Vec d) {B : ℝ} (hB : 0 ≤ B) (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) (i : Fin d) : (cubeBesovPartialNormTop Q s 2 M fun (x : HCPolySupport.Vec d) => (cubeFluctuation Q (fun (y : HCPolySupport.Vec d) => u.toFun y) x • ξ x) i) ≤ (2 * cubeScaleFactor Q * B + 3 * cubeLpNorm Q ⊤ ξ) * (fullVectorPoincareConstant Q * 3 ^ (↑d + 1) * ∑ i : Fin d, circNegativeBesovNorm Q (1 - s) 2 1 fun (x : Vec d) => u.grad x i)

theorem HCPolySupport.Book.Ch01.Legacy.cutoffProductPositiveBesov_infinite_from_h1 {d : ℕ} (Q : Cube d) (s : ℝ) (u : H1Function (openCubeSet Q)) (ξ : Vec d → Vec d) {B : ℝ} (hB : 0 ≤ B) (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) : (positiveBesovVectorNormTop Q s 2 fun (x : Vec d) => (u.toFun x - normalizedAverage Q fun (y : Vec d) => u.toFun y) • ξ x) ≤ ↑d * (2 * cubeScaleFactor Q * B + 3 * normalizedLpNorm Q ⊤ ξ) * (fullVectorPoincareConstant Q * 3 ^ (↑d + 1) * ∑ i : Fin d, circNegativeBesovNorm Q (1 - s) 2 1 fun (x : Vec d) => u.grad x i)

Legacy infinite-depth cutoff/product compatibility estimate with the disjoint-positive, totalized-real, componentwise-circ H1-facing right-hand side; not an exact manuscript overlap/Euclidean statement.

The vector Besov norm is the componentwise public convention positiveBesovVectorNormTop. The estimate has no finite-depth parameter and no local-multiscale or projected-Poincare contract hypotheses; all function-side control is supplied by the already-proved H¹ gradient-to-function corridor.