Coarse-graining support:

Support.Deterministic.ConstantCoefficientDirichletBesov.StandardProjectionSharpKernel

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

The sharp boundary tail as a geometric kernel input

The one-depth sharp boundary estimate leaves a concrete tail over coarser standard projection depths. This file names that tail and connects any geometric-kernel bound for it to the finite positive Besov summation theorem.

structure HCPolySupport.SharpBoundaryProjectionMemLp {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) : Prop

MemLp closure hypotheses needed by the sharp-boundary standard projection comparison. These are bookkeeping assumptions: the analytic content is in the finite bridge below.

• residual (j : ℕ) : MeasureTheory.MemLp (fun (x : Vec d) => u x - cubeProjectionVec Q j u x) 2 (normalizedCubeMeasure Q)
• residual_overlap (j : ℕ) (S : TriadicCube d) : S ∈ overlapCentersAtDepth Q j → MeasureTheory.MemLp (fun (x : Vec d) => u x - cubeProjectionVec Q j u x) 2 (normalizedOverlapCubeMeasure S)
• projection_overlap (j : ℕ) (S : TriadicCube d) : S ∈ overlapCentersAtDepth Q j → MeasureTheory.MemLp (cubeProjectionVec Q j u) 2 (normalizedOverlapCubeMeasure S)
• projection_zero_overlap (j : ℕ) (S : TriadicCube d) : S ∈ overlapCentersAtDepth Q j → MeasureTheory.MemLp (cubeProjectionVec Q 0 u) 2 (normalizedOverlapCubeMeasure S)
• projection_gap_overlap (j : ℕ) (S : TriadicCube d) : S ∈ overlapCentersAtDepth Q j → MeasureTheory.MemLp (cubeProjectionGapVec Q 0 j u) 2 (normalizedOverlapCubeMeasure S)
• increment_overlap (j : ℕ) (S : TriadicCube d) : S ∈ overlapCentersAtDepth Q j → ∀ m ∈ Finset.range j, MeasureTheory.MemLp (cubeIncrementVec Q (m + 1) u) 2 (normalizedOverlapCubeMeasure S)
• parent (j m : ℕ) : m ∈ Finset.range j → ∀ T ∈ descendantsAtDepth Q m, MeasureTheory.MemLp u 2 (normalizedCubeMeasure T)

theorem HCPolySupport.cubeProjectionVec_memLp_normalizedCubeMeasure {d : ℕ} (Q : TriadicCube d) (j : ℕ) (u : Vec d → Vec d) : MeasureTheory.MemLp (cubeProjectionVec Q j u) 2 (normalizedCubeMeasure Q)

The vector standard projection is L² on its parent cube.

theorem HCPolySupport.cubeProjectionVec_memLp_normalizedOverlapCubeMeasure {d : ℕ} {Q S : TriadicCube d} {j k : ℕ} (u : Vec d → Vec d) (hS : S ∈ overlapCentersAtDepth Q j) : MeasureTheory.MemLp (cubeProjectionVec Q k u) 2 (normalizedOverlapCubeMeasure S)

The vector standard projection restricts to every admissible overlap cube.

theorem HCPolySupport.cubeProjectionVec_residual_memLp_normalizedCubeMeasure {d : ℕ} {Q : TriadicCube d} (j : ℕ) {u : Vec d → Vec d} (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) : MeasureTheory.MemLp (fun (x : Vec d) => u x - cubeProjectionVec Q j u x) 2 (normalizedCubeMeasure Q)

The vector projection residual is L² on the parent cube.

theorem HCPolySupport.cubeProjectionVec_residual_memLp_normalizedOverlapCubeMeasure {d : ℕ} {Q S : TriadicCube d} {j : ℕ} {u : Vec d → Vec d} (hS : S ∈ overlapCentersAtDepth Q j) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) : MeasureTheory.MemLp (fun (x : Vec d) => u x - cubeProjectionVec Q j u x) 2 (normalizedOverlapCubeMeasure S)

The vector projection residual restricts to every admissible overlap cube.

theorem HCPolySupport.cubeProjectionGapVec_memLp_normalizedCubeMeasure {d : ℕ} (Q : TriadicCube d) (j n : ℕ) (u : Vec d → Vec d) : MeasureTheory.MemLp (cubeProjectionGapVec Q j n u) 2 (normalizedCubeMeasure Q)

A vector projection gap is the difference of two vector projections.

