EnergyPoincare

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

The Poincaré inequality in integral form, and solvability for a general elliptic field

Two ingredients that the measurability of the localized quantities needs.

The Poincaré inequality in integral form. The zero-trace Poincaré estimate of the ambient layer is stated between the L² classes of the value and of the coordinates of the gradient. Rewriting both sides as square roots of integrals turns it into the form the energy estimates are written in, at the price of the dimensional factor d from the supremum norm of the gradient.

Solvability for a general elliptic field. The rough-field existence statement is specialized to the cutoff coefficient; the same argument works for any field that is elliptic on the cube, which is what a coefficient-dependent solution map requires.

Main results

• exists_poincare_integral_constant.
• exists_isDirichletSolutionAt_of_isEllipticFieldOn.

References

• ABK26, the localized Dirichlet problems of Section 5.1.

1. The two L² norms as integrals

theorem Algsuperdiff.Section5.Support.norm_toScalarL2_eq_sqrt {d : ℕ} {U : Set (HCPolySupport.Vec d)} (w : HCPolySupport.H1Function U) : ‖w.toScalarL2‖ = √(∫ (x : HCPolySupport.Vec d) in U, w.toFun x ^ 2)

theorem Algsuperdiff.Section5.Support.norm_gradCoordToScalarL2_eq_sqrt {d : ℕ} {U : Set (HCPolySupport.Vec d)} (w : HCPolySupport.H1Function U) (i : Fin d) : ‖w.gradCoordToScalarL2 i‖ = √(∫ (x : HCPolySupport.Vec d) in U, w.grad x i ^ 2)

2. The gradient sum is dominated by the supremum-norm energy

theorem Algsuperdiff.Section5.Support.gradientCoordL2NormSum_le {d : ℕ} {U : Set (HCPolySupport.Vec d)} (w : HCPolySupport.H1Function U) : w.gradientCoordL2NormSum ≤ ↑d * √(∫ (x : HCPolySupport.Vec d) in U, ‖w.grad x‖ ^ 2)

3. The Poincaré inequality in integral form

theorem Algsuperdiff.Section5.Support.exists_poincare_integral_constant {d : ℕ} [NeZero d] {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) : ∃ (CP : ℝ), 0 ≤ CP ∧ ∀ (w : HCPolySupport.H10Function U), √(∫ (x : HCPolySupport.Vec d) in U, w.toFun x ^ 2) ≤ CP * √(∫ (x : HCPolySupport.Vec d) in U, ‖w.grad x‖ ^ 2)

The zero-trace Poincaré inequality, written between integrals.

4. Solvability for a general elliptic field

theorem Algsuperdiff.Section5.Support.exists_isDirichletSolutionAt_of_isEllipticFieldOn {d : ℕ} [NeZero d] {y : HCPolySupport.Vec d} {n : ℤ} {a : HCPolySupport.CoeffField d} {lam Lam : ℝ} (hEll : HCPolySupport.IsEllipticFieldOn lam Lam (cubeSetAt y n) a) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} {Kg : ℝ} (hKg : 0 ≤ Kg) (hg : Section4.Support.HolderSeminormBoundOn (cubeSetAt y n) (1 / 2) Kg g) : ∃ (u : HCPolySupport.H1Function (cubeSetAt y n)), IsDirichletSolutionAt a y n u g

The Dirichlet problem on y + □_n is solvable for every coefficient field that is elliptic on the cube.