Density extension to H₀¹ (dependency-chain step 4)

The Poincaré inequality, once established for every smooth compactly supported test function, extends to all of H₀¹(Ω) by density. The key structural facts (proved in Sobolev/Basic.lean) are that the test-function graphs already form a submodule (span_testGraphSet) and that H₀¹(Ω) is their topological closure. The Poincaré estimate is the condition 0 ≤ Φ for a continuous function Φ, hence a closed condition; holding on the dense test functions, it passes to the closure.

The base estimate on test functions is taken as a hypothesis here (it is supplied by the domain Poincaré inequality poincare_domain rewritten through the L² norms). This keeps the density mechanism independent of the geometry of Ω.

theorem EllipticPdes.Poincare.poincare_H01 {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (C : ℝ) (hbase : ∀ {φ : EuclideanSpace ℝ (Fin d) → ℝ} (h : Sobolev.IsTestFn Ω φ), ‖h.testGraph.ofLp 0‖ ^ 2 ≤ C * ∑ i : Fin d, ‖h.testGraph.ofLp i.succ‖ ^ 2) {U : Sobolev.H1amb Ω} (hU : U ∈ Sobolev.H01 Ω) : ‖U.ofLp 0‖ ^ 2 ≤ C * ∑ i : Fin d, ‖U.ofLp i.succ‖ ^ 2

Density Poincaré inequality on H₀¹. If the Poincaré bound ‖φ‖²_{L²} ≤ C · ∑ᵢ ‖∂ᵢφ‖²_{L²} holds for every test function φ (phrased through the graph coordinates testGraph 0 and testGraph i.succ), then it holds for every element of H₀¹(Ω): the function part U 0 is controlled by the gradient part U ∘ Fin.succ.