Coarse-graining support:

Support.Deterministic.ConstantCoefficientDirichletBesov.StandardProjectionBoundaryNeighborCount

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

Sharp boundary-neighbor hit counts

This file closes the geometric counting interface left by StandardProjectionBoundaryNeighbor. For a fixed depth-m parent T, any depth-m parent whose boundary children can charge T must lie in the one-step lattice neighborhood of T. That neighborhood has dimension-only cardinality, by triadic color injectivity.

noncomputable def HCPolySupport.oneStepNeighborParentsAtDepth {d : ℕ} (Q : TriadicCube d) (m : ℕ) (T : TriadicCube d) : Finset (TriadicCube d)

Depth-m descendants of Q whose indices differ from those of T by at most one in each coordinate.

Equations

• HCPolySupport.oneStepNeighborParentsAtDepth Q m T = {P ∈ HCPolySupport.descendantsAtDepth Q m | ∀ (i : Fin d), T.index i - 1 ≤ P.index i ∧ P.index i ≤ T.index i + 1}

theorem HCPolySupport.mem_oneStepNeighborParentsAtDepth_iff {d : ℕ} {Q P T : TriadicCube d} {m : ℕ} : P ∈ oneStepNeighborParentsAtDepth Q m T ↔ P ∈ descendantsAtDepth Q m ∧ ∀ (i : Fin d), T.index i - 1 ≤ P.index i ∧ P.index i ≤ T.index i + 1

theorem HCPolySupport.cubeColor_injOn_oneStepNeighborParentsAtDepth {d : ℕ} (Q : TriadicCube d) (m : ℕ) (T : TriadicCube d) : Set.InjOn cubeColor ↑(oneStepNeighborParentsAtDepth Q m T)

theorem HCPolySupport.oneStepNeighborParentsAtDepth_card_le_pow {d : ℕ} (Q : TriadicCube d) (m : ℕ) (T : TriadicCube d) : (oneStepNeighborParentsAtDepth Q m T).card ≤ 3 ^ d

theorem HCPolySupport.cubeScaleFactor_le_of_mem_descendantsAtDepth {d : ℕ} {Q R : TriadicCube d} {n : ℕ} (hR : R ∈ descendantsAtDepth Q n) : cubeScaleFactor R ≤ cubeScaleFactor Q

theorem HCPolySupport.cubeIndex_oneStep_of_overlap_inter_cube_of_descendant {d : ℕ} {P S T : TriadicCube d} {n : ℕ} (hSP : S ∈ descendantsAtDepth P n) (hscale : T.scale = P.scale) (hinter : (overlapCubeSet S ∩ cubeSet T).Nonempty) (i : Fin d) : T.index i - 1 ≤ P.index i ∧ P.index i ≤ T.index i + 1

theorem HCPolySupport.mem_descendantsAtDepth_succ_of_mem_childBoundaryLayerCentersAtDepth {d : ℕ} {P S : TriadicCube d} {n : ℕ} (hS : S ∈ childBoundaryLayerCentersAtDepth P n) : S ∈ descendantsAtDepth P (1 + n)

theorem HCPolySupport.boundaryGeneratingParentsForParent_subset_oneStepNeighborParentsAtDepth {d : ℕ} (Q : TriadicCube d) {j m : ℕ} (T : TriadicCube d) : boundaryGeneratingParentsForParent Q j m T ⊆ oneStepNeighborParentsAtDepth Q m T

theorem HCPolySupport.boundaryGeneratingParentsForParent_card_le_pow {d : ℕ} (Q : TriadicCube d) (j m : ℕ) (T : TriadicCube d) : (boundaryGeneratingParentsForParent Q j m T).card ≤ 3 ^ d

theorem HCPolySupport.boundaryNeighborCentersForParent_card_le_sharp {d : ℕ} (Q : TriadicCube d) (j m : ℕ) (T : TriadicCube d) : (boundaryNeighborCentersForParent Q j m T).card ≤ 3 ^ d * (3 ^ d * (2 * d * (3 ^ (d - 1)) ^ (j - m)))

