Coarse-graining support:

Support.Deterministic.ConstantCoefficientDirichletBesov.StandardProjectionBoundaryNeighbor

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

Boundary sums with local neighbor-energy budgets

This file refines the boundary-crossing reduction so that the enlarged boundary-layer sum is gated back to admissible overlap centers. That lets us insert the local-neighbor increment-energy estimate, whose hypotheses require overlapCubeSet S ⊆ cubeSet Q.

noncomputable def HCPolySupport.overlapIntersectingParentEnergy {d : ℕ} (Q S : TriadicCube d) (m : ℕ) (u : Vec d → Vec d) : ℝ

Child-energy budget of the depth-m parents whose cubes meet the overlap cube centered at S.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.overlapIntersectingParentEnergy_nonneg {d : ℕ} (Q S : TriadicCube d) (m : ℕ) (u : Vec d → Vec d) : 0 ≤ overlapIntersectingParentEnergy Q S m u

theorem HCPolySupport.cubeBesovOverlappingPositiveVectorDepthAverage_cubeIncrementVec_le_admissible_boundaryLayer_sum {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) {j m : ℕ} (hmj : m ≤ j) : cubeBesovOverlappingPositiveVectorDepthAverage Q (cubeIncrementVec Q (m + 1) u) j ≤ (↑(overlapCentersAtDepth Q j).card)⁻¹ * ∑ S ∈ incrementBoundaryLayerCentersAtDepth Q j m, if S ∈ overlapCentersAtDepth Q j then overlapCubeLpNorm S 2 (overlapCubeFluctuationVec S (cubeIncrementVec Q (m + 1) u)) ^ 2 else 0

Boundary-layer reduction with a gate back to admissible overlap centers. The gate is important because the raw ancestor boundary layer also contains fine descendants whose overlap cube may leave Q; crossing centers never do.

theorem HCPolySupport.cubeBesovOverlappingPositiveVectorDepthAverage_cubeIncrementVec_le_boundary_neighborEnergy_sum {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) {j m : ℕ} (hmj : m ≤ j) (hincLoc : ∀ S ∈ overlapCentersAtDepth Q j, MeasureTheory.MemLp (cubeIncrementVec Q (m + 1) u) 2 (normalizedOverlapCubeMeasure S)) (huChild : ∀ T ∈ descendantsAtDepth Q m, ∀ R ∈ childCubes T, MeasureTheory.MemLp u 2 (normalizedCubeMeasure R)) : cubeBesovOverlappingPositiveVectorDepthAverage Q (cubeIncrementVec Q (m + 1) u) j ≤ (↑(overlapCentersAtDepth Q j).card)⁻¹ * ∑ S ∈ incrementBoundaryLayerCentersAtDepth Q j m, if S ∈ overlapCentersAtDepth Q j then 4 * overlapIntersectingParentEnergy Q S m u else 0

Insert the local-neighbor increment-energy estimate into the admissible boundary-layer reduction. The remaining task after this theorem is purely geometric summation: control the admissible boundary-layer neighbor-energy sum by the ordinary standard positive depth budgets.

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

Admissible boundary-neighbor centers which charge a fixed depth-m parent.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.mem_boundaryNeighborCentersForParent_iff {d : ℕ} {Q S T : TriadicCube d} {j m : ℕ} : S ∈ boundaryNeighborCentersForParent Q j m T ↔ S ∈ incrementBoundaryLayerCentersAtDepth Q j m ∧ S ∈ overlapCentersAtDepth Q j ∧ T ∈ overlapIntersectingParentsAtDepth Q S m

theorem HCPolySupport.boundaryNeighborCentersForParent_subset_incrementBoundaryLayerCentersAtDepth {d : ℕ} (Q : TriadicCube d) (j m : ℕ) (T : TriadicCube d) : boundaryNeighborCentersForParent Q j m T ⊆ incrementBoundaryLayerCentersAtDepth Q j m

theorem HCPolySupport.boundaryNeighborCentersForParent_card_le_globalBoundaryLayer_card {d : ℕ} (Q : TriadicCube d) (j m : ℕ) (T : TriadicCube d) : (boundaryNeighborCentersForParent Q j m T).card ≤ (incrementBoundaryLayerCentersAtDepth Q j m).card

Safe global fallback for the parent-hit count. This is not the sharp surface-count estimate needed at the end, but it proves that every parent-hit family is a subfamily of the global increment boundary layer.

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

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

noncomputable def HCPolySupport.childBoundaryLayerCentersAtDepth {d : ℕ} (T : TriadicCube d) (n : ℕ) : Finset (TriadicCube d)

