SolutionCoefficientContinuity

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

The solution depends continuously on the coefficient field

Two Dirichlet solutions on y + □_n for the same forcing field but different coefficient fields differ, in the energy norm, by at most the supremum distance of the coefficient fields times the energy of one of them:

  ‖∇(u_a − u_b)‖_{L²} ≤ lam⁻¹ · d² · ‖a − b‖_∞ · ‖∇u_b‖_{L²} .

The proof is the printed one: subtract the two weak equations, test with the difference, use ellipticity on the left and the pairing bound on the right. The dimensional factor d² is the price of the supremum-norm carrier — one d from the pairing bound and one from the action of a matrix with entries bounded by ‖a − b‖_∞.

Main results

• sqrt_energy_grad_sub_le — the estimate above.

References

• ABK26, the localized Dirichlet problems of Section 5.1.

1. Auxiliary bounds

theorem Algsuperdiff.Section5.Support.norm_le_sqrt_vecNormSq {d : ℕ} (xi : HCPolySupport.Vec d) : ‖xi‖ ≤ √(HCPolySupport.vecNormSq xi)

theorem Algsuperdiff.Section5.Support.sq_norm_le_vecNormSq {d : ℕ} (xi : HCPolySupport.Vec d) : ‖xi‖ ^ 2 ≤ HCPolySupport.vecNormSq xi

theorem Algsuperdiff.Section5.Support.integrableOn_sq_norm_of_memVectorL2 {d : ℕ} {U : Set (HCPolySupport.Vec d)} {F : HCPolySupport.Vec d → HCPolySupport.Vec d} (hF : HCPolySupport.MemVectorL2 U F) : MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => ‖F x‖ ^ 2) U MeasureTheory.volume

The square of the norm of an L² field is integrable.

theorem Algsuperdiff.Section5.Support.sqrt_setIntegral_sq_norm_le_of_energy_bound {d : ℕ} {U : Set (HCPolySupport.Vec d)} {a : HCPolySupport.CoeffField d} {lam Lam C : ℝ} {F : HCPolySupport.Vec d → HCPolySupport.Vec d} (hlam : 0 ≤ lam) (hC : 0 ≤ C) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (hF : HCPolySupport.MemVectorL2 U F) (henergy : ∫ (x : HCPolySupport.Vec d) in U, HCPolySupport.vecDot (HCPolySupport.matVecMul (a x) (F x)) (F x) ≤ C * √(∫ (x : HCPolySupport.Vec d) in U, ‖F x‖ ^ 2)) : lam * √(∫ (x : HCPolySupport.Vec d) in U, ‖F x‖ ^ 2) ≤ C

Lower ellipticity converts any energy bound into an L² bound, independently of the equation or forcing used to obtain the pairing budget.

theorem Algsuperdiff.Section5.Support.abs_setIntegral_vecDot_le_of_norm_le {d : ℕ} (U : Set (HCPolySupport.Vec d)) (hU : MeasurableSet U) {F G H : HCPolySupport.Vec d → HCPolySupport.Vec d} {c : ℝ} (hc : 0 ≤ c) (hH : HCPolySupport.MemVectorL2 U H) (hG : HCPolySupport.MemVectorL2 U G) (hFH : ∀ x ∈ U, ‖F x‖ ≤ c * ‖H x‖) : |∫ (x : HCPolySupport.Vec d) in U, HCPolySupport.vecDot (F x) (G x)| ≤ ↑d * c * (√(∫ (x : HCPolySupport.Vec d) in U, ‖H x‖ ^ 2) * √(∫ (x : HCPolySupport.Vec d) in U, ‖G x‖ ^ 2))

The pairing bound with the first field controlled pointwise by a second one; this avoids any measurability assumption on the first field.

2. The estimate

theorem Algsuperdiff.Section5.Support.sqrt_energy_grad_sub_le_of_weak_solutions {d : ℕ} {y : HCPolySupport.Vec d} {n : ℤ} {a b : HCPolySupport.CoeffField d} {lam Lam delta : ℝ} (hdelta : 0 ≤ delta) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam (cubeSetAt y n) a) (hab : ∀ x ∈ cubeSetAt y n, ∀ (i j : Fin d), |a x i j - b x i j| ≤ delta) {u v : HCPolySupport.H1Function (cubeSetAt y n)} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hbv : HCPolySupport.MemVectorL2 (cubeSetAt y n) fun (x : HCPolySupport.Vec d) => HCPolySupport.matVecMul (b x) (v.grad x)) (w : HCPolySupport.H10Function (cubeSetAt y n)) (hwg : ∀ (x : HCPolySupport.Vec d), w.grad x = u.grad x - v.grad x) (hu : Section4.Support.IsDivFormWeakSolutionOn a (cubeSetAt y n) u g) (hv : Section4.Support.IsDivFormWeakSolutionOn b (cubeSetAt y n) v g) : √(∫ (x : HCPolySupport.Vec d) in cubeSetAt y n, ‖u.grad x - v.grad x‖ ^ 2) ≤ lam⁻¹ * (↑d * ↑d * delta) * √(∫ (x : HCPolySupport.Vec d) in cubeSetAt y n, ‖v.grad x‖ ^ 2)

Energy perturbation for weak solutions whose gradient difference has a zero-trace witness.

theorem Algsuperdiff.Section5.Support.sqrt_energy_grad_sub_le {d : ℕ} {y : HCPolySupport.Vec d} {n : ℤ} {a b : HCPolySupport.CoeffField d} {lam Lam delta : ℝ} (hdelta : 0 ≤ delta) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam (cubeSetAt y n) a) (hab : ∀ x ∈ cubeSetAt y n, ∀ (i j : Fin d), |a x i j - b x i j| ≤ delta) {u v : HCPolySupport.H1Function (cubeSetAt y n)} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hbv : HCPolySupport.MemVectorL2 (cubeSetAt y n) fun (x : HCPolySupport.Vec d) => HCPolySupport.matVecMul (b x) (v.grad x)) (hu : IsDirichletSolutionAt a y n u g) (hv : IsDirichletSolutionAt b y n v g) : √(∫ (x : HCPolySupport.Vec d) in cubeSetAt y n, ‖u.grad x - v.grad x‖ ^ 2) ≤ lam⁻¹ * (↑d * ↑d * delta) * √(∫ (x : HCPolySupport.Vec d) in cubeSetAt y n, ‖v.grad x‖ ^ 2)

The solution map is continuous in the coefficient field, in the energy norm, with the dimensional factor d² of the supremum-norm carrier.

hbv is the minimal integrability datum the subtraction of the two weak equations needs; at the use sites it is supplied by the ellipticity of the second coefficient field.