Coarse-graining support: Support.Sobolev.Foundations.CubeCalderonZygmund.AxisCubeHarmonicGain

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

Axis-cube transport of the harmonic gradient gain

This file consumes the Euclidean harmonic gain on the centered unit triadic cube and transports it to an arbitrary positive axis cube. The coordinate to Hilbert-vector comparison is kept here, so callers supply only harmonicity.

theorem HCPolySupport.CubeCalderonZygmund.axisCube_harmonicEuclideanGradientGain_coefficient_ne_top {d : ℕ} {r : FiniteLpExponent} {depth : ℕ} (G : INTERNAL.HarmonicEuclideanGradientGain d r depth) : G.constantValue * ↑d ≠ ⊤

The explicit finite-dimensional loss in the axis-cube transport remains finite whenever the centered-cube gain constant is finite.

theorem HCPolySupport.CubeCalderonZygmund.axisCube_harmonicEuclideanGradientGain {d : ℕ} {r : FiniteLpExponent} {depth : ℕ} (G : INTERNAL.HarmonicEuclideanGradientGain d r depth) (z : Vec d) (L : ℝ) (hL : 0 < L) (u : H1Function (axisCube z L)) (hu : WeakPoissonEquationOn (axisCube z L) u 0) : MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (u.grad x)) r.exponent (axisCubeNormalizedMeasure (axisCubeConcentricDepthCorner z L depth) (axisCubeConcentricDepthSide L depth)) ∧ MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertVec.ofVec (u.grad x)) r.exponent (axisCubeNormalizedMeasure (axisCubeConcentricDepthCorner z L depth) (axisCubeConcentricDepthSide L depth)) ≤ G.constantValue * ↑d * MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertVec.ofVec (u.grad x)) 2 (axisCubeNormalizedMeasure z L)

The fixed-depth Euclidean harmonic-gradient gain transported to an arbitrary positive axis cube. The right side is its parent normalized Hilbert-vector L² norm; the extra explicit factor is only the finite coordinate count.