theorem HCPolySupport.cubeProjectionGapVec_memLp_normalizedOverlapCubeMeasure {d : ℕ} {Q S : TriadicCube d} {j : ℕ} (n : ℕ) (u : Vec d → Vec d) (hS : S ∈ overlapCentersAtDepth Q j) : MeasureTheory.MemLp (cubeProjectionGapVec Q 0 n u) 2 (normalizedOverlapCubeMeasure S)

A vector projection gap restricts to every admissible overlap cube.

theorem HCPolySupport.cubeIncrementVec_succ_eq_sub_cubeProjectionVec {d : ℕ} (Q : TriadicCube d) (m : ℕ) (u : Vec d → Vec d) : cubeIncrementVec Q (m + 1) u = fun (x : Vec d) => cubeProjectionVec Q (m + 1) u x - cubeProjectionVec Q m u x

The vector martingale increment is the difference of consecutive vector standard projections.

theorem HCPolySupport.cubeIncrementVec_memLp_normalizedCubeMeasure {d : ℕ} (Q : TriadicCube d) (m : ℕ) (u : Vec d → Vec d) : MeasureTheory.MemLp (cubeIncrementVec Q (m + 1) u) 2 (normalizedCubeMeasure Q)

A vector martingale increment is L² on the parent cube.

theorem HCPolySupport.cubeIncrementVec_memLp_normalizedOverlapCubeMeasure {d : ℕ} {Q S : TriadicCube d} {j : ℕ} (m : ℕ) (u : Vec d → Vec d) (hS : S ∈ overlapCentersAtDepth Q j) : MeasureTheory.MemLp (cubeIncrementVec Q (m + 1) u) 2 (normalizedOverlapCubeMeasure S)

A vector martingale increment restricts to every admissible overlap cube.

theorem HCPolySupport.SharpBoundaryProjectionMemLp.of_memLp {d : ℕ} {Q : TriadicCube d} {u : Vec d → Vec d} (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) : SharpBoundaryProjectionMemLp Q u

The sharp-boundary projection MemLp closure package follows from parent L² membership. All projection, gap, and increment fields are finite-depth piecewise constants, and all overlap cubes are measured by restriction from the parent cube.

theorem HCPolySupport.triadicPositiveDepthWeight_eq_pow (t : ℝ) (j : ℕ) : Real.rpow 3 (t * ↑j) = Real.rpow 3 t ^ j

Positive triadic depth weights as powers of the one-step weight.

noncomputable def HCPolySupport.sharpBoundaryKernelConstant (d : ℕ) : ℝ

Dimension-only constant in the sharp boundary kernel.

Equations

• HCPolySupport.sharpBoundaryKernelConstant d = √(4 * ↑(3 ^ d * (3 ^ d * (2 * d))) * (3 ^ d * ↑(Fintype.card (Fin d))))

noncomputable def HCPolySupport.sharpBoundaryKernelRatio (d : ℕ) : ℝ

The square-root surface/volume ratio in one gap of the sharp boundary kernel. For positive dimension this is 3^{-1/2}.

Equations

• HCPolySupport.sharpBoundaryKernelRatio d = √(↑(3 ^ (d - 1)) / ↑(3 ^ d))

noncomputable def HCPolySupport.sharpBoundaryKernelBase (d : ℕ) (t : ℝ) : ℝ

One-gap kernel base before replacing the dimension ratio by 3^{-1/2}.

Equations

• HCPolySupport.sharpBoundaryKernelBase d t = Real.rpow 3 t * HCPolySupport.sharpBoundaryKernelRatio d

noncomputable def HCPolySupport.sharpBoundaryKernelLoss (d : ℕ) (t : ℝ) : ℝ

The explicit finite-depth sharp-boundary loss. For positive dimension and t < 1/2, the denominator is finite because sharpBoundaryKernelBase d t = 3^(t - 1/2) < 1.

Equations

• HCPolySupport.sharpBoundaryKernelLoss d t = 8 * 3 ^ d + 4 * HCPolySupport.sharpBoundaryKernelConstant d ^ 2 * (1 - HCPolySupport.sharpBoundaryKernelBase d t)⁻¹ ^ 2

theorem HCPolySupport.sharpBoundaryKernelConstant_nonneg (d : ℕ) : 0 ≤ sharpBoundaryKernelConstant d

theorem HCPolySupport.sharpBoundaryKernelRatio_nonneg (d : ℕ) : 0 ≤ sharpBoundaryKernelRatio d

theorem HCPolySupport.sharpBoundaryKernelBase_nonneg (d : ℕ) (t : ℝ) : 0 ≤ sharpBoundaryKernelBase d t

