Full Poincaré inequality on the domain (dependency-chain step 3)

Average the n directional bounds from poincare_slice_box to obtain the domain Poincaré inequality. Each coordinate direction i of the box contributes a bound ∫_Ω u² ≤ c i * ∫_Ω (∂_i u)²; summing over the n directions and dividing by n gives ∫_Ω u² ≤ (1 / n) * ∑_i c i * ∫_Ω (∂_i u)². The resulting constant is the domain constant C_P (for equal side lengths c i = L² / 2 this is L² / (2 n), matching the diameter-based bound).

theorem EllipticPdes.Poincare.poincare_domain {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {Ω : Set α} {n : ℕ} (hn : 0 < n) {u : α → ℝ} {d : Fin n → α → ℝ} {c : Fin n → ℝ} (hslice : ∀ (i : Fin n), ∫ (x : α) in Ω, u x ^ 2 ∂μ ≤ c i * ∫ (x : α) in Ω, d i x ^ 2 ∂μ) : ∫ (x : α) in Ω, u x ^ 2 ∂μ ≤ 1 / ↑n * ∑ i : Fin n, c i * ∫ (x : α) in Ω, d i x ^ 2 ∂μ

The averaging step of the domain Poincaré inequality.

Given n bounds of the form ∫_Ω u² ≤ c i * ∫_Ω (d i)², one per index i, this returns their average. The family d : Fin n → α → ℝ is arbitrary: nothing here requires d i to be a derivative of u, Ω to be a box or a bounded domain, or μ to be Lebesgue measure. Read on its own this is a statement about families of real-valued functions.

All the Poincaré content sits in the caller, which supplies hslice with d i = ∂_i u and pays for the geometry: poincare_H01_euclBox for a coordinate box, poincare_H01_of_bounded for a bounded domain. Cite one of those when citing the inequality itself.