Documentation

LeanPool.HighContrastHomogenization.Support.Besov.Positive.ExactOverlapEuclideanLpCoordinateBridge

Coarse-graining support: Support.Besov.Positive.ExactOverlapEuclideanLpCoordinateBridge #

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

Coordinate bridge for the finite-p Euclidean overlap oscillation #

The canonical finite-p Euclidean overlap seminorm is defined directly from the Hilbert realization of its vector fluctuation. This file records the local, exact coordinate identification with the scalar overlap fluctuation and the one-coordinate L^p bound. It deliberately contains no aggregation over coordinates, centers, or depths.

source
theorem HCPolySupport.ScalarOverlap.cubeAverageVec_apply_eq_cubeAverage {d : ℕ} (S : TriadicCube d) (F : Vec d → Vec d) (i : Fin d) :
cubeAverageVec S F i = cubeAverage S fun (x : Vec d) => F x i

A coordinate of the vector overlap average is exactly the scalar overlap average of that coordinate.

source
theorem HCPolySupport.euclideanOverlapResidual_coordinate_eq_scalar {d : ℕ} (S : TriadicCube d) (F : Vec d → Vec d) (i : Fin d) :
(fun (x : Vec d) => (F x - ScalarOverlap.cubeAverageVec S F) i) = fun (x : Vec d) => F x i - ScalarOverlap.cubeAverage S fun (y : Vec d) => F y i

The coordinate of the canonical Euclidean overlap residual is the scalar overlap residual of the same coordinate.

source
theorem HCPolySupport.scalarOverlap_eLpNorm_eq_coordinate_euclideanOverlapResidual {d : ℕ} (S : TriadicCube d) (p : FiniteLpExponent) (F : Vec d → Vec d) (i : Fin d) :
MeasureTheory.eLpNorm (fun (x : Vec d) => F x i - ScalarOverlap.cubeAverage S fun (y : Vec d) => F y i) p.exponent (ScalarOverlap.normalizedCubeMeasure S) = MeasureTheory.eLpNorm (fun (x : Vec d) => (F x - ScalarOverlap.cubeAverageVec S F) i) p.exponent (ScalarOverlap.normalizedCubeMeasure S)

The scalar overlap oscillation written using its scalar average is exactly the corresponding coordinate of the canonical Euclidean overlap residual.

source
theorem HCPolySupport.cubeBesovOverlapOscillation_coordinate_eq_residual_toReal {d : ℕ} (S : TriadicCube d) (p : FiniteLpExponent) (F : Vec d → Vec d) (i : Fin d) :
(cubeBesovOverlapOscillation S p.exponent fun (x : Vec d) => F x i) = (MeasureTheory.eLpNorm (fun (x : Vec d) => (F x - ScalarOverlap.cubeAverageVec S F) i) p.exponent (ScalarOverlap.normalizedCubeMeasure S)).toReal

The scalar overlap oscillation of a coordinate is the real value of the corresponding coordinate of the canonical Euclidean residual.

source
theorem HCPolySupport.scalarOverlap_eLpNorm_le_euclideanOverlap {d : ℕ} (S : TriadicCube d) (p : FiniteLpExponent) (F : Vec d → Vec d) (i : Fin d) :
MeasureTheory.eLpNorm (fun (x : Vec d) => F x i - ScalarOverlap.cubeAverage S fun (y : Vec d) => F y i) p.exponent (ScalarOverlap.normalizedCubeMeasure S) ≤ MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertVec.ofVec (F x - ScalarOverlap.cubeAverageVec S F)) p.exponent (ScalarOverlap.normalizedCubeMeasure S)

One scalar coordinate of the overlap oscillation is bounded by the direct Euclidean Hilbert overlap oscillation on the same cube.