theorem HCPolySupport.sharpBoundaryKernelLoss_nonneg (d : ℕ) (t : ℝ) : 0 ≤ sharpBoundaryKernelLoss d t

theorem HCPolySupport.sharpBoundaryKernelRatio_eq {d : ℕ} [NeZero d] : sharpBoundaryKernelRatio d = Real.rpow 3 (-(1 / 2))

theorem HCPolySupport.sharpBoundaryKernelBase_eq {d : ℕ} [NeZero d] (t : ℝ) : sharpBoundaryKernelBase d t = Real.rpow 3 (t - 1 / 2)

theorem HCPolySupport.sharpBoundaryKernelBase_lt_one {d : ℕ} [NeZero d] {t : ℝ} (ht : t < 1 / 2) : sharpBoundaryKernelBase d t < 1

noncomputable def HCPolySupport.sharpBoundaryDepthTailTerm {d : ℕ} (Q : TriadicCube d) (t : ℝ) (u : Vec d → Vec d) (j m : ℕ) : ℝ

The mth summand in the sharp boundary tail at depth j.

Equations

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

noncomputable def HCPolySupport.sharpBoundaryDepthTail {d : ℕ} (Q : TriadicCube d) (t : ℝ) (u : Vec d → Vec d) (j : ℕ) : ℝ

The sharp boundary tail appearing in the one-depth hard comparison.

Equations

• HCPolySupport.sharpBoundaryDepthTail Q t u j = ∑ m ∈ Finset.range j, HCPolySupport.sharpBoundaryDepthTailTerm Q t u j m

theorem HCPolySupport.sharpBoundaryDepthTailTerm_nonneg {d : ℕ} (Q : TriadicCube d) (t : ℝ) (u : Vec d → Vec d) (j m : ℕ) : 0 ≤ sharpBoundaryDepthTailTerm Q t u j m

theorem HCPolySupport.sharpBoundaryDepthTailTerm_le_kernelBase_add {d : ℕ} (Q : TriadicCube d) (t : ℝ) (u : Vec d → Vec d) (m n : ℕ) : sharpBoundaryDepthTailTerm Q t u (m + n) m ≤ sharpBoundaryKernelConstant d * sharpBoundaryKernelBase d t ^ n * cubeBesovPositiveVectorDepthSeminorm Q t u m

Single-summand scale arithmetic for the sharp boundary tail, in the clean j = m + n form.

theorem HCPolySupport.sharpBoundaryDepthTailTerm_le_kernelBase {d : ℕ} (Q : TriadicCube d) (t : ℝ) (u : Vec d → Vec d) {j m : ℕ} (hmj : m ≤ j) : sharpBoundaryDepthTailTerm Q t u j m ≤ sharpBoundaryKernelConstant d * sharpBoundaryKernelBase d t ^ (j - m) * cubeBesovPositiveVectorDepthSeminorm Q t u m

Single-summand scale arithmetic for the sharp boundary tail.

theorem HCPolySupport.sharpBoundaryDepthTail_nonneg {d : ℕ} (Q : TriadicCube d) (t : ℝ) (u : Vec d → Vec d) (j : ℕ) : 0 ≤ sharpBoundaryDepthTail Q t u j

theorem HCPolySupport.sharpBoundaryDepthTail_le_geometric_convolution_of_forall_term_le {d : ℕ} (Q : TriadicCube d) (t : ℝ) (u : Vec d → Vec d) (j : ℕ) {C r : ℝ} (hterm : ∀ m ∈ Finset.range j, sharpBoundaryDepthTailTerm Q t u j m ≤ C * (r ^ (j - m) * cubeBesovPositiveVectorDepthSeminorm Q t u m)) : sharpBoundaryDepthTail Q t u j ≤ C * ∑ m ∈ Finset.range j, r ^ (j - m) * cubeBesovPositiveVectorDepthSeminorm Q t u m

Summing termwise geometric bounds gives the sharp-tail geometric kernel bound.

theorem HCPolySupport.sq_cubeBesovOverlappingPositiveVectorDepthSeminorm_le_standard_add_sharpBoundaryDepthTail {d : ℕ} (Q : TriadicCube d) (t : ℝ) (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)) : cubeBesovOverlappingPositiveVectorDepthSeminorm Q t u j ^ 2 ≤ 8 * 3 ^ d * cubeBesovPositiveVectorDepthSeminorm Q t u j ^ 2 + 4 * sharpBoundaryDepthTail Q t u j ^ 2

