Coarse-graining support:

Support.Deterministic.HomogenizationBlackBoxes.DualityPositiveBridge.CoordinateStandard

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

Coordinate full-dual tests and the standard positive norm

This file separates the purely algebraic coordinate insertion step from the remaining finite-overlap localization estimate. A scalar full-dual unit test inserted into one coordinate has controlled ordinary positive vector Besov norm; the still-analytic bridge is the passage from that ordinary norm to the corrected overlapping norm used by the Dirichlet theorem.

@[simp]

theorem HCPolySupport.cubeAverageVec_coordinateVectorField_same {d : ℕ} (Q : TriadicCube d) (i : Fin d) (g : Vec d → ℝ) : cubeAverageVec Q (coordinateVectorField i g) i = cubeAverage Q g

@[simp]

theorem HCPolySupport.cubeAverageVec_coordinateVectorField_of_ne {d : ℕ} (Q : TriadicCube d) {i j : Fin d} (hji : j ≠ i) (g : Vec d → ℝ) : cubeAverageVec Q (coordinateVectorField i g) j = 0

theorem HCPolySupport.cubeFluctuationVec_coordinateVectorField {d : ℕ} (Q : TriadicCube d) (i : Fin d) (g : Vec d → ℝ) : cubeFluctuationVec Q (coordinateVectorField i g) = coordinateVectorField i (cubeFluctuation Q g)

theorem HCPolySupport.norm_coordinateVectorField_apply {d : ℕ} (i : Fin d) (g : Vec d → ℝ) (x : Vec d) : ‖coordinateVectorField i g x‖ = ‖g x‖

theorem HCPolySupport.sq_cubeLpNorm_two_coordinateVectorField {d : ℕ} (Q : TriadicCube d) (i : Fin d) (g : Vec d → ℝ) : cubeLpNorm Q 2 (coordinateVectorField i g) ^ 2 = cubeLpNorm Q 2 g ^ 2

theorem HCPolySupport.cubeBesovPositiveVectorDepthAverage_coordinateVectorField {d : ℕ} (Q : TriadicCube d) (i : Fin d) (g : Vec d → ℝ) (j : ℕ) : cubeBesovPositiveVectorDepthAverage Q (coordinateVectorField i g) j = cubeBesovDepthAverage Q 2 g j

theorem HCPolySupport.cubeBesovPositiveVectorDepthSeminorm_coordinateVectorField {d : ℕ} (Q : TriadicCube d) (s : ℝ) (i : Fin d) (g : Vec d → ℝ) (j : ℕ) : cubeBesovPositiveVectorDepthSeminorm Q s (coordinateVectorField i g) j = cubeBesovScaleWeight (-s) Q * cubeBesovDepthSeminorm Q s 2 g j

theorem HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo_coordinateVectorField {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (i : Fin d) (g : Vec d → ℝ) : cubeBesovPositiveVectorPartialSeminormTwo Q s N (coordinateVectorField i g) = cubeBesovScaleWeight (-s) Q * cubeBesovPartialSeminorm Q s 2 2 N g

theorem HCPolySupport.cubeBesovPartialSeminorm_two_two_le_dualTestNorm_two_two {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (g : Vec d → ℝ) : cubeBesovPartialSeminorm Q s 2 2 N g ≤ cubeBesovDualTestNorm Q s 2 2 N g

theorem HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo_coordinateVectorField_le_scaleWeight_neg {d : ℕ} (Q : TriadicCube d) {s : ℝ} (N : ℕ) (i : Fin d) (g : Vec d → ℝ) (hg : CubeBesovDualFullTest Q s 2 2 g) : cubeBesovPositiveVectorPartialSeminormTwo Q s N (coordinateVectorField i g) ≤ cubeBesovScaleWeight (-s) Q

theorem HCPolySupport.sqrt_vecNormSq_cubeAverageVec_coordinateVectorField {d : ℕ} (Q : TriadicCube d) (i : Fin d) (g : Vec d → ℝ) : √(vecNormSq (cubeAverageVec Q (coordinateVectorField i g))) = ‖cubeAverage Q g‖

theorem HCPolySupport.norm_cubeAverage_le_scaleWeight_neg_of_cubeBesovDualFullTest_two_two {d : ℕ} (Q : TriadicCube d) {s : ℝ} (g : Vec d → ℝ) (hg : CubeBesovDualFullTest Q s 2 2 g) : ‖cubeAverage Q g‖ ≤ cubeBesovScaleWeight (-s) Q

def HCPolySupport.UnitFullDualCoordinateStandardBridge (d : ℕ) (C : ℝ) : Prop

Standard, non-overlapping version of the coordinate full-dual bridge.

Equations

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

theorem HCPolySupport.unitFullDualCoordinateStandardBridge (d : ℕ) : UnitFullDualCoordinateStandardBridge d 2

def HCPolySupport.UnitFullDualCoordinateOverlappingBridgeSharpLoss (d : ℕ) (C : ℝ) : Prop

Low-exponent coordinate bridge with the sharp-boundary loss displayed in the RHS. It is only required for s < 1/2, exactly the summability range of the sharp boundary kernel.

Equations

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

theorem HCPolySupport.unitFullDualCoordinateOverlappingBridge_sharpBoundaryKernel {d : ℕ} [NeZero d] (Q : TriadicCube d) {s : ℝ} (i : Fin d) (g : Vec d → ℝ) (hs : 0 < s) (hs_lt_half : s < 1 / 2) (hg : CubeBesovDualFullTest Q s 2 2 g) (hmem : SharpBoundaryProjectionMemLp Q (coordinateVectorField i g)) : CubeVectorOverlappingBesovHRegularity Q s (coordinateVectorField i g) ∧ cubeBesovOverlappingPositiveVectorNormTwo Q s (coordinateVectorField i g) ≤ 2 * (1 + √(sharpBoundaryKernelLoss d s)) * cubeBesovScaleWeight (-s) Q

Low-exponent coordinate bridge supplied by the sharp-boundary comparison.

This is the honest replacement for the old uniform all-exponents overlap bridge: it works for s < 1/2, carries the explicit sharp-boundary loss, and keeps the overlap-cube MemLp closure package as an input.

theorem HCPolySupport.sharpBoundaryProjectionMemLp_coordinateVectorField_of_cubeBesovDualFullTest_two_two {d : ℕ} {Q : TriadicCube d} {s : ℝ} (i : Fin d) (g : Vec d → ℝ) (hg : CubeBesovDualFullTest Q s 2 2 g) : SharpBoundaryProjectionMemLp Q (coordinateVectorField i g)

Coordinate full-dual tests satisfy the MemLp closure package needed by the sharp-boundary standard-to-overlap comparison.

theorem HCPolySupport.UnitFullDualCoordinateOverlappingBridgeSharpLoss.of_sharpBoundaryMemLp {d : ℕ} [NeZero d] (hmem : ∀ (Q : TriadicCube d) {s : ℝ} (i : Fin d) (g : Vec d → ℝ), 0 < s → s < 1 / 2 → CubeBesovDualFullTest Q s 2 2 g → SharpBoundaryProjectionMemLp Q (coordinateVectorField i g)) : UnitFullDualCoordinateOverlappingBridgeSharpLoss d 2

The sharp-boundary coordinate bridge follows once the overlap-cube MemLp closure package is available for coordinate full-dual tests.

theorem HCPolySupport.unitFullDualCoordinateOverlappingBridgeSharpLoss (d : ℕ) [NeZero d] : UnitFullDualCoordinateOverlappingBridgeSharpLoss d 2

Closed sharp-boundary coordinate full-dual bridge.