Coarse-graining support:

Support.Sobolev.Fractional.ContinuousInterpolation.OverlapCoordinateBridge

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

Coordinate bridges for the overlapping positive Besov seminorm

The scalar fractional-Sobolev comparison and the vector discrete K-functional use two historically duplicated presentations of the same overlap geometry. This file identifies those presentations and compares their finite p = q = 2 truncations. No full real-valued sSup seminorm occurs here.

theorem HCPolySupport.ScalarOverlap.scaleFactor_eq_overlapCubeScaleFactor {d : ℕ} (S : TriadicCube d) : scaleFactor S = overlapCubeScaleFactor S

The duplicated overlap side-length definitions agree.

theorem HCPolySupport.ScalarOverlap.cubeSet_eq_overlapCubeSet {d : ℕ} (S : TriadicCube d) : cubeSet S = overlapCubeSet S

The duplicated half-open overlap cubes agree.

theorem HCPolySupport.ScalarOverlap.openCubeSet_eq_openOverlapCubeSet {d : ℕ} (S : TriadicCube d) : openCubeSet S = openOverlapCubeSet S

The duplicated open overlap cubes agree.

theorem HCPolySupport.ScalarOverlap.cubeVolume_eq_overlapCubeVolume {d : ℕ} (S : TriadicCube d) : cubeVolume S = overlapCubeVolume S

The duplicated overlap-volume definitions agree.

theorem HCPolySupport.ScalarOverlap.cubeMeasure_eq_overlapCubeMeasure {d : ℕ} (S : TriadicCube d) : cubeMeasure S = overlapCubeMeasure S

The duplicated unnormalized overlap measures agree.

theorem HCPolySupport.ScalarOverlap.normalizedCubeMeasure_eq_normalizedOverlapCubeMeasure {d : ℕ} (S : TriadicCube d) : normalizedCubeMeasure S = normalizedOverlapCubeMeasure S

The duplicated normalized overlap measures agree.

theorem HCPolySupport.ScalarOverlap.centersAtDepth_eq_overlapCentersAtDepth {d : ℕ} (Q : TriadicCube d) (j : ℕ) : centersAtDepth Q j = overlapCentersAtDepth Q j

The duplicated finite sets of overlap centers agree at every depth.

theorem HCPolySupport.ScalarOverlap.centersAverage_eq_overlapCentersAverage {d : ℕ} (Q : TriadicCube d) (j : ℕ) (f : TriadicCube d → ℝ) : centersAverage Q j f = overlapCentersAverage Q j f

The duplicated finite-center averages agree.

theorem HCPolySupport.ScalarOverlap.cubeAverage_eq_overlapCubeAverage {d : ℕ} (S : TriadicCube d) (f : Vec d → ℝ) : cubeAverage S f = overlapCubeAverage S f

The duplicated scalar overlap averages agree.

theorem HCPolySupport.ScalarOverlap.cubeAverageVec_eq_overlapCubeAverageVec {d : ℕ} (S : TriadicCube d) (F : Vec d → Vec d) : cubeAverageVec S F = overlapCubeAverageVec S F

The duplicated vector overlap averages agree.

theorem HCPolySupport.ScalarOverlap.cubeLpNorm_eq_overlapCubeLpNorm {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (S : TriadicCube d) (p : ENNReal) (f : Vec d → E) : cubeLpNorm S p f = overlapCubeLpNorm S p f

The duplicated normalized overlap L^p norms agree.

theorem HCPolySupport.cubeBesovOverlapOscillation_two_coordinate_eq_overlapCubeLpNorm {d : ℕ} (S : TriadicCube d) (F : Vec d → Vec d) (i : Fin d) : (cubeBesovOverlapOscillation S 2 fun (x : Vec d) => F x i) = overlapCubeLpNorm S 2 fun (x : Vec d) => overlapCubeFluctuationVec S F x i

A coordinate of the vector overlap fluctuation is the scalar overlap fluctuation used by cubeBesovOverlapOscillation.

theorem HCPolySupport.cubeBesovOverlapOscillation_two_coordinate_le_vector {d : ℕ} (S : TriadicCube d) (F : Vec d → Vec d) (i : Fin d) (hF : MeasureTheory.MemLp F 2 (normalizedOverlapCubeMeasure S)) : (cubeBesovOverlapOscillation S 2 fun (x : Vec d) => F x i) ≤ overlapCubeLpNorm S 2 (overlapCubeFluctuationVec S F)

Each scalar coordinate oscillation is bounded by the corrected vector oscillation on the same overlap cube.

theorem HCPolySupport.overlapCubeLpNorm_fluctuationVec_le_sum_cubeBesovOverlapOscillation_two {d : ℕ} (S : TriadicCube d) (F : Vec d → Vec d) (hF : MeasureTheory.MemLp F 2 (normalizedOverlapCubeMeasure S)) : overlapCubeLpNorm S 2 (overlapCubeFluctuationVec S F) ≤ ∑ i : Fin d, cubeBesovOverlapOscillation S 2 fun (x : Vec d) => F x i

The corrected vector oscillation is bounded by the sum of its scalar coordinate oscillations on the same overlap cube.

theorem HCPolySupport.cubeBesovOverlapDepthWeight_eq_scaleWeight_mul_rpow {d : ℕ} (Q : TriadicCube d) (s : ℝ) (j : ℕ) : cubeBesovOverlapDepthWeight Q s j = cubeBesovScaleWeight s Q * Real.rpow 3 (s * ↑j)

The legacy overlap depth weight is the root-scale factor times the corrected vector depth weight.

theorem HCPolySupport.cubeBesovOverlapDepthAverage_two_coordinate_le_vector {d : ℕ} (Q : TriadicCube d) (F : Vec d → Vec d) (i : Fin d) (j : ℕ) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) : cubeBesovOverlapDepthAverage Q 2 (fun (x : Vec d) => F x i) j ≤ cubeBesovOverlappingPositiveVectorDepthAverage Q F j

