Dirichlet

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Section 4 deterministic carriers: Dirichlet problems, Hölder and fractional gauges

The definitional layer beneath the §4.3 anchors (l.harmonic.approximation.good.scales) and beneath the two roots' deterministic clauses (t.homogenization; t.regularity). Everything here is stated over the CoarseGraining carriers Vec d, H1Function, H10Function, CoeffField, TriadicCube; no Section 3 probabilistic object appears, and no estimate is proved.

The Dirichlet carrier (frozen-surface resolution A7)

The manuscript's

  -∇ · a ∇u = ∇ · g   in □_m ,        u = h  on ∂□_m

Sign convention. IsDivFormWeakSolutionOn renders -∇·a∇u = ∇·g in the standard distributional convention ⟪∇·g, φ⟫ = -∫ g·∇φ, i.e. with the minus sign on the right of the weak identity. CoarseGraining's Homogenization.IsZeroTraceDirichletRhsWeakSolution carries the same equation with the opposite convention for ∇·g (its weak identity has no minus sign), so the two predicates correspond at the negated forcing. The frozen §4.3 statement quantifies universally over the pair (u, g) and bounds the right side by seminorms of g, both invariant under g ↦ -g, so the statement itself does not depend on which of the two conventions is fixed.

The Hölder carrier

The p = ∞ fractional slots [g]_{W^{1/2,∞}} and ‖∇h‖_{W^{1/2,∞}} are carried at the Hölder seminorm C^{0,α} in explicit bound-predicate form, following ABK26 ("[·]_{C^{0,s}} and [·]_{W^{s,∞}} are equivalent up to dimensional constants on a cube; we use them interchangeably"). HolderSeminormBoundOn U α K f is the plain [f]_{C^{0,α}(U)} ≤ K bound.

The fractional carrier

[u]_{W^{s,p}(U)} is defined by one normalized integral,

  [u]_{W^{s,p}(U)} = ( ⨍_U ∫_U |u(x) - u(y)|^p / |x-y|^{d+sp} dx dy )^{1/p} ,

which is exactly CoarseGraining's Gagliardo.cubeGagliardoESeminorm when U is a triadic cube (normalized product measure in the first slot, plain restricted volume in the second). §4.3 needs the same object on the intersection windows (x+□_{n+1}) ∩ □_m, which are not triadic cubes, so the normalized measure is rebuilt here for an arbitrary set and the cube case is proved to agree with CoarseGraining's (normalizedGagliardo). CoarseGraining's unnormalized gagliardo uses the plain restricted volume in both slots and is therefore not the tex's object.

Metric convention. CoarseGraining's Gagliardo.gagliardoKernel measures `|x

• y|in the ambientVec dnorm, which is the supremum norm onFin d → ℝ, not the manuscript's Euclidean norm (CoarseGraining records this deviation in its own module docstring; the two differ by a factor at most d^{(d+sp)/2}on the kernel, absorbed in the dimensional constants). HolderSeminormBoundOnuses the same ambient norm, so the twop = ∞andp = 2` carriers of this file are stated in one metric.

Main definitions

• IsWeaklyHarmonicOn W v — ∫_W ∇v · ∇φ = 0 for all φ ∈ H¹₀(W).
• IsDivFormWeakSolutionOn a W u g — the divergence-form weak equation.
• HasZeroTraceDifferenceOn W u h — u - h ∈ H¹₀(W), with witness.
• IsDirichletSolutionOn a Q u h g — the A7 rendering of the tex's problem.
• HolderSeminormBoundOn U α K f, MemHolder U α f — the C^{0,α} carriers.
• normalizedGagliardo A s f — the tex's [f]_{H^s(A)} on an arbitrary finite-volume set.

References

• ABK26, l.harmonic.approximation.good.scales.
• ABK26, the function-space conventions and the fractional Sobolev seminorm.

1. Weak harmonicity

def Algsuperdiff.Section4.Support.IsWeaklyHarmonicOn {d : ℕ} (W : Set (HCPolySupport.Vec d)) (v : HCPolySupport.H1Function W) : Prop

Weak harmonicity of an H¹ function on W: the first variation of the Dirichlet energy vanishes against every zero-trace test function, ∫_W ∇v · ∇φ = 0 for all φ ∈ H¹₀(W).

