Coarse-graining support:

Support.Deterministic.ConstantCoefficientDirichletBesov.StandardProjectionResidual

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

Overlap bounds for standard projection residuals

This file isolates the residual half of the hard comparison from the corrected overlapping positive norm back to the ordinary triadic positive norm. After subtracting the depth-j standard projection, the existing finite-overlap residual estimate controls the overlapping depth-j oscillation by the ordinary depth-j positive average.

theorem HCPolySupport.cubeBesovOverlappingPositiveVectorDepthAverage_sub_cubeProjectionVec_le {d : ℕ} (Q : TriadicCube d) (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)) : cubeBesovOverlappingPositiveVectorDepthAverage Q (fun (x : Vec d) => u x - cubeProjectionVec Q j u x) j ≤ 4 * 3 ^ d * cubeBesovPositiveVectorDepthAverage Q u j

The overlapping depth average of the depth-j standard projection residual is controlled by the ordinary positive depth average at the same scale.

theorem HCPolySupport.overlapCubeAverageVec_cubeProjectionVec_zero_of_mem_overlapCentersAtDepth {d : ℕ} {Q S : TriadicCube d} {j : ℕ} (u : Vec d → Vec d) (hS : S ∈ overlapCentersAtDepth Q j) : overlapCubeAverageVec S (cubeProjectionVec Q 0 u) = cubeAverageVec Q u

The depth-zero standard projection is constant on every admissible overlap cube, so its overlap average is the parent average.

theorem HCPolySupport.overlapCubeLpNorm_overlapCubeFluctuationVec_cubeProjectionVec_zero_eq_zero {d : ℕ} {Q S : TriadicCube d} {j : ℕ} (u : Vec d → Vec d) (hS : S ∈ overlapCentersAtDepth Q j) : overlapCubeLpNorm S 2 (overlapCubeFluctuationVec S (cubeProjectionVec Q 0 u)) = 0

The depth-zero standard projection has zero overlap fluctuation on every admissible overlap cube.

