Discharging the box Poincaré slice bound from the Euclidean geometry

Poincare/Geometry.lean reduces coercivity of the bilinear form of the Laplacian on a domain Ω to the slice bound

∫_Ω φ² ≤ C · ∫_Ω (∂ᵢφ)² (hslice, every test function, every direction i),

phrased on EuclideanSpace ℝ (Fin (n+1)). The one-dimensional/Fubini machinery of Poincare/Fubini.lean proves exactly this bound, but on the plain product Fin (n+1) → ℝ with the pi-Lebesgue measure (poincare_box_dir). This file is the missing transport: it moves poincare_box_dir across the measure-preserving identification WithLp.toLp between Fin (n+1) → ℝ and EuclideanSpace ℝ (Fin (n+1)), turning it into the slice bound on a coordinate box, and hence into unconditional coercivity of the bilinear form of the Laplacian on that box.

The three bridges:

• toLp_insertNth_eq: a coordinate slice of the box, reconstructed through toLp, is the affine line c + s • eᵢ in EuclideanSpace. This identifies the 1-D slice derivative used by poincare_box_dir with the Fréchet partial partialD i φ (hasDerivAt_slice).
• the measure-preserving equivalence MeasurableEquiv.toLp (EuclideanSpace.volume_preserving …) transports the box integrals and the integrability hypotheses between the two spaces.
• the left-face values vanish because tsupport φ sits inside the open box.

The headline results are slice_bound_euclBox (the per-direction Poincaré bound on the box) and laplaceBilin_coercive_euclBox (Dirichlet coercivity on any open box, no abstract hypothesis).

def EllipticPdes.Poincare.euclBox {n : ℕ} (a b : Fin (n + 1) → ℝ) : Set (EuclideanSpace ℝ (Fin (n + 1)))

The open coordinate box ∏ₖ (aₖ, bₖ) inside EuclideanSpace ℝ (Fin (n+1)).

Equations

• EllipticPdes.Poincare.euclBox a b = {x : EuclideanSpace ℝ (Fin (n + 1)) | ∀ (k : Fin (n + 1)), x.ofLp k ∈ Set.Ioo (a k) (b k)}

theorem EllipticPdes.Poincare.isOpen_euclBox {n : ℕ} (a b : Fin (n + 1) → ℝ) : IsOpen (euclBox a b)

The open coordinate box is open: it is a finite intersection of coordinate preimages of open intervals.

theorem EllipticPdes.Poincare.toLp_insertNth_eq {n : ℕ} (i : Fin (n + 1)) (y : Fin n → ℝ) (s : ℝ) : WithLp.toLp 2 (i.insertNth s y) = WithLp.toLp 2 (i.insertNth 0 y) + s • EuclideanSpace.single i 1

A coordinate slice s ↦ i.insertNth s y, transported into EuclideanSpace by toLp, is the affine line toLp (i.insertNth 0 y) + s • eᵢ.

theorem EllipticPdes.Poincare.hasDerivAt_slice {n : ℕ} {φ : EuclideanSpace ℝ (Fin (n + 1)) → ℝ} (hφ : Differentiable ℝ φ) (i : Fin (n + 1)) (y : Fin n → ℝ) (t : ℝ) : HasDerivAt (fun (s : ℝ) => φ (WithLp.toLp 2 (i.insertNth s y))) (Sobolev.partialD i φ (WithLp.toLp 2 (i.insertNth t y))) t

The slice of a test function along coordinate i, reconstructed through toLp, is differentiable with derivative the i-th classical partial partialD i φ.

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

Per-direction Poincaré bound on an open box (the slice bound hslice). For a test function φ supported in the open box ∏ₖ (aₖ, bₖ) of EuclideanSpace ℝ (Fin (n+1)), ∫ φ² ≤ (bᵢ - aᵢ)² / 2 · ∫ (∂ᵢφ)². This is poincare_box_dir (the 1-D/Fubini bound on the plain product) transported across the measure-preserving toLp.

theorem EllipticPdes.Poincare.laplaceBilin_coercive_euclBox {n : ℕ} (a b : Fin (n + 1) → ℝ) (hab : ∀ (k : Fin (n + 1)), a k ≤ b k) (C : ℝ) (hC : ∀ (i : Fin (n + 1)), (b i - a i) ^ 2 / 2 ≤ C) : IsCoercive (laplaceBilin (euclBox a b))

Unconditional Dirichlet coercivity on an open box (the closing Examples remark of Evans §6.2.2, geometry supplied). With C an upper bound for every side contribution (bᵢ - aᵢ)² / 2, the Poisson (Dirichlet) form is coercive on H₀¹ of the open box ∏ₖ (aₖ, bₖ), with no abstract Poincaré hypothesis: the slice bound is discharged from the box geometry by slice_bound_euclBox.

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

Poincaré inequality on a box (Theorem thm: poincare). For every U ∈ H₀¹(Ω) of the open coordinate box Ω = ∏ₖ (aₖ, bₖ) whose side lengths are bounded by L,

‖u‖²_{L²(Ω)} ≤ L² / (2 (n + 1)) · ‖∇u‖²_{L²(Ω)},

i.e. ‖u‖_{L²} ≤ C_P ‖∇u‖_{L²} with C_P = L / √(2 (n + 1)); taking L the maximal side length gives the diameter-based constant. In the graph encoding the function part is U 0 and the gradient components are U i.succ. The chain is fully discharged from the box geometry: the one-dimensional/Fubini slice bound (slice_bound_euclBox, resting on poincare_box_dir) is averaged over the n + 1 directions (poincare_testfn) and extended from the test functions to H₀¹ by density (poincare_H01); no abstract Poincaré hypothesis remains.

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

The test-function instance of the box Poincaré inequality, in the slice-constant form the coercivity layer consumes: with every side contribution (bᵢ - aᵢ)² / 2 bounded by C, every test function on the box obeys the graph-coordinate bound with constant C / (n + 1). Derived from the box Poincaré inequality poincare_H01_euclBox applied to the test-function graph (which lies in H₀¹), with L = √(2C) bounding the sides.