Named form of the one-depth hard comparison using sharpBoundaryDepthTail.

theorem HCPolySupport.sq_cubeBesovOverlappingPositiveVectorPartialSeminormTwo_le_of_sharpBoundaryDepthTail_kernel {d : ℕ} (Q : TriadicCube d) (t : ℝ) (N : ℕ) (u : Vec d → Vec d) {C r : ℝ} (hC_nonneg : 0 ≤ C) (hr_nonneg : 0 ≤ r) (hr_lt_one : r < 1) (hres : ∀ j ∈ Finset.range (N + 1), MeasureTheory.MemLp (fun (x : Vec d) => u x - cubeProjectionVec Q j u x) 2 (normalizedCubeMeasure Q)) (hresLoc : ∀ j ∈ Finset.range (N + 1), ∀ S ∈ overlapCentersAtDepth Q j, MeasureTheory.MemLp (fun (x : Vec d) => u x - cubeProjectionVec Q j u x) 2 (normalizedOverlapCubeMeasure S)) (hprojLoc : ∀ j ∈ Finset.range (N + 1), ∀ S ∈ overlapCentersAtDepth Q j, MeasureTheory.MemLp (cubeProjectionVec Q j u) 2 (normalizedOverlapCubeMeasure S)) (hzeroLoc : ∀ j ∈ Finset.range (N + 1), ∀ S ∈ overlapCentersAtDepth Q j, MeasureTheory.MemLp (cubeProjectionVec Q 0 u) 2 (normalizedOverlapCubeMeasure S)) (hgapLoc : ∀ j ∈ Finset.range (N + 1), ∀ S ∈ overlapCentersAtDepth Q j, MeasureTheory.MemLp (cubeProjectionGapVec Q 0 j u) 2 (normalizedOverlapCubeMeasure S)) (hincLoc : ∀ j ∈ Finset.range (N + 1), ∀ S ∈ overlapCentersAtDepth Q j, ∀ m ∈ Finset.range j, MeasureTheory.MemLp (cubeIncrementVec Q (m + 1) u) 2 (normalizedOverlapCubeMeasure S)) (huParent : ∀ j ∈ Finset.range (N + 1), ∀ m ∈ Finset.range j, ∀ T ∈ descendantsAtDepth Q m, MeasureTheory.MemLp u 2 (normalizedCubeMeasure T)) (hkernel : ∀ j ∈ Finset.range (N + 1), sharpBoundaryDepthTail Q t u j ≤ C * ∑ m ∈ Finset.range j, r ^ (j - m) * cubeBesovPositiveVectorDepthSeminorm Q t u m) : cubeBesovOverlappingPositiveVectorPartialSeminormTwo Q t N u ^ 2 ≤ (8 * 3 ^ d + 4 * C ^ 2 * (1 - r)⁻¹ ^ 2) * cubeBesovPositiveVectorPartialSeminormTwo Q t N u ^ 2

If the named sharp boundary tail is bounded by a geometric convolution of ordinary positive depth seminorms, then the finite overlapping positive seminorm is bounded by the ordinary finite positive seminorm.

theorem HCPolySupport.sq_cubeBesovOverlappingPositiveVectorPartialSeminormTwo_le_of_sharpBoundaryDepthTailTerm_kernel {d : ℕ} [NeZero d] (Q : TriadicCube d) (t : ℝ) (N : ℕ) (u : Vec d → Vec d) {C : ℝ} (ht : t < 1 / 2) (hC_nonneg : 0 ≤ C) (hres : ∀ j ∈ Finset.range (N + 1), MeasureTheory.MemLp (fun (x : Vec d) => u x - cubeProjectionVec Q j u x) 2 (normalizedCubeMeasure Q)) (hresLoc : ∀ j ∈ Finset.range (N + 1), ∀ S ∈ overlapCentersAtDepth Q j, MeasureTheory.MemLp (fun (x : Vec d) => u x - cubeProjectionVec Q j u x) 2 (normalizedOverlapCubeMeasure S)) (hprojLoc : ∀ j ∈ Finset.range (N + 1), ∀ S ∈ overlapCentersAtDepth Q j, MeasureTheory.MemLp (cubeProjectionVec Q j u) 2 (normalizedOverlapCubeMeasure S)) (hzeroLoc : ∀ j ∈ Finset.range (N + 1), ∀ S ∈ overlapCentersAtDepth Q j, MeasureTheory.MemLp (cubeProjectionVec Q 0 u) 2 (normalizedOverlapCubeMeasure S)) (hgapLoc : ∀ j ∈ Finset.range (N + 1), ∀ S ∈ overlapCentersAtDepth Q j, MeasureTheory.MemLp (cubeProjectionGapVec Q 0 j u) 2 (normalizedOverlapCubeMeasure S)) (hincLoc : ∀ j ∈ Finset.range (N + 1), ∀ S ∈ overlapCentersAtDepth Q j, ∀ m ∈ Finset.range j, MeasureTheory.MemLp (cubeIncrementVec Q (m + 1) u) 2 (normalizedOverlapCubeMeasure S)) (huParent : ∀ j ∈ Finset.range (N + 1), ∀ m ∈ Finset.range j, ∀ T ∈ descendantsAtDepth Q m, MeasureTheory.MemLp u 2 (normalizedCubeMeasure T)) (hterm : ∀ j ∈ Finset.range (N + 1), ∀ m ∈ Finset.range j, sharpBoundaryDepthTailTerm Q t u j m ≤ C * sharpBoundaryKernelBase d t ^ (j - m) * cubeBesovPositiveVectorDepthSeminorm Q t u m) : cubeBesovOverlappingPositiveVectorPartialSeminormTwo Q t N u ^ 2 ≤ (8 * 3 ^ d + 4 * C ^ 2 * (1 - sharpBoundaryKernelBase d t)⁻¹ ^ 2) * cubeBesovPositiveVectorPartialSeminormTwo Q t N u ^ 2

