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

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

One-dimensional harmonic gradient gain

In one dimension, the fixed-radius weak Hessian of a weakly harmonic function vanishes. Thus its only gradient coordinate is constant almost everywhere on the central triadic child. This supplies every finite normalized L^r gain without an endpoint Sobolev embedding.

theorem HCPolySupport.CubeCalderonZygmund.harmonic_gradCoord_memLp_centralDescendant_oneDim (p : FiniteLpExponent) (Q : TriadicCube 1) (u : H1Function (openCubeSet Q)) (h : WeakPoissonEquationOn (openCubeSet Q) u fun (x : Vec 1) => 0) : MeasureTheory.MemLp (fun (x : Vec 1) => u.grad x 0) p.exponent (normalizedCubeMeasure (centralDescendant Q 1))

The one-dimensional constant-gradient construction supplies actual finite L^p membership on the central child, not merely a real-valued norm bound. This is the finiteness witness required by the later ENNReal CZ carrier.

theorem HCPolySupport.CubeCalderonZygmund.exists_harmonic_gradCoord_finiteLp_bound_oneDim (p : FiniteLpExponent) : ∃ (C : ℝ), 0 < C ∧ ∀ (Q : TriadicCube 1) (u : H1Function (openCubeSet Q)), (WeakPoissonEquationOn (openCubeSet Q) u fun (x : Vec 1) => 0) → (cubeLpNorm { scale := Q.scale - 1, index := fun (i : Fin 1) => 3 * Q.index i } p.exponent fun (x : Vec 1) => u.grad x 0) ≤ C * cubeLpNorm Q 2 fun (x : Vec 1) => u.grad x 0

In one dimension a weakly harmonic gradient has every finite normalized L^r gain on the central child. The displayed proof uses the universal constant 3; in particular it is uniform in the exponent and cube scale.