This is -Δ v = 0 in W in the variational sense — the interior half of the tex's Dirichlet problem e.harmonic.approx.v.def.

Equations

• Algsuperdiff.Section4.Support.IsWeaklyHarmonicOn W v = ∀ (φ : HCPolySupport.H10Function W), ∫ (x : HCPolySupport.Vec d) in W, HCPolySupport.vecDot (v.grad x) (φ.grad x) = 0

2. Divergence-form weak solutions and the Dirichlet carrier

def Algsuperdiff.Section4.Support.IsDivFormWeakSolutionOn {d : ℕ} (a : HCPolySupport.CoeffField d) (W : Set (HCPolySupport.Vec d)) (u : HCPolySupport.H1Function W) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) : Prop

The divergence-form weak equation -∇ · a ∇u = ∇ · g on W, tested against H¹₀(W):

∫_W (a ∇u) · ∇φ = - ∫_W g · ∇φ for all φ ∈ H¹₀(W).

The minus sign is the standard distributional convention ⟪∇·g, φ⟫ = -∫ g·∇φ; see the module docstring for the correspondence with CoarseGraining's IsZeroTraceDirichletRhsWeakSolution, which fixes the opposite convention.

Equations

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

theorem Algsuperdiff.Section4.Support.isDivFormWeakSolutionOn_def {d : ℕ} {a : HCPolySupport.CoeffField d} {W : Set (HCPolySupport.Vec d)} {u : HCPolySupport.H1Function W} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} : IsDivFormWeakSolutionOn a W u g ↔ ∀ (φ : HCPolySupport.H10Function W), ∫ (x : HCPolySupport.Vec d) in W, HCPolySupport.vecDot (HCPolySupport.matVecMul (a x) (u.grad x)) (φ.grad x) = -∫ (x : HCPolySupport.Vec d) in W, HCPolySupport.vecDot (g x) (φ.grad x)

def Algsuperdiff.Section4.Support.HasZeroTraceDifferenceOn {d : ℕ} (W : Set (HCPolySupport.Vec d)) (u h : HCPolySupport.H1Function W) : Prop

Two H¹ functions differ by a zero-trace H¹ function, including their gradients.

Equations

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

def Algsuperdiff.Section4.Support.IsDirichletSolutionOn {d : ℕ} (a : HCPolySupport.CoeffField d) (Q : HCPolySupport.TriadicCube d) (u h : HCPolySupport.H1Function (HCPolySupport.openCubeSet Q)) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) : Prop

The §4.3 Dirichlet problem:

  u ∈ H¹(□) ,   -∇ · a ∇u = ∇ · g  in □ ,   u = h  on ∂□ ,

read as: u - h is realized in H¹₀(□) and u satisfies the divergence-form weak equation against H¹₀(□) tests. □ is the open realization openCubeSet Q of the triadic cube, the domain on which CoarseGraining's analytic lemmas are stated.

Equations

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

theorem Algsuperdiff.Section4.Support.IsDirichletSolutionOn.hasZeroTraceDifferenceOn {d : ℕ} {a : HCPolySupport.CoeffField d} {Q : HCPolySupport.TriadicCube d} {u h : HCPolySupport.H1Function (HCPolySupport.openCubeSet Q)} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hu : IsDirichletSolutionOn a Q u h g) : HasZeroTraceDifferenceOn (HCPolySupport.openCubeSet Q) u h

theorem Algsuperdiff.Section4.Support.IsDirichletSolutionOn.isDivFormWeakSolutionOn {d : ℕ} {a : HCPolySupport.CoeffField d} {Q : HCPolySupport.TriadicCube d} {u h : HCPolySupport.H1Function (HCPolySupport.openCubeSet Q)} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hu : IsDirichletSolutionOn a Q u h g) : IsDivFormWeakSolutionOn a (HCPolySupport.openCubeSet Q) u g

The CoarseGraining compatibility anchor

