DatumIntegralContinuity

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

The integral of the solution over a fixed set is continuous in the datum

Reading both localized quantities off ball averages replaces every pointwise statement about the solution by a statement about its integral over a fixed ball. What the reduction of the supremum over the forcing class to a countable subclass then needs is only this: at a fixed set inside the cube, the integral of the solution depends continuously on the forcing field in the supremum norm on the cube.

The chain is the energy estimate, the zero-trace Poincaré inequality and Cauchy-Schwarz against the constant one, with no regularity of the solution used anywhere.

Main results

• exists_eta_abs_setIntegral_sub_le, exists_eta_abs_setAverage_ball_sub_le.
• setAverage_ball_sub_of_h1 — the average of a difference splits.

References

• ABK26, the localized error and regularity quantities of Section 5.1.

theorem Algsuperdiff.Section5.Support.exists_eta_abs_setIntegral_sub_le {d : ℕ} [NeZero d] {y : HCPolySupport.Vec d} {n : ℤ} {a : HCPolySupport.CoeffField d} {lam Lam : ℝ} (hEll : HCPolySupport.IsEllipticFieldOn lam Lam (cubeSetAt y n) a) {B : Set (HCPolySupport.Vec d)} (hB : B ⊆ cubeSetAt y n) {eps : ℝ} (heps : 0 < eps) : ∃ (eta : ℝ), 0 < eta ∧ ∀ (g g' : HCPolySupport.Vec d → HCPolySupport.Vec d), HCPolySupport.MemVectorL2 (cubeSetAt y n) g → HCPolySupport.MemVectorL2 (cubeSetAt y n) g' → (∀ x ∈ cubeSetAt y n, ‖g x - g' x‖ ≤ eta) → ∀ (u u' : HCPolySupport.H1Function (cubeSetAt y n)), IsDirichletSolutionAt a y n u g → IsDirichletSolutionAt a y n u' g' → |(∫ (z : HCPolySupport.Vec d) in B, u.toFun z) - ∫ (z : HCPolySupport.Vec d) in B, u'.toFun z| ≤ eps

At a fixed subset of the cube the integral of the solution is uniformly continuous in the forcing field.

2. The same for the average, and a splitting

theorem Algsuperdiff.Section5.Support.setAverage_ball_sub_of_h1 {d : ℕ} {y : HCPolySupport.Vec d} {n : ℤ} (u v : HCPolySupport.H1Function (cubeSetAt y n)) {p : HCPolySupport.Vec d} {r : ℝ} (hB : Metric.ball p r ⊆ cubeSetAt y n) : ⨍ (z : HCPolySupport.Vec d) in Metric.ball p r, u.toFun z - v.toFun z = (⨍ (z : HCPolySupport.Vec d) in Metric.ball p r, u.toFun z) - ⨍ (z : HCPolySupport.Vec d) in Metric.ball p r, v.toFun z

theorem Algsuperdiff.Section5.Support.exists_eta_abs_setAverage_ball_sub_le {d : ℕ} [NeZero d] {y : HCPolySupport.Vec d} {n : ℤ} {a : HCPolySupport.CoeffField d} {lam Lam : ℝ} (hEll : HCPolySupport.IsEllipticFieldOn lam Lam (cubeSetAt y n) a) {p : HCPolySupport.Vec d} {r : ℝ} (hr : 0 < r) (hB : Metric.ball p r ⊆ cubeSetAt y n) {eps : ℝ} (heps : 0 < eps) : ∃ (eta : ℝ), 0 < eta ∧ ∀ (g g' : HCPolySupport.Vec d → HCPolySupport.Vec d), HCPolySupport.MemVectorL2 (cubeSetAt y n) g → HCPolySupport.MemVectorL2 (cubeSetAt y n) g' → (∀ x ∈ cubeSetAt y n, ‖g x - g' x‖ ≤ eta) → ∀ (u u' : HCPolySupport.H1Function (cubeSetAt y n)), IsDirichletSolutionAt a y n u g → IsDirichletSolutionAt a y n u' g' → |(⨍ (z : HCPolySupport.Vec d) in Metric.ball p r, u.toFun z) - ⨍ (z : HCPolySupport.Vec d) in Metric.ball p r, u'.toFun z| ≤ eps

At a fixed ball inside the cube the average of the solution is uniformly continuous in the forcing field.