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

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

Stability of finite-exponent cube divergence solutions

The supplied-solution cube Calderón--Zygmund estimate applies to the difference of two zero-trace solutions. This file packages that subtraction step, retaining the same exponent-only constant and the exact inverse coefficient scaling.

noncomputable def HCPolySupport.CubeCalderonZygmund.cubeEuclideanL2LpFieldSub {d : ℕ} {Q : TriadicCube d} {q : FiniteLpExponent} (h k : CubeEuclideanL2LpField Q q) : CubeEuclideanL2LpField Q q

Subtract two cube fields pointwise, retaining their Euclidean L^q and L² membership.

Equations

• HCPolySupport.CubeCalderonZygmund.cubeEuclideanL2LpFieldSub h k = { toField := fun (x : HCPolySupport.Vec d) => h.toField x - k.toField x, euclideanMemLp := ⋯, euclideanMemL2 := ⋯ }

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.centeredCubeH10ScalarDivergence_solution_stability (d : ℕ) [NeZero d] (q : FiniteLpExponent) : ∃ C < ⊤, ∀ (m : ℤ) (sigma0 : ℝ) (h k : CubeEuclideanL2LpField (originCube d m) q) (u v : H10Function (openCubeSet (originCube d m))), 0 < sigma0 → IsCenteredCubeH10ScalarDivergenceSolution m sigma0 u h.toLpTwo → IsCenteredCubeH10ScalarDivergenceSolution m sigma0 v k.toLpTwo → ((centeredCubeDomain d m).normalizedEuclideanLpENorm q.exponent fun (x : Vec d) => u.grad x - v.grad x) ≤ C * (ENNReal.ofReal sigma0)⁻¹ * (centeredCubeDomain d m).normalizedEuclideanLpENorm q.exponent fun (x : Vec d) => h.toField x - k.toField x

Two zero-trace scalar divergence solutions on the same centered cube are Lipschitz in their data in the normalized Euclidean L^q gradient norm. The constant is precisely the one supplied by centeredCubeH10ScalarDivergence_cz.