Boundary-layer centers generated by the children of one depth-m parent. This is the scale-sharp part of the hit count; the separate remaining geometry is to control centers generated by neighboring depth-m parents.

Equations

• HCPolySupport.childBoundaryLayerCentersAtDepth T n = (HCPolySupport.childCubes T).biUnion fun (R : HCPolySupport.TriadicCube d) => HCPolySupport.descendantBoundaryLayerAtDepth R n

theorem HCPolySupport.childBoundaryLayerCentersAtDepth_card_le {d : ℕ} (T : TriadicCube d) (n : ℕ) : (childBoundaryLayerCentersAtDepth T n).card ≤ 3 ^ d * (2 * d * (3 ^ (d - 1)) ^ n)

theorem HCPolySupport.childBoundaryLayerCentersAtDepth_card_cast_le {d : ℕ} (T : TriadicCube d) (n : ℕ) : ↑(childBoundaryLayerCentersAtDepth T n).card ≤ 3 ^ d * ↑(2 * d * (3 ^ (d - 1)) ^ n)

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

The own-child part of the parent hit family.

Equations

• HCPolySupport.ownChildBoundaryNeighborCentersForParent Q j m T = {S ∈ HCPolySupport.boundaryNeighborCentersForParent Q j m T | S ∈ HCPolySupport.childBoundaryLayerCentersAtDepth T (j - m)}

theorem HCPolySupport.ownChildBoundaryNeighborCentersForParent_subset_childBoundaryLayerCentersAtDepth {d : ℕ} (Q : TriadicCube d) (j m : ℕ) (T : TriadicCube d) : ownChildBoundaryNeighborCentersForParent Q j m T ⊆ childBoundaryLayerCentersAtDepth T (j - m)

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

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

Depth-m parents whose children generate at least one admissible boundary-neighbor center for the fixed charged parent T.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.mem_boundaryGeneratingParentsForParent_iff {d : ℕ} {Q P T : TriadicCube d} {j m : ℕ} : P ∈ boundaryGeneratingParentsForParent Q j m T ↔ P ∈ descendantsAtDepth Q m ∧ ∃ S ∈ boundaryNeighborCentersForParent Q j m T, S ∈ childBoundaryLayerCentersAtDepth P (j - m)

theorem HCPolySupport.boundaryNeighborCentersForParent_subset_generatingParents_childBoundary {d : ℕ} (Q : TriadicCube d) (j m : ℕ) (T : TriadicCube d) : boundaryNeighborCentersForParent Q j m T ⊆ (boundaryGeneratingParentsForParent Q j m T).biUnion fun (P : TriadicCube d) => childBoundaryLayerCentersAtDepth P (j - m)

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

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

