Coarse-graining support:

Support.Deterministic.ConstantCoefficientDirichletBesov.StandardProjectionVector

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

Vector projection API for standard positive Besov depths

This file packages the coordinatewise version of the scalar triadic projection and records that, on each depth-j descendant, the projection residual is exactly the ordinary cube fluctuation used in the standard positive vector norm.

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

Coordinatewise triadic projection of a vector field.

Equations

• HCPolySupport.cubeProjectionVec Q j u x i = HCPolySupport.cubeProjection Q j (fun (y : HCPolySupport.Vec d) => u y i) x

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

Coordinatewise triadic martingale increment of a vector field.

Equations

• HCPolySupport.cubeIncrementVec Q j u x i = HCPolySupport.cubeIncrement Q j (fun (y : HCPolySupport.Vec d) => u y i) x

noncomputable def HCPolySupport.cubeProjectionGapVec {d : ℕ} (Q : TriadicCube d) (j n : ℕ) (u : Vec d → Vec d) : Vec d → Vec d

Coordinatewise projection gap P_{j+n} u - P_j u.

Equations

• HCPolySupport.cubeProjectionGapVec Q j n u x i = HCPolySupport.cubeProjectionGap Q j n (fun (y : HCPolySupport.Vec d) => u y i) x

@[simp]

theorem HCPolySupport.cubeProjectionVec_apply {d : ℕ} (Q : TriadicCube d) (j : ℕ) (u : Vec d → Vec d) (x : Vec d) (i : Fin d) : cubeProjectionVec Q j u x i = cubeProjection Q j (fun (y : Vec d) => u y i) x

@[simp]

theorem HCPolySupport.cubeIncrementVec_apply {d : ℕ} (Q : TriadicCube d) (j : ℕ) (u : Vec d → Vec d) (x : Vec d) (i : Fin d) : cubeIncrementVec Q j u x i = cubeIncrement Q j (fun (y : Vec d) => u y i) x

@[simp]

theorem HCPolySupport.cubeProjectionGapVec_apply {d : ℕ} (Q : TriadicCube d) (j n : ℕ) (u : Vec d → Vec d) (x : Vec d) (i : Fin d) : cubeProjectionGapVec Q j n u x i = cubeProjectionGap Q j n (fun (y : Vec d) => u y i) x

