HarmonicReplacement #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Harmonic replacement on Euclidean balls #
This is the Dirichlet comparison used in the small-contrast Schauder estimate. The local Section 4 Dirichlet solver is reused; only the ball-specific package and its retained zero-trace witness are adapted here.
theorem
Algsuperdiff.StochasticProcess.Common.Regularity.Ported.isOpenBoundedConvexDomain_euclideanBall
{d : ℕ}
(z : HCPolySupport.Vec d)
{r : ℝ}
(hr : 0 < r)
:
Explicit Euclidean balls are open bounded convex domains.
theorem
Algsuperdiff.StochasticProcess.Common.Regularity.Ported.exists_unitHarmonicReplacement_withGradient
{d : ℕ}
[NeZero d]
{V : Set (HCPolySupport.Vec d)}
(hV : HCPolySupport.IsOpenBoundedConvexDomain V)
(hne : V.Nonempty)
(Phi : HCPolySupport.H1Function V)
:
∃ (h : HCPolySupport.H1Function V) (rho : HCPolySupport.H10Function V),
IsUnitWeaklyHarmonicOn V h ∧ (∀ (x : HCPolySupport.Vec d), h.toFun x = Phi.toFun x + rho.toFun x) ∧ ∀ (x : HCPolySupport.Vec d), h.grad x = Phi.grad x + rho.grad x
A weakly harmonic replacement with its concrete zero-trace witness and pointwise gradient identity.
theorem
Algsuperdiff.StochasticProcess.Common.Regularity.Ported.exists_unitHarmonicReplacement_euclideanBall
{d : ℕ}
[NeZero d]
(z : HCPolySupport.Vec d)
{r : ℝ}
(hr : 0 < r)
(u : HCPolySupport.H1Function (HCPolySupport.euclideanBall z r))
:
∃ (h : HCPolySupport.H1Function (HCPolySupport.euclideanBall z r)) (rho :
HCPolySupport.H10Function (HCPolySupport.euclideanBall z r)),
IsUnitWeaklyHarmonicOn (HCPolySupport.euclideanBall z r) h ∧ (∀ (x : HCPolySupport.Vec d), h.toFun x = u.toFun x + rho.toFun x) ∧ (∀ (x : HCPolySupport.Vec d), h.grad x = u.grad x + rho.grad x) ∧ ∫ (x : HCPolySupport.Vec d) in HCPolySupport.euclideanBall z r, HCPolySupport.vecDot (h.grad x) (h.grad x) ≤ ∫ (x : HCPolySupport.Vec d) in HCPolySupport.euclideanBall z r, HCPolySupport.vecDot (u.grad x) (u.grad x)
Harmonic replacement on a Euclidean ball, including the exact Dirichlet energy comparison with the datum.