CubeSchauderExistence

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

Cube Schauder, existence leg

  -sigma Δ v = ∇ · g   in □_m ,      v = h   on ∂□_m

has a solution in the development's IsDirichletSolutionOn carrier. This is CoarseGraining's Lax--Milgram Dirichlet existence theorem (exists_isZeroTraceDirichletRhsWeakSolution_of_potentialZeroTraceClosureRealization) at the constant scalar background sigma • I, composed with the affine shift by the datum h.

No estimate is proved here: the produced solution carries no regularity of its gradient representative. Every declaration is a proved local helper; no source node is claimed, realized, or closed by this module.

Main results

• exists_isDirichletSolutionOn_smul_one — existence with an arbitrary H¹ datum.
• exists_isDirichletSolutionOn_smul_one_of_holder — the specialization whose forcing hypothesis is the frozen statement's Hölder bound.

1. The constant scalar background

theorem Algsuperdiff.Section4.Provider.Schauder.matVecMul_smul_one {d : ℕ} (c : ℝ) (x : HCPolySupport.Vec d) : HCPolySupport.matVecMul (c • 1) x = c • x

(c • I) x = c • x, at the exact spelling c • (1 : Mat d) of the frozen statement.

theorem Algsuperdiff.Section4.Provider.Schauder.matVecMul_one {d : ℕ} (x : HCPolySupport.Vec d) : HCPolySupport.matVecMul 1 x = x

(1 : Mat d) x = x.

theorem Algsuperdiff.Section4.Provider.Schauder.isEllipticFieldOn_smul_one {d : ℕ} {sigma : ℝ} (hsigma : 0 < sigma) {U : Set (HCPolySupport.Vec d)} (hU : MeasurableSet U) : HCPolySupport.IsEllipticFieldOn sigma sigma U fun (x : HCPolySupport.Vec d) => sigma • 1

The constant scalar background sigma • I is a (sigma, sigma)-elliptic field on any measurable set.

2. Splitting the forcing pairing

theorem Algsuperdiff.Section4.Provider.Schauder.integral_vecDot_neg_split {d : ℕ} {U : Set (HCPolySupport.Vec d)} (F : HCPolySupport.Vec d → HCPolySupport.Vec d) (φ : HCPolySupport.H10Function U) : ∫ (x : HCPolySupport.Vec d) in U, HCPolySupport.vecDot (-F x) (φ.grad x) = -∫ (x : HCPolySupport.Vec d) in U, HCPolySupport.vecDot (F x) (φ.grad x)

The forcing pairing is odd in the force.

theorem Algsuperdiff.Section4.Provider.Schauder.integral_vecDot_add_split {d : ℕ} {U : Set (HCPolySupport.Vec d)} {F G H : HCPolySupport.Vec d → HCPolySupport.Vec d} (hF : HCPolySupport.MemVectorL2 U F) (hG : HCPolySupport.MemVectorL2 U G) (hH : ∀ (x : HCPolySupport.Vec d), H x = F x + G x) (φ : HCPolySupport.H10Function U) : ∫ (x : HCPolySupport.Vec d) in U, HCPolySupport.vecDot (H x) (φ.grad x) = (∫ (x : HCPolySupport.Vec d) in U, HCPolySupport.vecDot (F x) (φ.grad x)) + ∫ (x : HCPolySupport.Vec d) in U, HCPolySupport.vecDot (G x) (φ.grad x)

The forcing pairing is additive in the force.

theorem Algsuperdiff.Section4.Provider.Schauder.integral_vecDot_sub_split {d : ℕ} {U : Set (HCPolySupport.Vec d)} {F G H : HCPolySupport.Vec d → HCPolySupport.Vec d} (hF : HCPolySupport.MemVectorL2 U F) (hG : HCPolySupport.MemVectorL2 U G) (hH : ∀ (x : HCPolySupport.Vec d), H x = F x - G x) (φ : HCPolySupport.H10Function U) : ∫ (x : HCPolySupport.Vec d) in U, HCPolySupport.vecDot (H x) (φ.grad x) = (∫ (x : HCPolySupport.Vec d) in U, HCPolySupport.vecDot (F x) (φ.grad x)) - ∫ (x : HCPolySupport.Vec d) in U, HCPolySupport.vecDot (G x) (φ.grad x)

The forcing pairing is subtractive in the force.

theorem Algsuperdiff.Section4.Provider.Schauder.integral_vecDot_smul_split {d : ℕ} {U : Set (HCPolySupport.Vec d)} (c : ℝ) (F : HCPolySupport.Vec d → HCPolySupport.Vec d) (φ : HCPolySupport.H10Function U) : ∫ (x : HCPolySupport.Vec d) in U, HCPolySupport.vecDot (c • F x) (φ.grad x) = c * ∫ (x : HCPolySupport.Vec d) in U, HCPolySupport.vecDot (F x) (φ.grad x)

The forcing pairing is homogeneous in the force.

3. Existence

theorem Algsuperdiff.Section4.Provider.Schauder.exists_isDirichletSolutionOn_smul_one {d : ℕ} [NeZero d] {m : ℤ} {sigma : ℝ} (hsigma : 0 < sigma) (h : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hg : HCPolySupport.MemVectorL2 (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) g) : ∃ (v : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))), Support.IsDirichletSolutionOn (fun (x : HCPolySupport.Vec d) => sigma • 1) (HCPolySupport.originCube d m) v h g

The comparator exists. For every scale, diffusivity, H¹ datum and L² forcing the constant-coefficient cube Dirichlet problem has a solution in the development's carrier. No regularity of v.grad is asserted.

theorem Algsuperdiff.Section4.Provider.Schauder.exists_isDirichletSolutionOn_smul_one_of_holder {d : ℕ} [NeZero d] {m : ℤ} {sigma : ℝ} (hsigma : 0 < sigma) (h : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} {Kg : ℝ} (hKg : Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kg g) : ∃ (v : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))), Support.IsDirichletSolutionOn (fun (x : HCPolySupport.Vec d) => sigma • 1) (HCPolySupport.originCube d m) v h g

The existence leg with the frozen statement's Hölder hypothesis in place of L² membership.