theorem Algsuperdiff.Section4.Support.isZeroTraceDirichletRhsWeakSolution_iff_isDivFormWeakSolutionOn {d : ℕ} {a : HCPolySupport.CoeffField d} {W : Set (HCPolySupport.Vec d)} {u : HCPolySupport.H1Function W} {w : HCPolySupport.H10Function W} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hgrad : ∀ (x : HCPolySupport.Vec d), u.grad x = w.grad x) : (HCPolySupport.IsZeroTraceDirichletRhsWeakSolution a W w fun (x : HCPolySupport.Vec d) => -g x) ↔ IsDivFormWeakSolutionOn a W u g

Compatibility with the CoarseGraining Dirichlet surface.

If the gradient of u is the gradient of a zero-trace function w — in particular when u = h + w with h of vanishing gradient, the zero boundary datum — then the divergence-form weak equation for u at forcing g is exactly CoarseGraining's IsZeroTraceDirichletRhsWeakSolution for w at forcing -g.

The negation is the sign-convention correspondence recorded in the module docstring: CoarseGraining's predicate carries -∇·a∇u = ∇·g with the weak identity ∫ a∇u·∇φ = ∫ g·∇φ, this file with ∫ a∇u·∇φ = -∫ g·∇φ.

3. The Hölder carrier

