Poincaré's inequality with the mean subtracted

On a bounded connected open domain with C¹ boundary, an element of H¹(Ω) is within a constant times the L² norm of its gradient of its mean. This is Evans §5.8.1 Theorem 1 at p = 2. Only the gradient appears on the right, which is what distinguishes it from the Poincaré inequality on H₀¹(Ω) the library runs existence on, where the boundary condition replaces the subtraction of the mean.

The proof is Evans's, by contradiction. Were the estimate false, a sequence of elements of unit L² norm, zero mean and gradient tending to zero would exist; Rellich-Kondrachov on the graph space makes a subsequence converge in L², the limit has zero weak gradient because the graph space is closed, so it is constant on the connected domain, its mean is zero, so it vanishes, against its unit norm.

Main declarations

• EllipticPdes.Sobolev.constGraph: the graph of a constant, with zero gradient, and constGraph_mem_W12.
• EllipticPdes.Sobolev.meanL2: the mean over the domain as a continuous linear functional on L²(Ω).
• EllipticPdes.Sobolev.poincare_wirtinger: the inequality.

References

L. C. Evans, Partial Differential Equations (2nd ed.), §5.8.1 Theorem 1 (p. 290).

Constants

noncomputable def EllipticPdes.Sobolev.constL2 {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩb : Bornology.IsBounded Ω) (c : ℝ) : L2D Ω

The class of a constant in L²(Ω).

Equations

• EllipticPdes.Sobolev.constL2 hΩb c = MeasureTheory.MemLp.toLp (fun (x : EuclideanSpace ℝ (Fin d)) => c) ⋯

theorem EllipticPdes.Sobolev.coeFn_constL2 {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩb : Bornology.IsBounded Ω) (c : ℝ) : ↑↑(constL2 hΩb c) =ᵐ[MeasureTheory.volume.restrict Ω] fun (x : EuclideanSpace ℝ (Fin d)) => c

theorem EllipticPdes.Sobolev.constL2_zero {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩb : Bornology.IsBounded Ω) : constL2 hΩb 0 = 0

noncomputable def EllipticPdes.Sobolev.constGraph {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩb : Bornology.IsBounded Ω) (c : ℝ) : H1amb Ω

The graph of a constant: the constant as function coordinate and zero as gradient.

Equations

• EllipticPdes.Sobolev.constGraph hΩb c = WithLp.toLp 2 (Fin.cons (EllipticPdes.Sobolev.constL2 hΩb c) fun (x : Fin d) => 0)

@[simp]

theorem EllipticPdes.Sobolev.constGraph_zero {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩb : Bornology.IsBounded Ω) (c : ℝ) : (constGraph hΩb c).ofLp 0 = constL2 hΩb c

@[simp]

theorem EllipticPdes.Sobolev.constGraph_succ {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩb : Bornology.IsBounded Ω) (c : ℝ) (k : Fin d) : (constGraph hΩb c).ofLp k.succ = 0

theorem EllipticPdes.Sobolev.constGraph_mem_W12 {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩb : Bornology.IsBounded Ω) (c : ℝ) : constGraph hΩb c ∈ W12 Ω

Membership of a constant in the graph space, with zero weak gradient: a test function's partial derivative integrates to zero.

noncomputable def EllipticPdes.Sobolev.meanL2 {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩb : Bornology.IsBounded Ω) : L2D Ω →L[ℝ] ℝ

Mean as a functional. The mean over Ω of an L²(Ω) class, read as the inner product against the constant one over the measure of the domain.

Equations

• EllipticPdes.Sobolev.meanL2 hΩb = (MeasureTheory.volume Ω).toReal⁻¹ • (innerSL ℝ) (EllipticPdes.Sobolev.constL2 hΩb 1)

theorem EllipticPdes.Sobolev.meanL2_apply {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩb : Bornology.IsBounded Ω) (f : L2D Ω) : (meanL2 hΩb) f = (MeasureTheory.volume Ω).toReal⁻¹ * ∫ (x : EuclideanSpace ℝ (Fin d)) in Ω, ↑↑f x

theorem EllipticPdes.Sobolev.meanL2_constL2 {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩb : Bornology.IsBounded Ω) (hΩ0 : MeasureTheory.volume Ω ≠ 0) (c : ℝ) : (meanL2 hΩb) (constL2 hΩb c) = c

The inequality

theorem EllipticPdes.Sobolev.poincare_wirtinger {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hd : 0 < d) (hΩopen : IsOpen Ω) (hΩb : Bornology.IsBounded Ω) (hC1 : Extension.HasC1Boundary Ω) (hconn : IsPreconnected Ω) (hne : Ω.Nonempty) : ∃ (C : ℝ), ∀ (U : ↥(W12 Ω)), ‖(embW12 Ω) U - constL2 hΩb ((meanL2 hΩb) ((embW12 Ω) U))‖ ≤ C * √(∑ k : Fin d, ‖(↑U).ofLp k.succ‖ ^ 2)

Poincaré's inequality with the mean subtracted (Evans §5.8.1 Theorem 1 at p = 2). On a bounded, connected, open domain with C¹ boundary, one constant bounds the L² distance of every element of H¹(Ω) from its mean by the L² norm of its gradient.

theorem EllipticPdes.Sobolev.poincare_wirtinger_ball {d : ℕ} (hd : 0 < d) : ∃ (C : ℝ), ∀ (U : ↥(W12 (Metric.ball 0 1))), ‖(embW12 (Metric.ball 0 1)) U - constL2 ⋯ ((meanL2 ⋯) ((embW12 (Metric.ball 0 1)) U))‖ ≤ C * √(∑ k : Fin d, ‖(↑U).ofLp k.succ‖ ^ 2)

Inequality on the unit ball, every hypothesis discharged: the ball is open, bounded, convex hence connected, nonempty, and has C¹ boundary.