DatumContinuity

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

The difference of two solutions of the same localized problem

For a fixed elliptic coefficient field on y + □_n the difference of the solutions of two Dirichlet problems with the same zero boundary condition is itself a zero-trace function on the cube, and a uniform bound on the difference of the two data is an L² bound on the cube.

Those are the two steps a continuity estimate in the datum starts from: the energy estimate carries the L² size of the datum difference to the gradient of the difference of the solutions, and the zero-trace Poincaré inequality carries it back to the L² size of the difference itself.

Main results

• exists_h10Function_sub — the zero-trace witness of a difference of solutions.
• setIntegral_sq_le_of_forall_norm_le — a uniform bound gives an L² bound.

References

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

1. The zero-trace witness of a difference of solutions

theorem Algsuperdiff.Section5.Support.exists_h10Function_sub {d : ℕ} {y : HCPolySupport.Vec d} {n : ℤ} {a : HCPolySupport.CoeffField d} {u u' : HCPolySupport.H1Function (cubeSetAt y n)} {g g' : HCPolySupport.Vec d → HCPolySupport.Vec d} (hu : IsDirichletSolutionAt a y n u g) (hu' : IsDirichletSolutionAt a y n u' g') : ∃ (w : HCPolySupport.H10Function (cubeSetAt y n)), (∀ (x : HCPolySupport.Vec d), w.toFun x = u.toFun x - u'.toFun x) ∧ ∀ (x : HCPolySupport.Vec d), w.grad x = u.grad x - u'.grad x

The difference of two solutions of the same localized problem has a zero-trace witness, whatever the two forcing fields are.

2. A uniform bound on the cube is an L² bound

theorem Algsuperdiff.Section5.Support.setIntegral_sq_le_of_forall_norm_le {d : ℕ} {y : HCPolySupport.Vec d} {n : ℤ} {f : HCPolySupport.Vec d → HCPolySupport.Vec d} {eta : ℝ} (hf : ∀ x ∈ cubeSetAt y n, ‖f x‖ ≤ eta) : ∫ (x : HCPolySupport.Vec d) in cubeSetAt y n, ‖f x‖ ^ 2 ≤ MeasureTheory.volume.real (cubeSetAt y n) * eta ^ 2

A uniformly small field on the cube is small in L² there.