theorem HCPolySupport.cubeBesovOverlappingPositiveVectorDepthAverage_cubeProjectionVec_zero_eq_zero {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (j : ℕ) : cubeBesovOverlappingPositiveVectorDepthAverage Q (cubeProjectionVec Q 0 u) j = 0

The depth-zero standard projection contributes no corrected overlapping positive depth average.

theorem HCPolySupport.cubeBesovOverlappingPositiveVectorDepthSeminorm_cubeProjectionVec_zero_eq_zero {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (j : ℕ) : cubeBesovOverlappingPositiveVectorDepthSeminorm Q s (cubeProjectionVec Q 0 u) j = 0

Seminorm form of cubeBesovOverlappingPositiveVectorDepthAverage_cubeProjectionVec_zero_eq_zero.

theorem HCPolySupport.overlapCubeLpNorm_overlapCubeFluctuationVec_cubeIncrementVec_eq_zero_of_subset_descendant {d : ℕ} {Q S R : TriadicCube d} {m : ℕ} (u : Vec d → Vec d) (hR : R ∈ descendantsAtDepth Q (m + 1)) (hsub : overlapCubeSet S ⊆ cubeSet R) : overlapCubeLpNorm S 2 (overlapCubeFluctuationVec S (cubeIncrementVec Q (m + 1) u)) = 0

If an overlap cube is contained in one standard descendant at the scale of a martingale increment, then that increment has zero overlap fluctuation on the overlap cube.

theorem HCPolySupport.cubeBesovOverlappingPositiveVectorDepthAverage_congr_on_overlapCenters {d : ℕ} (Q : TriadicCube d) (j : ℕ) {u v : Vec d → Vec d} (h : ∀ S ∈ overlapCentersAtDepth Q j, ∀ x ∈ overlapCubeSet S, u x = v x) : cubeBesovOverlappingPositiveVectorDepthAverage Q u j = cubeBesovOverlappingPositiveVectorDepthAverage Q v j

Corrected overlapping depth averages only depend on the tested function on the overlap cubes used at that depth.

theorem HCPolySupport.overlapCubeLpNorm_overlapCubeFluctuationVec_finset_sum_le {d : ℕ} {ι : Type u_1} (S : TriadicCube d) (I : Finset ι) (u : ι → Vec d → Vec d) (hu : ∀ i ∈ I, MeasureTheory.MemLp (u i) 2 (normalizedOverlapCubeMeasure S)) : overlapCubeLpNorm S 2 (overlapCubeFluctuationVec S fun (x : Vec d) => ∑ i ∈ I, u i x) ≤ ∑ i ∈ I, overlapCubeLpNorm S 2 (overlapCubeFluctuationVec S (u i))

Triangle inequality for the overlap fluctuation of a finite sum.

theorem HCPolySupport.sqrt_cubeBesovOverlappingPositiveVectorDepthAverage_finset_sum_le {d : ℕ} {ι : Type u_1} (Q : TriadicCube d) (j : ℕ) (I : Finset ι) (u : ι → Vec d → Vec d) (hu : ∀ S ∈ overlapCentersAtDepth Q j, ∀ i ∈ I, MeasureTheory.MemLp (u i) 2 (normalizedOverlapCubeMeasure S)) : √(cubeBesovOverlappingPositiveVectorDepthAverage Q (fun (x : Vec d) => ∑ i ∈ I, u i x) j) ≤ ∑ i ∈ I, √(cubeBesovOverlappingPositiveVectorDepthAverage Q (u i) j)

Minkowski inequality for corrected overlapping depth averages of finite sums, in square-root form.

theorem HCPolySupport.cubeBesovOverlappingPositiveVectorDepthAverage_cubeProjectionVec_le_gap_zero {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (j : ℕ) (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)) : cubeBesovOverlappingPositiveVectorDepthAverage Q (cubeProjectionVec Q j u) j ≤ 2 * cubeBesovOverlappingPositiveVectorDepthAverage Q (cubeProjectionGapVec Q 0 j u) j

The projection part of the hard comparison reduces to the projection gap from depth zero. This is the algebraic split before estimating the gap by ordinary standard positive terms.

theorem HCPolySupport.cubeBesovOverlappingPositiveVectorDepthAverage_le_residual_add_projection {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (j : ℕ) (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)) : cubeBesovOverlappingPositiveVectorDepthAverage Q u j ≤ 2 * cubeBesovOverlappingPositiveVectorDepthAverage Q (fun (x : Vec d) => u x - cubeProjectionVec Q j u x) j + 2 * cubeBesovOverlappingPositiveVectorDepthAverage Q (cubeProjectionVec Q j u) j

Split a field into its depth-j standard projection residual plus its depth-j standard projection, at the corrected overlapping depth average.

theorem HCPolySupport.sq_cubeBesovOverlappingPositiveVectorDepthSeminorm_cubeProjectionVec_le_gap_zero {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (j : ℕ) (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)) : cubeBesovOverlappingPositiveVectorDepthSeminorm Q s (cubeProjectionVec Q j u) j ^ 2 ≤ 2 * cubeBesovOverlappingPositiveVectorDepthSeminorm Q s (cubeProjectionGapVec Q 0 j u) j ^ 2

Seminorm-squared form of cubeBesovOverlappingPositiveVectorDepthAverage_cubeProjectionVec_le_gap_zero.

theorem HCPolySupport.cubeBesovOverlappingPositiveVectorDepthAverage_gap_zero_eq_sum_incrementVec {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (j : ℕ) : cubeBesovOverlappingPositiveVectorDepthAverage Q (cubeProjectionGapVec Q 0 j u) j = cubeBesovOverlappingPositiveVectorDepthAverage Q (fun (x : Vec d) => ∑ m ∈ Finset.range j, cubeIncrementVec Q (m + 1) u x) j

The depth-j projection gap from depth zero is the finite sum of vector martingale increments, at the level of corrected overlapping depth averages.

theorem HCPolySupport.cubeBesovOverlappingPositiveVectorDepthSeminorm_gap_zero_eq_sum_incrementVec {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (j : ℕ) : cubeBesovOverlappingPositiveVectorDepthSeminorm Q s (cubeProjectionGapVec Q 0 j u) j = cubeBesovOverlappingPositiveVectorDepthSeminorm Q s (fun (x : Vec d) => ∑ m ∈ Finset.range j, cubeIncrementVec Q (m + 1) u x) j

Seminorm form of cubeBesovOverlappingPositiveVectorDepthAverage_gap_zero_eq_sum_incrementVec.

theorem HCPolySupport.sqrt_cubeBesovOverlappingPositiveVectorDepthAverage_gap_zero_le_sum_incrementVec {d : ℕ} (Q : TriadicCube d) (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)) : √(cubeBesovOverlappingPositiveVectorDepthAverage Q (cubeProjectionGapVec Q 0 j u) j) ≤ ∑ m ∈ Finset.range j, √(cubeBesovOverlappingPositiveVectorDepthAverage Q (cubeIncrementVec Q (m + 1) u) j)

The projection gap is controlled, in corrected overlapping square-root depth average, by the sum of its martingale increments.

theorem HCPolySupport.cubeBesovOverlappingPositiveVectorDepthSeminorm_gap_zero_le_sum_incrementVec {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)) : cubeBesovOverlappingPositiveVectorDepthSeminorm Q s (cubeProjectionGapVec Q 0 j u) j ≤ ∑ m ∈ Finset.range j, cubeBesovOverlappingPositiveVectorDepthSeminorm Q s (cubeIncrementVec Q (m + 1) u) j

Seminorm form of sqrt_cubeBesovOverlappingPositiveVectorDepthAverage_gap_zero_le_sum_incrementVec.

theorem HCPolySupport.sq_cubeBesovOverlappingPositiveVectorDepthSeminorm_sub_cubeProjectionVec_le {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)) : cubeBesovOverlappingPositiveVectorDepthSeminorm Q s (fun (x : Vec d) => u x - cubeProjectionVec Q j u x) j ^ 2 ≤ 4 * 3 ^ d * cubeBesovPositiveVectorDepthSeminorm Q s u j ^ 2

Seminorm-squared form of cubeBesovOverlappingPositiveVectorDepthAverage_sub_cubeProjectionVec_le.

theorem HCPolySupport.sq_cubeBesovOverlappingPositiveVectorDepthSeminorm_le_standard_add_gap_zero {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)) : cubeBesovOverlappingPositiveVectorDepthSeminorm Q s u j ^ 2 ≤ 8 * 3 ^ d * cubeBesovPositiveVectorDepthSeminorm Q s u j ^ 2 + 4 * cubeBesovOverlappingPositiveVectorDepthSeminorm Q s (cubeProjectionGapVec Q 0 j u) j ^ 2

Combined depth split for the hard comparison. The residual branch is paid by the ordinary same-depth positive term, while the projection branch is paid by the depth-zero projection gap.