Coarse-graining support: Support.Deterministic.ConstantCoefficientDirichletBesov.Basic

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

Discrete constant-coefficient Dirichlet Besov compatibility kernel

This file records the discrete compatibility kernel used by the legacy K-functional/overlap route. It is not the exact Lean contract for l.constant.coefficient.Dirichlet.Besov.function.spaces pending the continuum K/H^s gate.

theorem HCPolySupport.memVectorL2_openCubeSet_of_memLp_normalizedCubeMeasure {d : ℕ} (Q : TriadicCube d) {f : Vec d → Vec d} (hf : MeasureTheory.MemLp f 2 (normalizedCubeMeasure Q)) : MemVectorL2 (openCubeSet Q) f

Normalized cube L² data also gives vector L² data on the open cube. This is the measure-conversion needed when normalized Besov data is paired against Sobolev test gradients.

theorem HCPolySupport.cubeAverage_le_of_le_on_cubeSet {d : ℕ} {Q : TriadicCube d} {f g : Vec d → ℝ} (hf : MeasureTheory.IntegrableOn f (cubeSet Q) MeasureTheory.volume) (hg : MeasureTheory.IntegrableOn g (cubeSet Q) MeasureTheory.volume) (hle : ∀ x ∈ cubeSet Q, f x ≤ g x) : cubeAverage Q f ≤ cubeAverage Q g

Monotonicity of the normalized cube average, with integrability supplied on the underlying half-open cube.

theorem HCPolySupport.sq_cubeAverage_le_cubeAverage_sq_of_memLp {d : ℕ} (Q : TriadicCube d) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f 2 (normalizedCubeMeasure Q)) : cubeAverage Q f ^ 2 ≤ cubeAverage Q fun (x : Vec d) => f x ^ 2

Jensen/Cauchy bound for the normalized scalar cube average.

theorem HCPolySupport.vecNormSq_cubeAverageVec_le_sum_cubeAverage_sq_of_memLp {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) : vecNormSq (cubeAverageVec Q u) ≤ ∑ i : Fin d, cubeAverage Q fun (x : Vec d) => u x i ^ 2

Coordinatewise Jensen/Cauchy bound for vector-valued cube averages.

theorem HCPolySupport.norm_le_sqrt_vecNormSq {d : ℕ} (v : Vec d) : ‖v‖ ≤ √(vecNormSq v)

The ambient Pi norm of a project vector is bounded by its Euclidean square root.

theorem HCPolySupport.vecNormSq_le_card_mul_norm_sq {d : ℕ} (v : Vec d) : vecNormSq v ≤ ↑(Fintype.card (Fin d)) * ‖v‖ ^ 2

theorem HCPolySupport.enorm_rpow_two_le_ofReal_vecNormSq {d : ℕ} (v : Vec d) : ‖v‖ₑ ^ 2 ≤ ENNReal.ofReal (vecNormSq v)

theorem HCPolySupport.ofReal_vecNormSq_le_card_mul_enorm_rpow_two {d : ℕ} (v : Vec d) : ENNReal.ofReal (vecNormSq v) ≤ ↑(Fintype.card (Fin d)) * ‖v‖ₑ ^ 2

theorem HCPolySupport.H1Function.norm_gradToVectorL2_le_gradientCoordL2NormSum {d : ℕ} {U : Set (Vec d)} (v : H1Function U) : ‖v.gradToVectorL2‖ ≤ v.gradientCoordL2NormSum

theorem HCPolySupport.cubeLpNorm_two_sq_le_cubeAverage_vecNormSq {d : ℕ} {Q : TriadicCube d} {F : Vec d → Vec d} (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) : cubeLpNorm Q 2 F ^ 2 ≤ cubeAverage Q fun (x : Vec d) => vecNormSq (F x)

The square of the normalized vector L² norm is controlled by the normalized average of the Euclidean square. The dimension-free direction uses ‖v‖_∞ ≤ |v|_2 pointwise.

theorem HCPolySupport.abs_cubeAverage_vecDot_le_card_mul_cubeLpNorm_two_mul {d : ℕ} (Q : TriadicCube d) (F G : Vec d → Vec d) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) (hG : MeasureTheory.MemLp G 2 (normalizedCubeMeasure Q)) : |cubeAverage Q fun (x : Vec d) => vecDot (F x) (G x)| ≤ ↑(Fintype.card (Fin d)) * cubeLpNorm Q 2 F * cubeLpNorm Q 2 G

Vector Cauchy-Schwarz for normalized cube averages, stated in the ambient cubeLpNorm used by the K-functional layer.

theorem HCPolySupport.memScalarL2_of_contDiff_hasCompactSupport {d : ℕ} (U : Set (Vec d)) {ψ : Vec d → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψ_compact : HasCompactSupport ψ) : MemScalarL2 U ψ

theorem HCPolySupport.memScalarL2_euclideanCoordDeriv_of_contDiff_hasCompactSupport {d : ℕ} (U : Set (Vec d)) (i : Fin d) {ψ : Vec d → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψ_compact : HasCompactSupport ψ) : MemScalarL2 U (euclideanCoordDeriv i ψ)

theorem HCPolySupport.H1Function.integral_mul_zeroTrace_gradCoord_eq_neg_integral_gradCoord_mul {d : ℕ} {U : Set (Vec d)} (u : H1Function U) (φ : H10Function U) (i : Fin d) : ∫ (x : Vec d) in U, u.toFun x * φ.grad x i = -∫ (x : Vec d) in U, u.grad x i * φ.toFun x

Weak integration by parts between an H¹ function and a zero-trace H¹ test.