Coarse-graining support:

Support.Deterministic.ConstantCoefficientDirichletBesov.StandardProjectionBoundary

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

Boundary-crossing centers for projection increments

For one martingale increment, an overlap cube contributes only if it crosses the standard triadic partition at the increment scale. This file isolates that support reduction. The remaining geometric work is then a finite counting estimate for the crossing centers.

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

Overlap centers whose overlap cube is not contained in any standard descendant at the increment scale m + 1.

Equations

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

theorem HCPolySupport.mem_overlapCrossingCentersAtDepth_iff {d : ℕ} {Q S : TriadicCube d} {j m : ℕ} : S ∈ overlapCrossingCentersAtDepth Q j m ↔ S ∈ overlapCentersAtDepth Q j ∧ ∀ R ∈ descendantsAtDepth Q (m + 1), ¬overlapCubeSet S ⊆ cubeSet R

theorem HCPolySupport.mem_overlapCentersAtDepth_of_mem_overlapCrossingCentersAtDepth {d : ℕ} {Q S : TriadicCube d} {j m : ℕ} (hS : S ∈ overlapCrossingCentersAtDepth Q j m) : S ∈ overlapCentersAtDepth Q j

theorem HCPolySupport.overlapCrossingCentersAtDepth_subset_overlapCentersAtDepth {d : ℕ} (Q : TriadicCube d) (j m : ℕ) : overlapCrossingCentersAtDepth Q j m ⊆ overlapCentersAtDepth Q j

theorem HCPolySupport.overlapCubeLpNorm_overlapCubeFluctuationVec_cubeIncrementVec_eq_zero_of_not_mem_crossing {d : ℕ} {Q S : TriadicCube d} {j m : ℕ} (u : Vec d → Vec d) (hS : S ∈ overlapCentersAtDepth Q j) (hSnot : S ∉ overlapCrossingCentersAtDepth Q j m) : overlapCubeLpNorm S 2 (overlapCubeFluctuationVec S (cubeIncrementVec Q (m + 1) u)) = 0

If an admissible overlap center is not crossing at the increment scale, then the increment has zero corrected overlap fluctuation on that center.