theorem HCPolySupport.cubeProjectionVec_eq_cubeAverageVec_of_mem_descendantsAtDepth {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (u : Vec d → Vec d) {x : Vec d} (hR : R ∈ descendantsAtDepth Q j) (hxR : x ∈ cubeSet R) : cubeProjectionVec Q j u x = cubeAverageVec R u

On a descendant cube, the vector projection is the descendant average.

theorem HCPolySupport.cubeProjectionVec_zero_eq_cubeAverageVec_of_mem_cubeSet {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) {x : Vec d} (hxQ : x ∈ cubeSet Q) : cubeProjectionVec Q 0 u x = cubeAverageVec Q u

Depth-zero vector projections are the parent average on the parent cube.

theorem HCPolySupport.cubeProjectionGapVec_eq_sub_cubeProjectionVec {d : ℕ} (Q : TriadicCube d) (j n : ℕ) (u : Vec d → Vec d) : cubeProjectionGapVec Q j n u = fun (x : Vec d) => cubeProjectionVec Q (j + n) u x - cubeProjectionVec Q j u x

Vector projection gaps are pointwise projection differences.

theorem HCPolySupport.cubeProjectionVec_eq_projection_zero_add_gap_zero {d : ℕ} (Q : TriadicCube d) (j : ℕ) (u : Vec d → Vec d) : cubeProjectionVec Q j u = fun (x : Vec d) => cubeProjectionVec Q 0 u x + cubeProjectionGapVec Q 0 j u x

Projection as depth-zero projection plus the gap from depth zero.

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

Vector projections telescope as a finite sum of coordinatewise increments.

@[simp]

theorem HCPolySupport.cubeProjectionGapVec_zero {d : ℕ} (Q : TriadicCube d) (j : ℕ) (u : Vec d → Vec d) : cubeProjectionGapVec Q j 0 u = 0

theorem HCPolySupport.cubeProjectionVec_eq_average_add_gap_zero_of_mem_cubeSet {d : ℕ} (Q : TriadicCube d) (j : ℕ) (u : Vec d → Vec d) {x : Vec d} (hxQ : x ∈ cubeSet Q) : cubeProjectionVec Q j u x = cubeAverageVec Q u + cubeProjectionGapVec Q 0 j u x

The depth-j vector projection is the parent average plus the gap from depth zero to depth j, on the parent cube.

theorem HCPolySupport.cubeIncrementVec_eq_sub_cubeAverageVec_of_mem_childCubes {d : ℕ} {Q T R : TriadicCube d} {m : ℕ} (u : Vec d → Vec d) (hT : T ∈ descendantsAtDepth Q m) (hRT : R ∈ childCubes T) {x : Vec d} (hxR : x ∈ cubeSet R) : cubeIncrementVec Q (m + 1) u x = cubeAverageVec R u - cubeAverageVec T u

On a child of a depth-m descendant, the vector martingale increment is the child average minus the parent average.

theorem HCPolySupport.exists_const_cubeIncrementVec_on_mem_descendantsAtDepth_succ {d : ℕ} {Q R : TriadicCube d} {m : ℕ} (u : Vec d → Vec d) (hR : R ∈ descendantsAtDepth Q (m + 1)) : ∃ (c : Vec d), ∀ x ∈ cubeSet R, cubeIncrementVec Q (m + 1) u x = c

A vector martingale increment is constant on every standard descendant at its own scale.

theorem HCPolySupport.sub_cubeProjectionVec_eq_cubeFluctuationVec_of_mem_descendantsAtDepth {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (u : Vec d → Vec d) {x : Vec d} (hR : R ∈ descendantsAtDepth Q j) (hxR : x ∈ cubeSet R) : u x - cubeProjectionVec Q j u x = cubeFluctuationVec R u x

On a descendant cube, the vector projection residual is the ordinary fluctuation on that cube.

theorem HCPolySupport.cubeLpNorm_sub_cubeProjectionVec_eq_cubeLpNorm_cubeFluctuationVec_of_mem_descendantsAtDepth {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (u : Vec d → Vec d) (hR : R ∈ descendantsAtDepth Q j) : (cubeLpNorm R 2 fun (x : Vec d) => u x - cubeProjectionVec Q j u x) = cubeLpNorm R 2 (cubeFluctuationVec R u)

The L² norm of the projection residual on a descendant is the ordinary positive fluctuation norm on that descendant.

theorem HCPolySupport.cubeBesovPositiveVectorDepthAverage_eq_projectionVec_residual {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (j : ℕ) : cubeBesovPositiveVectorDepthAverage Q u j = descendantsAverage Q j fun (R : TriadicCube d) => (cubeLpNorm R 2 fun (x : Vec d) => u x - cubeProjectionVec Q j u x) ^ 2

Ordinary positive vector depth averages can be read as projection-residual averages at the same depth.

theorem HCPolySupport.cubeBesovPositiveVectorDepthSeminorm_eq_projectionVec_residual {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (j : ℕ) : cubeBesovPositiveVectorDepthSeminorm Q s u j = Real.rpow 3 (s * ↑j) * √(descendantsAverage Q j fun (R : TriadicCube d) => (cubeLpNorm R 2 fun (x : Vec d) => u x - cubeProjectionVec Q j u x) ^ 2)

Depth seminorm form of cubeBesovPositiveVectorDepthAverage_eq_projectionVec_residual.

theorem HCPolySupport.descendantsAverage_cubeLpNorm_two_sq_eq_cubeLpNorm_two_sq {d : ℕ} (Q : TriadicCube d) (v : Vec d → Vec d) (j : ℕ) (hv : MeasureTheory.MemLp v 2 (normalizedCubeMeasure Q)) : (descendantsAverage Q j fun (R : TriadicCube d) => cubeLpNorm R 2 v ^ 2) = cubeLpNorm Q 2 v ^ 2

The descendant average of squared vector L² norms is the parent squared L² norm.

theorem HCPolySupport.cubeLpNorm_sub_cubeProjectionVec_sq_eq_cubeBesovPositiveVectorDepthAverage {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)) : (cubeLpNorm Q 2 fun (x : Vec d) => u x - cubeProjectionVec Q j u x) ^ 2 = cubeBesovPositiveVectorDepthAverage Q u j

The parent L² norm of the depth-j projection residual is exactly the ordinary positive depth average.