Poincaré inequality on arbitrary bounded domains (chain step 5)

BoxSlice.lean discharges the per-direction slice bound when the domain IS the open coordinate box. This file removes that restriction: any Ω contained in a box inherits the slice bound, because a test function of Ω is a test function of the box (IsTestFn.mono) and the box integrals restrict to Ω (the integrands vanish off tsupport φ ⊆ Ω). Averaging (poincare_testfn) and density (poincare_H01) are already domain-general, so the Poincaré inequality follows on every bounded domain (poincare_H01_of_bounded), with the closed-form constant L²/(2(n+1)) from any bounding box of side L. This is the p = q = 2 Friedrichs (Poincaré) inequality for H₀¹; the limit passage from test functions to H₀¹(Ω) by density is the density step poincare_H01, which is architectural here because H₀¹ is defined as the closure of the test-function graphs.

theorem EllipticPdes.Poincare.slice_bound_of_subset_euclBox {n : ℕ} {a b : Fin (n + 1) → ℝ} (hab : ∀ (k : Fin (n + 1)), a k ≤ b k) {Ω : Set (EuclideanSpace ℝ (Fin (n + 1)))} (hsub : Ω ⊆ euclBox a b) {φ : EuclideanSpace ℝ (Fin (n + 1)) → ℝ} (h : Sobolev.IsTestFn Ω φ) (i : Fin (n + 1)) : ∫ (x : EuclideanSpace ℝ (Fin (n + 1))) in Ω, φ x ^ 2 ≤ (b i - a i) ^ 2 / 2 * ∫ (x : EuclideanSpace ℝ (Fin (n + 1))) in Ω, Sobolev.partialD i φ x ^ 2

Per-direction Poincaré bound for a subset of a box. A test function of any Ω inside the open box obeys the box slice bound with the integrals taken over Ω.

theorem EllipticPdes.Poincare.poincare_H01_of_subset_euclBox {n : ℕ} {a b : Fin (n + 1) → ℝ} (hab : ∀ (k : Fin (n + 1)), a k ≤ b k) {Ω : Set (EuclideanSpace ℝ (Fin (n + 1)))} (hsub : Ω ⊆ euclBox a b) {L : ℝ} (hL : ∀ (i : Fin (n + 1)), b i - a i ≤ L) {U : Sobolev.H1amb Ω} (hU : U ∈ Sobolev.H01 Ω) : ‖U.ofLp 0‖ ^ 2 ≤ L ^ 2 / (2 * (↑n + 1)) * ∑ i : Fin (n + 1), ‖U.ofLp i.succ‖ ^ 2

Poincaré inequality on H₀¹(Ω) for Ω inside a box with sides at most L: ‖U₀‖² ≤ L²/(2(n+1)) · ∑ᵢ ‖Uᵢ‖².

theorem EllipticPdes.Poincare.testfn_bound_of_subset_euclBox {n : ℕ} {a b : Fin (n + 1) → ℝ} (hab : ∀ (k : Fin (n + 1)), a k ≤ b k) {Ω : Set (EuclideanSpace ℝ (Fin (n + 1)))} (hsub : Ω ⊆ euclBox a b) {C : ℝ} (hC : ∀ (i : Fin (n + 1)), (b i - a i) ^ 2 / 2 ≤ C) {φ : EuclideanSpace ℝ (Fin (n + 1)) → ℝ} (h : Sobolev.IsTestFn Ω φ) : ‖h.testGraph.ofLp 0‖ ^ 2 ≤ C / (↑n + 1) * ∑ i : Fin (n + 1), ‖h.testGraph.ofLp i.succ‖ ^ 2

The test-function instance, in the slice-constant form the coercivity layer consumes. Derived FROM poincare_H01_of_subset_euclBox (test graphs lie in H₀¹).

theorem EllipticPdes.Poincare.exists_euclBox_superset {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin (n + 1)))} (hΩb : Bornology.IsBounded Ω) : ∃ (a : Fin (n + 1) → ℝ) (b : Fin (n + 1) → ℝ) (L : ℝ), (∀ (k : Fin (n + 1)), a k ≤ b k) ∧ Ω ⊆ euclBox a b ∧ ∀ (i : Fin (n + 1)), b i - a i ≤ L

Every bounded set sits inside an open coordinate box with sides bounded by a single L (derived from a bounding radius about the origin).

theorem EllipticPdes.Poincare.poincare_H01_of_bounded {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin (n + 1)))} (hΩb : Bornology.IsBounded Ω) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ U ∈ Sobolev.H01 Ω, ‖U.ofLp 0‖ ^ 2 ≤ C * ∑ i : Fin (n + 1), ‖U.ofLp i.succ‖ ^ 2

Poincaré inequality on H₀¹ of an arbitrary bounded domain (the Friedrichs inequality, p = q = 2): some constant C ≥ 0 controls the function part by the gradient part, uniformly over H₀¹(Ω).

Guo, Partial Differential Equations (JHU AS.110.631-632), Theorem III.4.6 states the W_0^{1,p} form, ‖u‖_{L^q} ≤ C ‖Du‖_{L^p} for q ∈ [1, p*], and derives it from the Gagliardo-Nirenberg-Sobolev inequality. This declaration is its p = q = 2 case, proved on a different route and consequently in every dimension: Guo's hypothesis p ∈ [1, n) reads n > 2 at p = 2, excluding n = 1 and n = 2, because the GNS route needs a finite Sobolev conjugate. The route here goes through the one-dimensional inequality and Fubini, which asks nothing of the dimension, with the constant L²/(2(n+1)) in place of the sharp one.

theorem EllipticPdes.Poincare.laplaceBilin_coercive_of_bounded {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin (n + 1)))} (hΩb : Bornology.IsBounded Ω) : IsCoercive (laplaceBilin Ω)

Coercivity of the bilinear form of the Laplacian on a bounded domain, with no abstract Poincaré hypothesis. poincare_H01_of_bounded names the constant, so the only input is boundedness of Ω. This is the form of coercivity the direct method uses, where the domain is a ball and no box structure is at hand.