theorem HCPolySupport.overlapCentersAtDepth_sum_cubeIncrementVec_eq_crossing_sum {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (j m : ℕ) : ∑ S ∈ overlapCentersAtDepth Q j, overlapCubeLpNorm S 2 (overlapCubeFluctuationVec S (cubeIncrementVec Q (m + 1) u)) ^ 2 = ∑ S ∈ overlapCrossingCentersAtDepth Q j m, overlapCubeLpNorm S 2 (overlapCubeFluctuationVec S (cubeIncrementVec Q (m + 1) u)) ^ 2

The overlap-center sum for one increment may be restricted to the crossing centers. Non-crossing centers contribute zero by local constancy.

theorem HCPolySupport.cubeBesovOverlappingPositiveVectorDepthAverage_cubeIncrementVec_eq_crossing_sum {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (j m : ℕ) : cubeBesovOverlappingPositiveVectorDepthAverage Q (cubeIncrementVec Q (m + 1) u) j = (↑(overlapCentersAtDepth Q j).card)⁻¹ * ∑ S ∈ overlapCrossingCentersAtDepth Q j m, overlapCubeLpNorm S 2 (overlapCubeFluctuationVec S (cubeIncrementVec Q (m + 1) u)) ^ 2

Depth-average form of overlapCentersAtDepth_sum_cubeIncrementVec_eq_crossing_sum.

theorem HCPolySupport.overlapCoordLower_eq_cubeCoordLower_sub_cubeScaleFactor {d : ℕ} (S : TriadicCube d) (i : Fin d) : overlapCoordLower S i = cubeCoordLower S i - cubeScaleFactor S

theorem HCPolySupport.overlapCoordUpper_eq_cubeCoordUpper_add_cubeScaleFactor {d : ℕ} (S : TriadicCube d) (i : Fin d) : overlapCoordUpper S i = cubeCoordUpper S i + cubeScaleFactor S

theorem HCPolySupport.overlapCubeSet_subset_cubeSet_of_coord_one_scale_separated {d : ℕ} {R S : TriadicCube d} (hlo : ∀ (i : Fin d), cubeCoordLower R i + cubeScaleFactor S ≤ cubeCoordLower S i) (hhi : ∀ (i : Fin d), cubeCoordUpper S i + cubeScaleFactor S ≤ cubeCoordUpper R i) : overlapCubeSet S ⊆ cubeSet R

If a fine descendant is one fine scale away from every face of a coarser cube, then its overlap cube is contained in that coarser cube.

theorem HCPolySupport.not_mem_overlapCrossingCentersAtDepth_of_coord_one_scale_separated {d : ℕ} {Q R S : TriadicCube d} {j m : ℕ} (hR : R ∈ descendantsAtDepth Q (m + 1)) (hlo : ∀ (i : Fin d), cubeCoordLower R i + cubeScaleFactor S ≤ cubeCoordLower S i) (hhi : ∀ (i : Fin d), cubeCoordUpper S i + cubeScaleFactor S ≤ cubeCoordUpper R i) : S ∉ overlapCrossingCentersAtDepth Q j m

A one-scale-separated descendant cannot be a crossing center for the coarser increment partition.

theorem HCPolySupport.not_forall_coord_one_scale_separated_of_mem_overlapCrossingCentersAtDepth {d : ℕ} {Q R S : TriadicCube d} {j m n : ℕ} (hS : S ∈ overlapCrossingCentersAtDepth Q j m) (hR : R ∈ descendantsAtDepth Q (m + 1)) (_hSR : S ∈ descendantsAtDepth R n) : ¬∀ (i : Fin d), cubeCoordLower R i + cubeScaleFactor S ≤ cubeCoordLower S i ∧ cubeCoordUpper S i + cubeScaleFactor S ≤ cubeCoordUpper R i

Crossing descendants fail the one-fine-scale interior separation from any coarser descendant that contains their center cube. This is the boundary-layer form needed for the cardinality estimate.

theorem HCPolySupport.exists_increment_ancestor_of_mem_overlapCentersAtDepth {d : ℕ} {Q S : TriadicCube d} {j m : ℕ} (hS : S ∈ overlapCentersAtDepth Q j) (hmj : m ≤ j) : ∃ R ∈ descendantsAtDepth Q (m + 1), S ∈ descendantsAtDepth R (j - m)

An overlap center at depth j has an ancestor at any increment depth m + 1 ≤ j + 1.

theorem HCPolySupport.exists_increment_ancestor_boundary_layer_of_mem_overlapCrossingCentersAtDepth {d : ℕ} {Q S : TriadicCube d} {j m : ℕ} (hS : S ∈ overlapCrossingCentersAtDepth Q j m) (hmj : m ≤ j) : ∃ R ∈ descendantsAtDepth Q (m + 1), S ∈ descendantsAtDepth R (j - m) ∧ ¬∀ (i : Fin d), cubeCoordLower R i + cubeScaleFactor S ≤ cubeCoordLower S i ∧ cubeCoordUpper S i + cubeScaleFactor S ≤ cubeCoordUpper R i

A crossing overlap center has a coarser increment ancestor, and relative to that ancestor it lies in the one-fine-scale boundary layer.

noncomputable def HCPolySupport.descendantBoundaryLayerAtDepth {d : ℕ} (R : TriadicCube d) (n : ℕ) : Finset (TriadicCube d)

Descendants of R at depth n lying in the one-fine-scale boundary layer of R.

Equations

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

theorem HCPolySupport.mem_descendantBoundaryLayerAtDepth_iff {d : ℕ} {R S : TriadicCube d} {n : ℕ} : S ∈ descendantBoundaryLayerAtDepth R n ↔ S ∈ descendantsAtDepth R n ∧ ¬∀ (i : Fin d), cubeCoordLower R i + cubeScaleFactor S ≤ cubeCoordLower S i ∧ cubeCoordUpper S i + cubeScaleFactor S ≤ cubeCoordUpper R i

theorem HCPolySupport.mem_descendantBoundaryLayerAtDepth_iff_exists_coord_face {d : ℕ} {R S : TriadicCube d} {n : ℕ} : S ∈ descendantBoundaryLayerAtDepth R n ↔ S ∈ descendantsAtDepth R n ∧ ∃ (i : Fin d), cubeCoordLower S i = cubeCoordLower R i ∨ cubeCoordUpper S i = cubeCoordUpper R i

The boundary layer is exactly the union of the descendants sharing at least one lower or upper coordinate face with the parent cube.

noncomputable def HCPolySupport.fixedCoordinateFunctionEquiv {α : Type u_1} {β : Type u_2} [DecidableEq α] (i : α) (a : β) : { f : α → β // f i = a } ≃ ({ j : α // j ≠ i } → β)

Remove a fixed coordinate from a function, with inverse given by restoring its prescribed value; used to count face digits.

Equations

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

theorem HCPolySupport.cubeCoordLower_child_eq_parent_iff_digit_zero {d : ℕ} (R : TriadicCube d) (digits : Fin d → Fin 3) (i : Fin d) : cubeCoordLower { scale := R.scale - 1, index := fun (k : Fin d) => 3 * R.index k + ↑↑(digits k) - 1 } i = cubeCoordLower R i ↔ digits i = 0

theorem HCPolySupport.cubeCoordUpper_child_eq_parent_iff_digit_two {d : ℕ} (R : TriadicCube d) (digits : Fin d → Fin 3) (i : Fin d) : cubeCoordUpper { scale := R.scale - 1, index := fun (k : Fin d) => 3 * R.index k + ↑↑(digits k) - 1 } i = cubeCoordUpper R i ↔ digits i = 2

theorem HCPolySupport.childCubes_lowerFace_card {d : ℕ} (R : TriadicCube d) (i : Fin d) : {S ∈ childCubes R | cubeCoordLower S i = cubeCoordLower R i}.card = 3 ^ (d - 1)

theorem HCPolySupport.childCubes_upperFace_card {d : ℕ} (R : TriadicCube d) (i : Fin d) : {S ∈ childCubes R | cubeCoordUpper S i = cubeCoordUpper R i}.card = 3 ^ (d - 1)

noncomputable def HCPolySupport.descendantLowerFaceAtDepth {d : ℕ} (R : TriadicCube d) (n : ℕ) (i : Fin d) : Finset (TriadicCube d)

Depth-n descendants whose lower ith face coincides with the lower face of R.

Equations

• HCPolySupport.descendantLowerFaceAtDepth R n i = {S ∈ HCPolySupport.descendantsAtDepth R n | HCPolySupport.cubeCoordLower S i = HCPolySupport.cubeCoordLower R i}

theorem HCPolySupport.mem_descendantLowerFaceAtDepth_iff {d : ℕ} {R S : TriadicCube d} {n : ℕ} {i : Fin d} : S ∈ descendantLowerFaceAtDepth R n i ↔ S ∈ descendantsAtDepth R n ∧ cubeCoordLower S i = cubeCoordLower R i

noncomputable def HCPolySupport.descendantUpperFaceAtDepth {d : ℕ} (R : TriadicCube d) (n : ℕ) (i : Fin d) : Finset (TriadicCube d)

Depth-n descendants whose upper ith face coincides with the upper face of R.

Equations

• HCPolySupport.descendantUpperFaceAtDepth R n i = {S ∈ HCPolySupport.descendantsAtDepth R n | HCPolySupport.cubeCoordUpper S i = HCPolySupport.cubeCoordUpper R i}

theorem HCPolySupport.mem_descendantUpperFaceAtDepth_iff {d : ℕ} {R S : TriadicCube d} {n : ℕ} {i : Fin d} : S ∈ descendantUpperFaceAtDepth R n i ↔ S ∈ descendantsAtDepth R n ∧ cubeCoordUpper S i = cubeCoordUpper R i

noncomputable def HCPolySupport.descendantFaceBoundaryAtDepth {d : ℕ} (R : TriadicCube d) (n : ℕ) : Finset (TriadicCube d)

The coordinate-face union containing the boundary layer.

Equations

• HCPolySupport.descendantFaceBoundaryAtDepth R n = Finset.univ.biUnion fun (i : Fin d) => HCPolySupport.descendantLowerFaceAtDepth R n i ∪ HCPolySupport.descendantUpperFaceAtDepth R n i

theorem HCPolySupport.descendantBoundaryLayerAtDepth_subset_faceBoundaryAtDepth {d : ℕ} (R : TriadicCube d) (n : ℕ) : descendantBoundaryLayerAtDepth R n ⊆ descendantFaceBoundaryAtDepth R n

theorem HCPolySupport.descendantLowerFaceAtDepth_succ_subset_biUnion {d : ℕ} (R : TriadicCube d) (n : ℕ) (i : Fin d) : descendantLowerFaceAtDepth R (n + 1) i ⊆ (descendantLowerFaceAtDepth R n i).biUnion fun (P : TriadicCube d) => descendantLowerFaceAtDepth P 1 i

theorem HCPolySupport.descendantUpperFaceAtDepth_succ_subset_biUnion {d : ℕ} (R : TriadicCube d) (n : ℕ) (i : Fin d) : descendantUpperFaceAtDepth R (n + 1) i ⊆ (descendantUpperFaceAtDepth R n i).biUnion fun (P : TriadicCube d) => descendantUpperFaceAtDepth P 1 i

theorem HCPolySupport.descendantLowerFaceAtDepth_card_le {d : ℕ} (R : TriadicCube d) (n : ℕ) (i : Fin d) : (descendantLowerFaceAtDepth R n i).card ≤ (3 ^ (d - 1)) ^ n

theorem HCPolySupport.descendantUpperFaceAtDepth_card_le {d : ℕ} (R : TriadicCube d) (n : ℕ) (i : Fin d) : (descendantUpperFaceAtDepth R n i).card ≤ (3 ^ (d - 1)) ^ n

theorem HCPolySupport.descendantBoundaryLayerAtDepth_card_le {d : ℕ} (R : TriadicCube d) (n : ℕ) : (descendantBoundaryLayerAtDepth R n).card ≤ 2 * d * (3 ^ (d - 1)) ^ n

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

Boundary-layer descendants over all increment-scale ancestors.

Equations

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

theorem HCPolySupport.incrementBoundaryLayerCentersAtDepth_card_le {d : ℕ} (Q : TriadicCube d) (j m : ℕ) : (incrementBoundaryLayerCentersAtDepth Q j m).card ≤ (descendantsAtDepth Q (m + 1)).card * (2 * d * (3 ^ (d - 1)) ^ (j - m))

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

theorem HCPolySupport.incrementBoundaryLayerCentersAtDepth_sum_le_ancestor_boundaryLayer_sum {d : ℕ} (Q : TriadicCube d) (j m : ℕ) (F : TriadicCube d → ℝ) (hF : ∀ S ∈ incrementBoundaryLayerCentersAtDepth Q j m, 0 ≤ F S) : (incrementBoundaryLayerCentersAtDepth Q j m).sum F ≤ ∑ R ∈ descendantsAtDepth Q (m + 1), (descendantBoundaryLayerAtDepth R (j - m)).sum F

theorem HCPolySupport.incrementBoundaryLayerCentersAtDepth_sum_le_ancestor_weighted_sum {d : ℕ} (Q : TriadicCube d) (j m : ℕ) (F B : TriadicCube d → ℝ) (hF : ∀ S ∈ incrementBoundaryLayerCentersAtDepth Q j m, 0 ≤ F S) (hbound : ∀ R ∈ descendantsAtDepth Q (m + 1), ∀ S ∈ descendantBoundaryLayerAtDepth R (j - m), F S ≤ B R) : (incrementBoundaryLayerCentersAtDepth Q j m).sum F ≤ ∑ R ∈ descendantsAtDepth Q (m + 1), ↑(descendantBoundaryLayerAtDepth R (j - m)).card * B R

theorem HCPolySupport.incrementBoundaryLayerCentersAtDepth_sum_le_const_mul_ancestor_sum {d : ℕ} (Q : TriadicCube d) (j m : ℕ) (F B : TriadicCube d → ℝ) (hF : ∀ S ∈ incrementBoundaryLayerCentersAtDepth Q j m, 0 ≤ F S) (hB : ∀ R ∈ descendantsAtDepth Q (m + 1), 0 ≤ B R) (hbound : ∀ R ∈ descendantsAtDepth Q (m + 1), ∀ S ∈ descendantBoundaryLayerAtDepth R (j - m), F S ≤ B R) : (incrementBoundaryLayerCentersAtDepth Q j m).sum F ≤ 2 * ↑d * (3 ^ (d - 1)) ^ (j - m) * ∑ R ∈ descendantsAtDepth Q (m + 1), B R

theorem HCPolySupport.overlapCrossingCentersAtDepth_subset_incrementBoundaryLayerCentersAtDepth {d : ℕ} (Q : TriadicCube d) {j m : ℕ} (hmj : m ≤ j) : overlapCrossingCentersAtDepth Q j m ⊆ incrementBoundaryLayerCentersAtDepth Q j m

Every crossing center belongs to the boundary layer of its increment-scale ancestor.

theorem HCPolySupport.overlapCrossingCentersAtDepth_sum_le_incrementBoundaryLayerCentersAtDepth_sum {d : ℕ} (Q : TriadicCube d) {j m : ℕ} (hmj : m ≤ j) (F : TriadicCube d → ℝ) (hF : ∀ S ∈ incrementBoundaryLayerCentersAtDepth Q j m, 0 ≤ F S) : (overlapCrossingCentersAtDepth Q j m).sum F ≤ (incrementBoundaryLayerCentersAtDepth Q j m).sum F

theorem HCPolySupport.cubeBesovOverlappingPositiveVectorDepthAverage_cubeIncrementVec_le_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, overlapCubeLpNorm S 2 (overlapCubeFluctuationVec S (cubeIncrementVec Q (m + 1) u)) ^ 2

One-increment depth averages are controlled by the corresponding boundary-layer sum. The remaining work is to count that boundary layer.

theorem HCPolySupport.cubeBesovOverlappingPositiveVectorDepthAverage_cubeIncrementVec_le_const_mul_ancestor_sum {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) {j m : ℕ} (hmj : m ≤ j) (B : TriadicCube d → ℝ) (hB : ∀ R ∈ descendantsAtDepth Q (m + 1), 0 ≤ B R) (hbound : ∀ R ∈ descendantsAtDepth Q (m + 1), ∀ S ∈ descendantBoundaryLayerAtDepth R (j - m), overlapCubeLpNorm S 2 (overlapCubeFluctuationVec S (cubeIncrementVec Q (m + 1) u)) ^ 2 ≤ B R) : cubeBesovOverlappingPositiveVectorDepthAverage Q (cubeIncrementVec Q (m + 1) u) j ≤ (↑(overlapCentersAtDepth Q j).card)⁻¹ * (2 * ↑d * (3 ^ (d - 1)) ^ (j - m) * ∑ R ∈ descendantsAtDepth Q (m + 1), B R)

One-increment overlap averages are controlled by any nonnegative increment-ancestor budget which bounds each boundary-layer center of that ancestor. This is the counted form of the boundary reduction: the only remaining analytic work is to provide the pointwise ancestor budget.

theorem HCPolySupport.overlappingPositiveDepthAverage_increment_le_ancestorSum {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) {j m : ℕ} (hmj : m ≤ j) (B : TriadicCube d → ℝ) (hB : ∀ R ∈ descendantsAtDepth Q (m + 1), 0 ≤ B R) (hbound : ∀ R ∈ descendantsAtDepth Q (m + 1), ∀ S ∈ descendantBoundaryLayerAtDepth R (j - m), overlapCubeLpNorm S 2 (overlapCubeFluctuationVec S (cubeIncrementVec Q (m + 1) u)) ^ 2 ≤ B R) : cubeBesovOverlappingPositiveVectorDepthAverage Q (cubeIncrementVec Q (m + 1) u) j ≤ (↑((3 ^ d) ^ j))⁻¹ * (2 * ↑d * (3 ^ (d - 1)) ^ (j - m) * ∑ R ∈ descendantsAtDepth Q (m + 1), B R)

Lowering the overlap-center normalization to the explicit standard cardinality lower bound gives the scale-separated counted form of the one-increment boundary estimate.