A scalar coordinate depth average is bounded by the corrected vector depth average.

theorem HCPolySupport.sqrt_cubeBesovOverlappingPositiveVectorDepthAverage_le_sum_coordinates {d : ℕ} (Q : TriadicCube d) (F : Vec d → Vec d) (j : ℕ) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) : √(cubeBesovOverlappingPositiveVectorDepthAverage Q F j) ≤ ∑ i : Fin d, √(cubeBesovOverlapDepthAverage Q 2 (fun (x : Vec d) => F x i) j)

The square root of the corrected vector depth average is bounded by the sum of the square roots of the scalar coordinate depth averages.

theorem HCPolySupport.cubeBesovOverlapDepthSeminorm_two_coordinate_le_vector {d : ℕ} (Q : TriadicCube d) (s : ℝ) (F : Vec d → Vec d) (i : Fin d) (j : ℕ) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) : cubeBesovOverlapDepthSeminorm Q s 2 (fun (x : Vec d) => F x i) j ≤ cubeBesovScaleWeight s Q * cubeBesovOverlappingPositiveVectorDepthSeminorm Q s F j

A scalar coordinate depth seminorm is bounded by the root-scale factor times the corrected vector depth seminorm.

theorem HCPolySupport.scaleWeight_mul_vectorDepthSeminorm_le_sum_coordinates {d : ℕ} (Q : TriadicCube d) (s : ℝ) (F : Vec d → Vec d) (j : ℕ) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) : cubeBesovScaleWeight s Q * cubeBesovOverlappingPositiveVectorDepthSeminorm Q s F j ≤ ∑ i : Fin d, cubeBesovOverlapDepthSeminorm Q s 2 (fun (x : Vec d) => F x i) j

After inserting the root-scale factor, the corrected vector depth seminorm is bounded by the sum of the scalar coordinate depth seminorms.

theorem HCPolySupport.cubeBesovOverlapPartialSeminorm_two_two_eq_sqrt_sum_sq {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (f : Vec d → ℝ) : cubeBesovOverlapPartialSeminorm Q s 2 2 N f = √(∑ j ∈ Finset.range (N + 1), cubeBesovOverlapDepthSeminorm Q s 2 f j ^ 2)

The scalar finite p = q = 2 overlap seminorm is the square root of the sum of its squared depth terms.

theorem HCPolySupport.cubeBesovOverlapPartialSeminorm_two_coordinate_le_vector {d : ℕ} (Q : TriadicCube d) (s : ℝ) (F : Vec d → Vec d) (i : Fin d) (N : ℕ) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) : (cubeBesovOverlapPartialSeminorm Q s 2 2 N fun (x : Vec d) => F x i) ≤ cubeBesovScaleWeight s Q * cubeBesovOverlappingPositiveVectorPartialSeminormTwo Q s N F

A scalar coordinate finite truncation is bounded by the root-scale factor times the corrected vector finite truncation.

theorem HCPolySupport.scaleWeight_mul_vectorPartialSeminorm_le_sum_coordinates {d : ℕ} (Q : TriadicCube d) (s : ℝ) (F : Vec d → Vec d) (N : ℕ) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) : cubeBesovScaleWeight s Q * cubeBesovOverlappingPositiveVectorPartialSeminormTwo Q s N F ≤ ∑ i : Fin d, cubeBesovOverlapPartialSeminorm Q s 2 2 N fun (x : Vec d) => F x i

After inserting the root-scale factor, the corrected vector finite truncation is bounded by the sum of the scalar coordinate finite truncations. This is uniform in the truncation depth.

theorem HCPolySupport.sqrt_sum_sq_coordinatePartialSeminorm_le_sqrt_dim_mul_vector {d : ℕ} (Q : TriadicCube d) (s : ℝ) (F : Vec d → Vec d) (N : ℕ) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) : √(∑ i : Fin d, (cubeBesovOverlapPartialSeminorm Q s 2 2 N fun (x : Vec d) => F x i) ^ 2) ≤ √↑d * (cubeBesovScaleWeight s Q * cubeBesovOverlappingPositiveVectorPartialSeminormTwo Q s N F)

The Euclidean aggregate of the scalar coordinate finite truncations is controlled by the corrected vector truncation with the explicit factor sqrt d.