Coarse-graining support: Support.Book.Ch03.Theorems.CoarseCaccioppoliRHS.ZeroTraceValue

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

Zero-Trace Value Estimates for Coarse Caccioppoli with RHS

This file is split mechanically out of CoarseCaccioppoliRHS.lean.

Audit tag

Claim: relate normalized open-cube L² squares for the zero-trace corrector to cube norms and the public forced Caccioppoli value terms.

Downstream target: CoarseCaccioppoliRHS/PublicRHSScalar.lean. This file should remain value/norm comparison infrastructure.

theorem HCPolySupport.Book.Ch03.normalizedL2SqOnSet_nonneg {d : ℕ} (V : Set (Vec d)) (u : Vec d → ℝ) : MeasurableSet V → 0 ≤ normalizedL2SqOnSet V u

Normalized L² squares are nonnegative.

theorem HCPolySupport.Book.Ch03.normalizedL2SqOnSet_openCubeSet_eq_cubeLpNorm_two_sq {d : ℕ} (Q : TriadicCube d) (u : Vec d → ℝ) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) : normalizedL2SqOnSet (openCubeSet Q) u = cubeLpNorm Q 2 u ^ 2

On a parent open cube, the normalized L² square is the square of the normalized cube L² norm.

theorem HCPolySupport.Book.Ch03.cubeBesovDepthSeminorm_two_depth_zero_fluctuation_eq {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → ℝ) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) : cubeBesovDepthSeminorm Q s 2 (cubeFluctuation Q u) 0 = cubeBesovScaleWeight s Q * cubeLpNorm Q 2 (cubeFluctuation Q u)

Depth zero of the scalar positive Besov seminorm of a fluctuation is the top-scale normalized L² norm.

theorem HCPolySupport.Book.Ch03.cubeBesovScaleWeight_mul_cubeLpNorm_fluctuation_le_partialNormTop {d : ℕ} (Q : TriadicCube d) (s : ℝ) (M : ℕ) (u : Vec d → ℝ) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) : cubeBesovScaleWeight s Q * cubeLpNorm Q 2 (cubeFluctuation Q u) ≤ cubeBesovPartialNormTop Q s 2 M (cubeFluctuation Q u)

Any positive-Besov finite top norm contains the depth-zero fluctuation L² contribution.

theorem HCPolySupport.Book.Ch03.cubeBesovScaleWeight_one_mul_cubeLpNorm_fluctuation_le_grad_negativeBesovTwo {d : ℕ} (Q : TriadicCube d) {t : ℝ} (u : H1Function (openCubeSet Q)) (ht : 0 < t) (ht_lt : t < 1 / 2) : cubeBesovScaleWeight 1 Q * cubeLpNorm Q 2 (cubeFluctuation Q fun (x : Vec d) => u.toFun x) ≤ Ch01.Legacy.fullVectorPoincareConstant Q * 3 ^ (↑d + 1) * (↑d * √(1 - Real.rpow 3 (-2 * (1 / 2 - t)))⁻¹) * cubeBesovNegativeVectorSeminormTwo Q (2 * t) fun (x : Vec d) => u.grad x

The fluctuation half of the zero-trace value bridge: the top-scale fluctuation L² norm is controlled by the public q = 2 negative-Besov norm of the gradient, with the geometric exponent-gap loss left explicit.

theorem HCPolySupport.Book.Ch03.cubeBesovScaleWeight_one_mul_abs_cubeAverage_h10_le_grad_negativeBesovTwo {d : ℕ} [NeZero d] (Q : TriadicCube d) {t : ℝ} (u : H10Function (cubeSet Q)) (ht : 0 < t) (ht_lt : t < 1 / 2) : cubeBesovScaleWeight 1 Q * ‖cubeAverage Q fun (x : Vec d) => u.toFun x‖ ≤ 2 * 3 ^ (↑d + 1) * √(1 - Real.rpow 3 (-2 * (1 - 2 * t)))⁻¹ * cubeBesovNegativeVectorSeminormTwo Q (2 * t) fun (x : Vec d) => u.grad x

The scalar average of a zero-trace function is controlled by the public negative-Besov norm of its gradient. The proof uses the zero-trace identity ∫ u = -∫ ∂ᵢu (xᵢ - centerᵢ) and tests the gradient component against the centered coordinate.

theorem HCPolySupport.Book.Ch03.sqrt_inv_one_sub_rpow_three_neg_two_mul_le_sqrt_inv_one_sub_rpow_three_neg {r : ℝ} (hr : 0 < r) : √(1 - Real.rpow 3 (-2 * r))⁻¹ ≤ √(1 - Real.rpow 3 (-r))⁻¹

The geometric loss with exponent 2r is no larger than the corresponding loss with exponent r.

theorem HCPolySupport.Book.Ch03.cubeLpNorm_two_le_cubeLpNorm_fluctuation_add_norm_cubeAverage {d : ℕ} (Q : TriadicCube d) (v : Vec d → ℝ) (hv : MeasureTheory.MemLp v 2 (normalizedCubeMeasure Q)) : cubeLpNorm Q 2 v ≤ cubeLpNorm Q 2 (cubeFluctuation Q v) + ‖cubeAverage Q v‖

The normalized L² norm is bounded by the fluctuation part plus the absolute scalar average.

theorem HCPolySupport.Book.Ch03.cubeBesovScaleWeight_one_mul_cubeLpNorm_h10_le_grad_negativeBesovTwo {d : ℕ} [NeZero d] (Q : TriadicCube d) {t : ℝ} (u : H10Function (cubeSet Q)) (ht : 0 < t) (ht_lt : t < 1 / 2) : (cubeBesovScaleWeight 1 Q * cubeLpNorm Q 2 fun (x : Vec d) => u.toFun x) ≤ (↑d * Legacy.cubeNeumannW22CalderonZygmundConstant d * 3 ^ (↑d + 1) * ↑d + 2 * 3 ^ (↑d + 1)) * √(1 - Real.rpow 3 (-2 * (1 / 2 - t)))⁻¹ * cubeBesovNegativeVectorSeminormTwo Q (2 * t) fun (x : Vec d) => u.grad x

Full parent-cube zero-trace value estimate: the top-scale normalized L² norm is controlled by the public negative-Besov norm of the gradient.