Coarse-graining support:

Support.Sobolev.Foundations.CubeCalderonZygmund.ScalarPoissonGradientBelowTwo

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

Scalar Poisson gradient estimates below the energy exponent

This file proves the centered-cube L^q gradient estimate for a zero-trace solution of the scalar Poisson equation when 1 < q < 2. The proof uses self-adjoint duality against the already-established divergence-form Calderón--Zygmund estimate at the conjugate exponent.

Both functions in the mutual-testing step belong to H¹₀; no boundary trace of a gradient coordinate is asserted or used.

theorem HCPolySupport.CubeCalderonZygmund.ScalarPoissonGradientBelowTwo.centeredOpenCube_eq_smul_unitCenteredOpenCube {d : ℕ} (m : ℤ) : openCubeSet (originCube d m) = centeredCubeScale m • openCubeSet (originCube d 0)

noncomputable def HCPolySupport.CubeCalderonZygmund.ScalarPoissonGradientBelowTwo.centeredCubeH10Pullback {d : ℕ} {m : ℤ} (v : H10Function (openCubeSet (originCube d m))) : H10Function (openCubeSet (originCube d 0))

The normalized pullback of an H¹₀ function from a centered cube to the centered unit cube. Its gradient is the unscaled physical gradient.

Equations

• HCPolySupport.CubeCalderonZygmund.ScalarPoissonGradientBelowTwo.centeredCubeH10Pullback v = (HCPolySupport.centeredCubeScale m)⁻¹ • HCPolySupport.H10Function.unscale ⋯ (⋯ ▸ v)

theorem HCPolySupport.CubeCalderonZygmund.ScalarPoissonGradientBelowTwo.centeredCubeH10_value_eLpNorm_le_scale_mul_grad {d : ℕ} [NeZero d] (p : FiniteLpExponent) (Cp : ℝ) (hCp : 0 ≤ Cp) (hPoincare : ∀ (w : W10pFunction (openCubeSet (originCube d 0)) p.exponent), (MeasureTheory.eLpNorm w.toFun p.exponent (volumeMeasureOn (openCubeSet (originCube d 0)))).toReal ≤ Cp * ∑ i : Fin d, (MeasureTheory.eLpNorm (fun (x : Vec d) => w.grad x i) p.exponent (volumeMeasureOn (openCubeSet (originCube d 0)))).toReal) (m : ℤ) (v : H10Function (openCubeSet (originCube d m))) (hvgrad : MeasureTheory.MemLp (hilbertifyVecField v.grad) p.exponent (centeredCubeDomain d m).normalizedVolume) : MeasureTheory.eLpNorm v.toFun p.exponent (centeredCubeDomain d m).normalizedVolume ≤ ENNReal.ofReal (Cp * ↑d) * ENNReal.ofReal (centeredCubeScale m) * MeasureTheory.eLpNorm (hilbertifyVecField v.grad) p.exponent (centeredCubeDomain d m).normalizedVolume

Scale-correct normalized L^p Poincare control for an H¹₀ function on a centered cube, assuming the corresponding unit-cube W¹ᵖ₀ estimate.

noncomputable def HCPolySupport.CubeCalderonZygmund.ScalarPoissonGradientBelowTwo.radialTruncationL2LpField {d : ℕ} (m : ℤ) (q : FiniteLpExponent) (u : H10Function (openCubeSet (originCube d m))) (n : ℕ) : CubeEuclideanL2LpField (originCube d m) q.conjugate

Package radial truncation at level n of a zero-trace solution gradient as a cube field with Euclidean L² and L^{q.conjugate} membership.

Equations

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

theorem HCPolySupport.CubeCalderonZygmund.centeredCubeH10ScalarPoisson_gradient_cz_of_lt_two (d : ℕ) [NeZero d] (q : FiniteLpExponent) (hq : q.exponent.toReal < 2) : ∃ C < ⊤, ∀ (m : ℤ) (sigma0 : ℝ) (F : Vec d → ℝ) (u : H10Function (openCubeSet (originCube d m))), MeasureTheory.MemLp F 2 (centeredCubeDomain d m).normalizedVolume → MeasureTheory.MemLp F q.exponent (centeredCubeDomain d m).normalizedVolume → 0 < sigma0 → (∀ (phi : H10Function (openCubeSet (originCube d m))), sigma0 * ∫ (x : Vec d), vecDot (u.grad x) (phi.grad x) ∂(centeredCubeDomain d m).normalizedVolume = ∫ (x : Vec d), F x * phi.toFun x ∂(centeredCubeDomain d m).normalizedVolume) → (centeredCubeDomain d m).normalizedEuclideanLpENorm q.exponent u.grad ≤ C * ENNReal.ofReal (cubeScaleFactor (originCube d m)) * (ENNReal.ofReal sigma0)⁻¹ * MeasureTheory.eLpNorm F q.exponent (centeredCubeDomain d m).normalizedVolume

Below the energy exponent, a supplied zero-trace solution of the scalar Poisson equation on a centered cube has the scale-correct normalized L^q gradient bound. The source is represented directly by a scalar field with separate normalized L² and L^q membership.