FieldSolutionMap

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

The solution as a function of a continuous coefficient field on the closed cube

The measurability of the localized quantities factors the sample out of the solution: the sample enters only through the continuous matrix field a_m(ω) restricted to the closed cube, and the solution depends on that field alone. This module builds the parameter space and the solution map on it.

The parameter space is the set of continuous matrix fields on closedCubeAt y n whose symmetric part is ν I. It is closed, hence measurable — the skew-symmetry of the shells makes this the exact condition the cutoff coefficient satisfies — and on a compact carrier every such field is bounded, so each of them is elliptic on the cube with a lower constant ν and an upper constant of its own. No ellipticity constant is fixed across the parameter space, and no fallback branch is used: the field off the closed cube is the value at the coordinatewise retraction, which is the identity on the cube.

Main definitions

• extendCoeff y n A — the coefficient field of a continuous matrix field on the closed cube.
• ellipticCube nu y n — the parameter space.
• solutionOfField — the solution attached to a parameter.

References

• ABK26, the localized Dirichlet problems of Section 5.1.

1. The coefficient field of a continuous matrix field

noncomputable def Algsuperdiff.Section5.Support.extendCoeff {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) (A : C(↑(closedCubeAt y n), HCPolySupport.Mat d)) : HCPolySupport.CoeffField d

The coefficient field determined by a continuous matrix field on the closed cube: off the cube it is the value at the coordinatewise retraction.

Equations

• Algsuperdiff.Section5.Support.extendCoeff y n A x = A ⟨Algsuperdiff.Section5.Support.clampTo y n x, ⋯⟩

theorem Algsuperdiff.Section5.Support.continuous_extendCoeff {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) (A : C(↑(closedCubeAt y n), HCPolySupport.Mat d)) : Continuous (extendCoeff y n A)

theorem Algsuperdiff.Section5.Support.extendCoeff_apply_of_mem {d : ℕ} {y : HCPolySupport.Vec d} {n : ℤ} (A : C(↑(closedCubeAt y n), HCPolySupport.Mat d)) {x : HCPolySupport.Vec d} (hx : x ∈ closedCubeAt y n) : extendCoeff y n A x = A ⟨x, hx⟩

2. The equation only sees the coefficient on the cube

theorem Algsuperdiff.Section5.Support.isDivFormWeakSolutionOn_congr_coeff {d : ℕ} {W : Set (HCPolySupport.Vec d)} (hW : MeasurableSet W) {a b : HCPolySupport.CoeffField d} (hab : ∀ x ∈ W, a x = b x) {u : HCPolySupport.H1Function W} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (h : Section4.Support.IsDivFormWeakSolutionOn a W u g) : Section4.Support.IsDivFormWeakSolutionOn b W u g

theorem Algsuperdiff.Section5.Support.isDirichletSolutionAt_congr_coeff {d : ℕ} {y : HCPolySupport.Vec d} {n : ℤ} {a b : HCPolySupport.CoeffField d} (hab : ∀ x ∈ cubeSetAt y n, a x = b x) {u : HCPolySupport.H1Function (cubeSetAt y n)} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (h : IsDirichletSolutionAt a y n u g) : IsDirichletSolutionAt b y n u g

3. The parameter space

def Algsuperdiff.Section5.Support.ellipticCube {d : ℕ} (nu : ℝ) (y : HCPolySupport.Vec d) (n : ℤ) : Set C(↑(closedCubeAt y n), HCPolySupport.Mat d)

The continuous matrix fields on the closed cube whose symmetric part is ν I.

Equations

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

theorem Algsuperdiff.Section5.Support.coefficientCutoffRestrict_mem_ellipticCube {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (y : HCPolySupport.Vec d) (n : ℤ) (omega : Section3.Cutoff.CutoffSample d) : coefficientCutoffRestrict M.nu m (closedCubeAt y n) omega ∈ ellipticCube M.nu y n

4. Ellipticity of the extended field

theorem Algsuperdiff.Section5.Support.exists_isEllipticFieldOn_extendCoeff {d : ℕ} {nu : ℝ} (hnu : 0 < nu) (y : HCPolySupport.Vec d) (n : ℤ) {A : C(↑(closedCubeAt y n), HCPolySupport.Mat d)} (hA : A ∈ ellipticCube nu y n) : ∃ (Lam : ℝ), HCPolySupport.IsEllipticFieldOn nu Lam (cubeSetAt y n) (extendCoeff y n A)

5. The solution attached to a parameter

theorem Algsuperdiff.Section5.Support.exists_isDirichletSolutionAt_extendCoeff {d : ℕ} (M : Section3.ABKModel d) (y : HCPolySupport.Vec d) (n : ℤ) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} {Kg : ℝ} (hKg : 0 ≤ Kg) (hg : Section4.Support.HolderSeminormBoundOn (cubeSetAt y n) (1 / 2) Kg g) (A : ↑(ellipticCube M.nu y n)) : ∃ (u : HCPolySupport.H1Function (cubeSetAt y n)), IsDirichletSolutionAt (extendCoeff y n ↑A) y n u g

noncomputable def Algsuperdiff.Section5.Support.solutionOfField {d : ℕ} (M : Section3.ABKModel d) (y : HCPolySupport.Vec d) (n : ℤ) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} {Kg : ℝ} (hKg : 0 ≤ Kg) (hg : Section4.Support.HolderSeminormBoundOn (cubeSetAt y n) (1 / 2) Kg g) (A : ↑(ellipticCube M.nu y n)) : HCPolySupport.H1Function (cubeSetAt y n)

The solution attached to a parameter.

Equations

• Algsuperdiff.Section5.Support.solutionOfField M y n hKg hg A = ⋯.choose

theorem Algsuperdiff.Section5.Support.isDirichletSolutionAt_solutionOfField {d : ℕ} (M : Section3.ABKModel d) (y : HCPolySupport.Vec d) (n : ℤ) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} {Kg : ℝ} (hKg : 0 ≤ Kg) (hg : Section4.Support.HolderSeminormBoundOn (cubeSetAt y n) (1 / 2) Kg g) (A : ↑(ellipticCube M.nu y n)) : IsDirichletSolutionAt (extendCoeff y n ↑A) y n (solutionOfField M y n hKg hg A) g

theorem Algsuperdiff.Section5.Support.isDirichletSolutionAt_solutionOfField_cutoff {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (y : HCPolySupport.Vec d) (n : ℤ) (omega : Section3.Cutoff.CutoffSample d) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} {Kg : ℝ} (hKg : 0 ≤ Kg) (hg : Section4.Support.HolderSeminormBoundOn (cubeSetAt y n) (1 / 2) Kg g) : IsDirichletSolutionAt (Section3.Cutoff.coefficientCutoff M.nu m omega).toCoeffField y n (solutionOfField M y n hKg hg ⟨coefficientCutoffRestrict M.nu m (closedCubeAt y n) omega, ⋯⟩) g

At the sample's own parameter the two solutions agree. The extended field and the cutoff field coincide on the cube, so the parameter solution solves the sample's problem.