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

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

theorem HCPolySupport.SmoothOverlapPartition.exists_cubeVectorKFunctional_le_mul_sqrt_depthAverage {d : ℕ} {Q : TriadicCube d} {j : ℕ} (P : SmoothOverlapPartition Q j) (h : Vec d → Vec d) (hloc : ∀ S ∈ overlapCentersAtDepth Q j, MeasureTheory.MemLp h 2 (normalizedOverlapCubeMeasure S)) : ∃ (C : ℝ), 0 ≤ C ∧ cubeVectorKFunctional Q (Real.rpow 3 (-↑j)) h ≤ C * √(cubeBesovOverlappingPositiveVectorDepthAverage Q h j)

Phase-5 K-functional endpoint for the concrete overlap-averaging competitor coming from a supplied smooth overlap partition.

theorem HCPolySupport.SmoothOverlapPartition.exists_cubeKBesovVectorDepthSeminorm_le_mul_overlapDepthSeminorm {d : ℕ} {Q : TriadicCube d} {j : ℕ} (P : SmoothOverlapPartition Q j) (s : ℝ) (h : Vec d → Vec d) (hloc : ∀ S ∈ overlapCentersAtDepth Q j, MeasureTheory.MemLp h 2 (normalizedOverlapCubeMeasure S)) : ∃ (C : ℝ), 0 ≤ C ∧ cubeKBesovVectorDepthSeminorm Q s h j ≤ C * cubeBesovOverlappingPositiveVectorDepthSeminorm Q s h j

Phase-5 depth-seminorm estimate for the concrete overlap-averaging competitor coming from a supplied smooth overlap partition.

theorem HCPolySupport.SmoothOverlapPartition.exists_cubeKBesovVectorPartialSeminormTwo_le_mul_overlapPartialSeminorm {d : ℕ} {Q : TriadicCube d} {N : ℕ} (s : ℝ) (h : Vec d → Vec d) (hparent : MeasureTheory.MemLp h 2 (normalizedCubeMeasure Q)) (hpart : ∀ j ∈ Finset.range (N + 1), Nonempty (SmoothOverlapPartition Q j)) : ∃ (C : ℝ), 0 ≤ C ∧ cubeKBesovVectorPartialSeminormTwo Q s N h ≤ C * cubeBesovOverlappingPositiveVectorPartialSeminormTwo Q s N h

Concrete finite-depth Phase-6 assembly from supplied smooth overlap partitions at every depth in the partial sum. The constant may depend on the finite family of supplied partitions; the later public axiom removal still requires the uniform partition construction.