theorem HCPolySupport.admissible_boundary_neighborEnergy_sum_le_count_mul_parentEnergy_sum {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (j m : ℕ) {M : ℝ} (hM : ∀ T ∈ descendantsAtDepth Q m, ↑(boundaryNeighborCentersForParent Q j m T).card ≤ M) : (∑ S ∈ incrementBoundaryLayerCentersAtDepth Q j m, if S ∈ overlapCentersAtDepth Q j then overlapIntersectingParentEnergy Q S m u else 0) ≤ M * ∑ T ∈ descendantsAtDepth Q m, ∑ R ∈ childCubes T, ∑ i : Fin d, cubeAverage R fun (y : Vec d) => (u y i - cubeAverageVec T u i) ^ 2

Pure finite-sum bookkeeping for the remaining geometry. If every depth-m parent is charged by at most M admissible boundary-neighbor centers, then the full boundary-neighbor energy sum is controlled by M times the ordinary depth-m parent child-energy sum.

theorem HCPolySupport.overlappingPositiveDepthAverage_increment_le_neighborParentEnergy {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) {j m : ℕ} (hmj : m ≤ j) {M : ℝ} (hM : ∀ T ∈ descendantsAtDepth Q m, ↑(boundaryNeighborCentersForParent Q j m T).card ≤ M) (hincLoc : ∀ S ∈ overlapCentersAtDepth Q j, MeasureTheory.MemLp (cubeIncrementVec Q (m + 1) u) 2 (normalizedOverlapCubeMeasure S)) (huChild : ∀ T ∈ descendantsAtDepth Q m, ∀ R ∈ childCubes T, MeasureTheory.MemLp u 2 (normalizedCubeMeasure R)) : cubeBesovOverlappingPositiveVectorDepthAverage Q (cubeIncrementVec Q (m + 1) u) j ≤ (↑(overlapCentersAtDepth Q j).card)⁻¹ * (4 * (M * ∑ T ∈ descendantsAtDepth Q m, ∑ R ∈ childCubes T, ∑ i : Fin d, cubeAverage R fun (y : Vec d) => (u y i - cubeAverageVec T u i) ^ 2))

One-increment boundary estimate after the local-neighbor budget and a supplied parent-hit counting bound. The remaining geometric theorem should provide the count M ≃ (3^(d-1))^(j-m).

theorem HCPolySupport.cubeBesovOverlappingPositiveVectorDepthAverage_cubeIncrementVec_le_neighbor_count_depthAverage {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) {j m : ℕ} (hmj : m ≤ j) {M : ℝ} (hM : ∀ T ∈ descendantsAtDepth Q m, ↑(boundaryNeighborCentersForParent Q j m T).card ≤ M) (hincLoc : ∀ S ∈ overlapCentersAtDepth Q j, MeasureTheory.MemLp (cubeIncrementVec Q (m + 1) u) 2 (normalizedOverlapCubeMeasure S)) (huParent : ∀ T ∈ descendantsAtDepth Q m, MeasureTheory.MemLp u 2 (normalizedCubeMeasure T)) : cubeBesovOverlappingPositiveVectorDepthAverage Q (cubeIncrementVec Q (m + 1) u) j ≤ (↑(overlapCentersAtDepth Q j).card)⁻¹ * (4 * (M * (3 ^ d * ↑(Fintype.card (Fin d)) * ↑(descendantsAtDepth Q m).card * cubeBesovPositiveVectorDepthAverage Q u m)))

One-increment boundary estimate after the parent-hit count, expressed in terms of the ordinary standard positive depth-m average.

theorem HCPolySupport.overlappingPositiveDepthMean_increment_le_inversePower_neighborCount_mean {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) {j m : ℕ} (hmj : m ≤ j) {M : ℝ} (hM : ∀ T ∈ descendantsAtDepth Q m, ↑(boundaryNeighborCentersForParent Q j m T).card ≤ M) (hincLoc : ∀ S ∈ overlapCentersAtDepth Q j, MeasureTheory.MemLp (cubeIncrementVec Q (m + 1) u) 2 (normalizedOverlapCubeMeasure S)) (huParent : ∀ T ∈ descendantsAtDepth Q m, MeasureTheory.MemLp u 2 (normalizedCubeMeasure T)) : cubeBesovOverlappingPositiveVectorDepthAverage Q (cubeIncrementVec Q (m + 1) u) j ≤ (↑((3 ^ d) ^ j))⁻¹ * (4 * (M * (3 ^ d * ↑(Fintype.card (Fin d)) * ↑(descendantsAtDepth Q m).card * cubeBesovPositiveVectorDepthAverage Q u m)))

Scale-separated normalization form of cubeBesovOverlappingPositiveVectorDepthAverage_cubeIncrementVec_le_neighbor_count_depthAverage.

theorem HCPolySupport.cubeBesovOverlappingPositiveVectorDepthSeminorm_gap_zero_le_sum_sqrt_neighbor_count_depthAverage {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (j : ℕ) (M : ℕ → ℝ) (hincLoc : ∀ S ∈ overlapCentersAtDepth Q j, ∀ m ∈ Finset.range j, MeasureTheory.MemLp (cubeIncrementVec Q (m + 1) u) 2 (normalizedOverlapCubeMeasure S)) (hM : ∀ m ∈ Finset.range j, ∀ T ∈ descendantsAtDepth Q m, ↑(boundaryNeighborCentersForParent Q j m T).card ≤ M m) (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 * (M m * (3 ^ d * ↑(Fintype.card (Fin d)) * ↑(descendantsAtDepth Q m).card * cubeBesovPositiveVectorDepthAverage Q u m))))

Projection-gap seminorm estimate assembled from the one-increment neighbor-count estimates. This is the downstream form of the remaining geometry: supply the hit count for every increment scale, and the projection jump is controlled by the corresponding weighted standard positive depths.

theorem HCPolySupport.overlappingPositiveDepthSeminorm_gap_zero_le_sum_sqrt_boundaryLayerMean {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) ^ (m + 1) * (2 * d * (3 ^ (d - 1)) ^ (j - m))) * (3 ^ d * ↑(Fintype.card (Fin d)) * ↑(descendantsAtDepth Q m).card * cubeBesovPositiveVectorDepthAverage Q u m))))

Baseline projection-gap estimate using the global boundary-layer count. This is scale-incorrect for the final theorem, but it is a fully proved fallback showing that the hit-count interface composes without any remaining analytic hypotheses.