def Algsuperdiff.Section4.Support.HolderSeminormBoundOn {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (U : Set (HCPolySupport.Vec d)) (alpha K : ℝ) (f : HCPolySupport.Vec d → E) : Prop

[f]_{C^{0,α}(U)} ≤ K in explicit bound-predicate form: |f(x) - f(y)| ≤ K |x - y|^α for all x, y ∈ U.

The volume/scale normalization of W^{α,∞} is not folded in and must be supplied by the consuming statement.

|·| is the ambient norm of Vec d, the supremum norm — the same metric CoarseGraining's Gagliardo.gagliardoKernel uses; the manuscript's Euclidean norm differs by a dimensional factor.

Equations

• Algsuperdiff.Section4.Support.HolderSeminormBoundOn U alpha K f = ∀ x ∈ U, ∀ y ∈ U, ‖f x - f y‖ ≤ K * ‖x - y‖ ^ alpha

theorem Algsuperdiff.Section4.Support.holderSeminormBoundOn_def {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] {U : Set (HCPolySupport.Vec d)} {alpha K : ℝ} {f : HCPolySupport.Vec d → E} : HolderSeminormBoundOn U alpha K f ↔ ∀ x ∈ U, ∀ y ∈ U, ‖f x - f y‖ ≤ K * ‖x - y‖ ^ alpha

theorem Algsuperdiff.Section4.Support.HolderSeminormBoundOn.continuousOn {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] {U : Set (HCPolySupport.Vec d)} {alpha K : ℝ} {f : HCPolySupport.Vec d → E} (hf : HolderSeminormBoundOn U alpha K f) (hK : 0 ≤ K) (halpha : 0 < alpha) : ContinuousOn f U

A positive-exponent Hölder bound implies continuity for any normed additive codomain.

theorem Algsuperdiff.Section4.Support.HolderSeminormBoundOn.mono_const {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] {U : Set (HCPolySupport.Vec d)} {alpha K K' : ℝ} {f : HCPolySupport.Vec d → E} (hf : HolderSeminormBoundOn U alpha K f) (hKK : K ≤ K') : HolderSeminormBoundOn U alpha K' f

The bound is monotone in the constant.

theorem Algsuperdiff.Section4.Support.HolderSeminormBoundOn.mono_set {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] {U V : Set (HCPolySupport.Vec d)} {alpha K : ℝ} {f : HCPolySupport.Vec d → E} (hf : HolderSeminormBoundOn U alpha K f) (hVU : V ⊆ U) : HolderSeminormBoundOn V alpha K f

The bound is monotone (decreasing) in the domain.

theorem Algsuperdiff.Section4.Support.HolderSeminormBoundOn.nonneg {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] {U : Set (HCPolySupport.Vec d)} {alpha K : ℝ} {f : HCPolySupport.Vec d → E} (hf : HolderSeminormBoundOn U alpha K f) {x y : HCPolySupport.Vec d} (hx : x ∈ U) (hy : y ∈ U) (hxy : x ≠ y) : 0 ≤ K

A Hölder bound holding at two distinct points of U forces the constant to be nonnegative.

theorem Algsuperdiff.Section4.Support.holderSeminormBoundOn_zero {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (U : Set (HCPolySupport.Vec d)) (alpha : ℝ) {K : ℝ} (hK : 0 ≤ K) : HolderSeminormBoundOn U alpha K fun (x : HCPolySupport.Vec d) => 0

The zero field satisfies every nonnegative Hölder bound.

4. The volume-normalized fractional (Gagliardo) gauge

noncomputable def Algsuperdiff.Section4.Support.normalizedVolumeMeasureOn {d : ℕ} (A : Set (HCPolySupport.Vec d)) : MeasureTheory.Measure (HCPolySupport.Vec d)

⨍_A, the volume-normalized restriction of Lebesgue measure to A. On a triadic cube this is CoarseGraining's normalizedCubeMeasure (normalizedVolumeMeasureOn_cubeSet).

Equations

• Algsuperdiff.Section4.Support.normalizedVolumeMeasureOn A = (MeasureTheory.volume A)⁻¹ • MeasureTheory.volume.restrict A

theorem Algsuperdiff.Section4.Support.normalizedVolumeMeasureOn_def {d : ℕ} (A : Set (HCPolySupport.Vec d)) : normalizedVolumeMeasureOn A = (MeasureTheory.volume A)⁻¹ • MeasureTheory.volume.restrict A

theorem Algsuperdiff.Section4.Support.normalizedVolumeMeasureOn_cubeSet {d : ℕ} (Q : HCPolySupport.TriadicCube d) : normalizedVolumeMeasureOn (HCPolySupport.cubeSet Q) = HCPolySupport.normalizedCubeMeasure Q

noncomputable def Algsuperdiff.Section4.Support.normalizedGagliardoMeasureOn {d : ℕ} (A : Set (HCPolySupport.Vec d)) : MeasureTheory.Measure (HCPolySupport.Vec d × HCPolySupport.Vec d)

The manuscript's ⨍_A ∫_A normalization as a product measure: normalized in the first variable, plain restricted volume in the second — CoarseGraining's Gagliardo.gagliardoCubeMeasure construction on an arbitrary set.

Equations

• Algsuperdiff.Section4.Support.normalizedGagliardoMeasureOn A = (Algsuperdiff.Section4.Support.normalizedVolumeMeasureOn A).prod (MeasureTheory.volume.restrict A)

theorem Algsuperdiff.Section4.Support.normalizedGagliardoMeasureOn_def {d : ℕ} (A : Set (HCPolySupport.Vec d)) : normalizedGagliardoMeasureOn A = (normalizedVolumeMeasureOn A).prod (MeasureTheory.volume.restrict A)

theorem Algsuperdiff.Section4.Support.normalizedGagliardoMeasureOn_cubeSet {d : ℕ} (Q : HCPolySupport.TriadicCube d) : normalizedGagliardoMeasureOn (HCPolySupport.cubeSet Q) = HCPolySupport.Gagliardo.gagliardoCubeMeasure Q

noncomputable def Algsuperdiff.Section4.Support.normalizedGagliardoESeminormOn {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (A : Set (HCPolySupport.Vec d)) (s : ℝ) (f : HCPolySupport.Vec d → E) : ENNReal

[f]_{H^s(A)}, the manuscript's volume-normalized fractional Sobolev seminorm at p = 2 on an arbitrary set A:

  [f]_{H^s(A)} = ( ⨍_A ∫_A |f(x) - f(y)|² / |x-y|^{d+2s} dx dy )^{1/2} ,

ℝ≥0∞-valued, with CoarseGraining's difference-quotient kernel.

The definition is generic in the target E, so the scalar leg ‖∇h‖_{H^s} (E := ℝ) and the vector leg [g]_{H^s} (E := Vec d, whose norm is the ambient supremum norm) are instances of one declaration.

Equations

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

theorem Algsuperdiff.Section4.Support.normalizedGagliardoESeminormOn_def {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (A : Set (HCPolySupport.Vec d)) (s : ℝ) (f : HCPolySupport.Vec d → E) : normalizedGagliardoESeminormOn A s f = MeasureTheory.eLpNorm (HCPolySupport.Gagliardo.gagliardoKernel s 2 f) 2 (normalizedGagliardoMeasureOn A)