Version of sq_cubeBesovOverlappingPositiveVectorPartialSeminormTwo_le_of_sharpBoundaryDepthTail_kernel where the geometric kernel bound is supplied term-by-term with the canonical sharp boundary kernel base. The only remaining input is the local single-summand scale arithmetic estimate.

theorem HCPolySupport.sq_cubeBesovOverlappingPositiveVectorPartialSeminormTwo_le_sharpBoundaryKernel {d : ℕ} [NeZero d] (Q : TriadicCube d) (t : ℝ) (N : ℕ) (u : Vec d → Vec d) (ht : t < 1 / 2) (hres : ∀ j ∈ Finset.range (N + 1), MeasureTheory.MemLp (fun (x : Vec d) => u x - cubeProjectionVec Q j u x) 2 (normalizedCubeMeasure Q)) (hresLoc : ∀ j ∈ Finset.range (N + 1), ∀ S ∈ overlapCentersAtDepth Q j, MeasureTheory.MemLp (fun (x : Vec d) => u x - cubeProjectionVec Q j u x) 2 (normalizedOverlapCubeMeasure S)) (hprojLoc : ∀ j ∈ Finset.range (N + 1), ∀ S ∈ overlapCentersAtDepth Q j, MeasureTheory.MemLp (cubeProjectionVec Q j u) 2 (normalizedOverlapCubeMeasure S)) (hzeroLoc : ∀ j ∈ Finset.range (N + 1), ∀ S ∈ overlapCentersAtDepth Q j, MeasureTheory.MemLp (cubeProjectionVec Q 0 u) 2 (normalizedOverlapCubeMeasure S)) (hgapLoc : ∀ j ∈ Finset.range (N + 1), ∀ S ∈ overlapCentersAtDepth Q j, MeasureTheory.MemLp (cubeProjectionGapVec Q 0 j u) 2 (normalizedOverlapCubeMeasure S)) (hincLoc : ∀ j ∈ Finset.range (N + 1), ∀ S ∈ overlapCentersAtDepth Q j, ∀ m ∈ Finset.range j, MeasureTheory.MemLp (cubeIncrementVec Q (m + 1) u) 2 (normalizedOverlapCubeMeasure S)) (huParent : ∀ j ∈ Finset.range (N + 1), ∀ m ∈ Finset.range j, ∀ T ∈ descendantsAtDepth Q m, MeasureTheory.MemLp u 2 (normalizedCubeMeasure T)) : cubeBesovOverlappingPositiveVectorPartialSeminormTwo Q t N u ^ 2 ≤ (8 * 3 ^ d + 4 * sharpBoundaryKernelConstant d ^ 2 * (1 - sharpBoundaryKernelBase d t)⁻¹ ^ 2) * cubeBesovPositiveVectorPartialSeminormTwo Q t N u ^ 2

Closed finite partial bridge for the sharp boundary branch. The overlapping exponent must satisfy t < 1/2, exactly because the sharp boundary kernel has base 3^(t - 1/2).

