DirichletSolvability #

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

Solvability of the localized Dirichlet problems, and uniqueness up to null sets #

Section 5 names two solutions on y + □_n: the solution u_m of -∇·a_m∇u = ∇·g for the cutoff coefficient field at scale m, and the comparator v solving -σ_n Δ v = ∇·g. Naming them presupposes that they exist, and using them in a supremum presupposes that the family they range over is nonempty. This module supplies both existence statements on the translated carrier, and the uniqueness that holds at this level of regularity: two solutions of the same problem agree away from a null set.

Pointwise uniqueness is a statement about a continuous representative, not about the H¹ witnesses; it belongs to the representative theory and is not proved here.

Main results #

exists_isDirichletSolutionAt_comparator — the comparator exists for every 1/2-Hölder forcing field.
exists_isDirichletSolutionAt_cutoff — the rough-field solution exists for every 1/2-Hölder forcing field, at every scale m and every sample.
isDirichletSolutionAt_ae_unique — two solutions of the same problem, for a coefficient field that is elliptic on the cube, have gradients and values that agree almost everywhere on the cube.

The ellipticity hypothesis of the uniqueness statement #

isDirichletSolutionAt_ae_unique carries IsEllipticFieldOn lam Lam on the cube. This is a genuine premise, not a convenience: for a degenerate coefficient field the Dirichlet problem has many solutions, so no hypothesis-free uniqueness statement is true. Both families used by Section 5 satisfy it — the comparator with lam = Lam = σ_n, the cutoff field with lam = ν — and the two hypothesis-free specializations isDirichletSolutionAt_ae_unique_comparator and isDirichletSolutionAt_ae_unique_cutoff are recorded below.

References #

ABK26, the localized Dirichlet problems of Section 5.1.

1. Moving a solution from `□_n` back to `y + □_n` #

source

theorem Algsuperdiff.Section5.Support.h1Function_ext {d : ℕ} {U : Set (HCPolySupport.Vec d)} {u v : HCPolySupport.H1Function U} :

u.toFun = v.toFun → u.grad = v.grad → u = v

Two H¹ witnesses with the same value and gradient are equal: the remaining fields are propositions.

source

noncomputable def Algsuperdiff.Section5.Support.translateSolution {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) (v : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d n))) :

HCPolySupport.H1Function (cubeSetAt y n)

An H¹ witness on □_n, read on y + □_n as x ↦ v(x - y).

Equations

Algsuperdiff.Section5.Support.translateSolution y n v = Algsuperdiff.Section5.Support.castH1 ⋯ (v.translate y)

Instances For

source

@[simp]

theorem Algsuperdiff.Section5.Support.originPullback_translateSolution {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) (v : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d n))) :

originPullback y n (translateSolution y n v) = v

2. Hölder data on the translated cube #

source

theorem Algsuperdiff.Section5.Support.holderSeminormBoundOn_originCube_of_cubeSetAt {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] {y : HCPolySupport.Vec d} {n : ℤ} {alpha K : ℝ} {f : HCPolySupport.Vec d → E} (hf : Section4.Support.HolderSeminormBoundOn (cubeSetAt y n) alpha K f) :

Section4.Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) alpha K fun (x : HCPolySupport.Vec d) => f (y + x)

The C^{0,α} bound transports to the origin cube.

source

theorem Algsuperdiff.Section5.Support.holderSeminormBoundOn_nonneg_cubeSetAt {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] {y : HCPolySupport.Vec d} {n : ℤ} {alpha K : ℝ} {f : HCPolySupport.Vec d → E} (hd : 0 < d) (hf : Section4.Support.HolderSeminormBoundOn (cubeSetAt y n) alpha K f) :

0 ≤ K

On the translated cube in dimension d ≥ 1, a Hölder bound forces its constant to be nonnegative.

source

theorem Algsuperdiff.Section5.Support.memVectorL2_of_holderSeminormBoundOn_cubeSetAt {d : ℕ} {y : HCPolySupport.Vec d} {n : ℤ} {alpha K : ℝ} {f : HCPolySupport.Vec d → HCPolySupport.Vec d} (hK : 0 ≤ K) (halpha : 0 < alpha) (hf : Section4.Support.HolderSeminormBoundOn (cubeSetAt y n) alpha K f) :

HCPolySupport.MemVectorL2 (cubeSetAt y n) f

A Hölder-continuous vector field on y + □_n is square integrable there.

3. Existence for the comparator #

source

theorem Algsuperdiff.Section5.Support.exists_isDirichletSolutionAt_comparator {d : ℕ} (M : Section3.ABKModel d) (n : ℤ) (y : HCPolySupport.Vec d) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} {Kg : ℝ} (hg : Section4.Support.HolderSeminormBoundOn (cubeSetAt y n) (1 / 2) Kg g) :

∃ (v : HCPolySupport.H1Function (cubeSetAt y n)), IsDirichletSolutionAt (fun (x : HCPolySupport.Vec d) => ↑(Section3.Annealed.sigmaBar M n) • 1) y n v g

The comparator exists. For every scale, centre and 1/2-Hölder forcing field the constant-coefficient Dirichlet problem -σ_n Δ v = ∇·g on y + □_n with zero boundary values has a solution.

4. Existence for the rough field #

source

theorem Algsuperdiff.Section5.Support.exists_cubeSetAt_subset_openCubeSet {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) :

∃ (ell : ℤ), cubeSetAt y n ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d ell)

Every translated cube is contained in a centred cube of a large enough scale.

source

theorem Algsuperdiff.Section5.Support.exists_isDirichletSolutionAt_cutoff {d : ℕ} (M : Section3.ABKModel d) (m n : ℤ) (y : HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} {Kg : ℝ} (hg : Section4.Support.HolderSeminormBoundOn (cubeSetAt y n) (1 / 2) Kg g) :

∃ (u : HCPolySupport.H1Function (cubeSetAt y n)), IsDirichletSolutionAt (Section3.Cutoff.coefficientCutoff M.nu m omega).toCoeffField y n u g

The rough-field solution exists. For every sample, every scale m, every cube y + □_n and every 1/2-Hölder forcing field the Dirichlet problem -∇·a_m∇u = ∇·g with zero boundary values has a solution.