theorem HCPolySupport.boundaryNeighborCentersForParent_card_cast_le_sharp {d : ℕ} (Q : TriadicCube d) (j m : ℕ) (T : TriadicCube d) : ↑(boundaryNeighborCentersForParent Q j m T).card ≤ ↑(3 ^ d * (3 ^ d * (2 * d * (3 ^ (d - 1)) ^ (j - m))))

theorem HCPolySupport.overlappingPositiveDepthSeminorm_gapZero_le_sharpBoundaryAverage {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (j : ℕ) (hincLoc : ∀ S ∈ overlapCentersAtDepth Q j, ∀ m ∈ Finset.range j, MeasureTheory.MemLp (cubeIncrementVec Q (m + 1) u) 2 (normalizedOverlapCubeMeasure S)) (huParent : ∀ m ∈ Finset.range j, ∀ T ∈ descendantsAtDepth Q m, MeasureTheory.MemLp u 2 (normalizedCubeMeasure T)) : cubeBesovOverlappingPositiveVectorDepthSeminorm Q s (cubeProjectionGapVec Q 0 j u) j ≤ ∑ m ∈ Finset.range j, Real.rpow 3 (s * ↑j) * √((↑((3 ^ d) ^ j))⁻¹ * (4 * (↑(3 ^ d * (3 ^ d * (2 * d * (3 ^ (d - 1)) ^ (j - m)))) * (3 ^ d * ↑(Fintype.card (Fin d)) * ↑(descendantsAtDepth Q m).card * cubeBesovPositiveVectorDepthAverage Q u m))))

Projection-gap estimate with the sharp per-parent boundary-neighbor count. This is the closed geometric version of the hit-count interface from StandardProjectionBoundaryNeighbor: the only remaining inputs are the local L² hypotheses needed to form the overlap norms and the ordinary standard parent L² hypotheses.

theorem HCPolySupport.sq_cubeBesovOverlappingPositiveVectorDepthSeminorm_le_standard_add_sharpBoundary_sum {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (j : ℕ) (hres : MeasureTheory.MemLp (fun (x : Vec d) => u x - cubeProjectionVec Q j u x) 2 (normalizedCubeMeasure Q)) (hresLoc : ∀ S ∈ overlapCentersAtDepth Q j, MeasureTheory.MemLp (fun (x : Vec d) => u x - cubeProjectionVec Q j u x) 2 (normalizedOverlapCubeMeasure S)) (hprojLoc : ∀ S ∈ overlapCentersAtDepth Q j, MeasureTheory.MemLp (cubeProjectionVec Q j u) 2 (normalizedOverlapCubeMeasure S)) (hzeroLoc : ∀ S ∈ overlapCentersAtDepth Q j, MeasureTheory.MemLp (cubeProjectionVec Q 0 u) 2 (normalizedOverlapCubeMeasure S)) (hgapLoc : ∀ S ∈ overlapCentersAtDepth Q j, MeasureTheory.MemLp (cubeProjectionGapVec Q 0 j u) 2 (normalizedOverlapCubeMeasure S)) (hincLoc : ∀ S ∈ overlapCentersAtDepth Q j, ∀ m ∈ Finset.range j, MeasureTheory.MemLp (cubeIncrementVec Q (m + 1) u) 2 (normalizedOverlapCubeMeasure S)) (huParent : ∀ m ∈ Finset.range j, ∀ T ∈ descendantsAtDepth Q m, MeasureTheory.MemLp u 2 (normalizedCubeMeasure T)) : have G := ∑ m ∈ Finset.range j, Real.rpow 3 (s * ↑j) * √((↑((3 ^ d) ^ j))⁻¹ * (4 * (↑(3 ^ d * (3 ^ d * (2 * d * (3 ^ (d - 1)) ^ (j - m)))) * (3 ^ d * ↑(Fintype.card (Fin d)) * ↑(descendantsAtDepth Q m).card * cubeBesovPositiveVectorDepthAverage Q u m)))); cubeBesovOverlappingPositiveVectorDepthSeminorm Q s u j ^ 2 ≤ 8 * 3 ^ d * cubeBesovPositiveVectorDepthSeminorm Q s u j ^ 2 + 4 * G ^ 2

One-depth hard comparison with the sharp projection-gap branch inserted. The residual half is paid by the same-depth ordinary standard positive term; the projection half is paid by the sharp boundary-neighbor sum over coarser ordinary positive depths.