theorem HCPolySupport.cubeBesovOverlappingPositiveVectorPartialSeminormTwo_le_sqrt_sharpBoundaryKernel {d : ℕ} [NeZero d] (Q : TriadicCube d) (t : ℝ) (N : ℕ) (u : Vec d → Vec d) (ht : t < 1 / 2) (hres : ∀ j ∈ Finset.range (N + 1), MeasureTheory.MemLp (fun (x : Vec d) => u x - cubeProjectionVec Q j u x) 2 (normalizedCubeMeasure Q)) (hresLoc : ∀ j ∈ Finset.range (N + 1), ∀ S ∈ overlapCentersAtDepth Q j, MeasureTheory.MemLp (fun (x : Vec d) => u x - cubeProjectionVec Q j u x) 2 (normalizedOverlapCubeMeasure S)) (hprojLoc : ∀ j ∈ Finset.range (N + 1), ∀ S ∈ overlapCentersAtDepth Q j, MeasureTheory.MemLp (cubeProjectionVec Q j u) 2 (normalizedOverlapCubeMeasure S)) (hzeroLoc : ∀ j ∈ Finset.range (N + 1), ∀ S ∈ overlapCentersAtDepth Q j, MeasureTheory.MemLp (cubeProjectionVec Q 0 u) 2 (normalizedOverlapCubeMeasure S)) (hgapLoc : ∀ j ∈ Finset.range (N + 1), ∀ S ∈ overlapCentersAtDepth Q j, MeasureTheory.MemLp (cubeProjectionGapVec Q 0 j u) 2 (normalizedOverlapCubeMeasure S)) (hincLoc : ∀ j ∈ Finset.range (N + 1), ∀ S ∈ overlapCentersAtDepth Q j, ∀ m ∈ Finset.range j, MeasureTheory.MemLp (cubeIncrementVec Q (m + 1) u) 2 (normalizedOverlapCubeMeasure S)) (huParent : ∀ j ∈ Finset.range (N + 1), ∀ m ∈ Finset.range j, ∀ T ∈ descendantsAtDepth Q m, MeasureTheory.MemLp u 2 (normalizedCubeMeasure T)) : cubeBesovOverlappingPositiveVectorPartialSeminormTwo Q t N u ≤ √(8 * 3 ^ d + 4 * sharpBoundaryKernelConstant d ^ 2 * (1 - sharpBoundaryKernelBase d t)⁻¹ ^ 2) * cubeBesovPositiveVectorPartialSeminormTwo Q t N u

Square-root form of sq_cubeBesovOverlappingPositiveVectorPartialSeminormTwo_le_sharpBoundaryKernel.

theorem HCPolySupport.CubeVectorOverlappingBesovHRegularity.of_sharpBoundaryKernel {d : ℕ} [NeZero d] {Q : TriadicCube d} {t : ℝ} {u : Vec d → Vec d} (ht : t < 1 / 2) (hstd : CubeVectorBesovHRegularity Q t u) (hmem : SharpBoundaryProjectionMemLp Q u) : CubeVectorOverlappingBesovHRegularity Q t u

Full overlapping regularity from ordinary positive regularity and the sharp-boundary projection MemLp closure package.

theorem HCPolySupport.cubeBesovOverlappingPositiveVectorSeminormTwo_le_sqrt_sharpBoundaryKernel {d : ℕ} [NeZero d] (Q : TriadicCube d) (t : ℝ) (u : Vec d → Vec d) (ht : t < 1 / 2) (hstd : CubeVectorBesovHRegularity Q t u) (hmem : SharpBoundaryProjectionMemLp Q u) : cubeBesovOverlappingPositiveVectorSeminormTwo Q t u ≤ √(sharpBoundaryKernelLoss d t) * cubeBesovPositiveVectorSeminormTwo Q t u

Full seminorm form of the sharp-boundary comparison.

theorem HCPolySupport.cubeBesovOverlappingPositiveVectorNormTwo_le_one_add_sqrt_sharpBoundaryKernel {d : ℕ} [NeZero d] (Q : TriadicCube d) (t : ℝ) (u : Vec d → Vec d) (ht : t < 1 / 2) (hstd : CubeVectorBesovHRegularity Q t u) (hmem : SharpBoundaryProjectionMemLp Q u) : cubeBesovOverlappingPositiveVectorNormTwo Q t u ≤ (1 + √(sharpBoundaryKernelLoss d t)) * cubeBesovPositiveVectorNormTwo Q t u

Full norm form of the sharp-boundary comparison. The average part is common to the two positive norms, so the seminorm loss becomes 1 + sqrt L on the full norm.