Per-coordinate-direction bound via Fubini (dependency-chain step 2)

Apply the one-dimensional Poincaré inequality (MeasureTheory.poincare_1d) on each coordinate slice of a box and integrate the remaining variables out.

A box Ω = B ×ˢ (a, b) ⊆ β × ℝ is integrated over by Fubini as ∫_Ω f = ∫_{y ∈ B} ∫_{x ∈ (a,b)} f (y, x). On each slice x ↦ f (y, x) the one-dimensional Poincaré inequality controls the L² norm by the L² norm of the slice derivative ∂_x f. Integrating that estimate over the remaining variables y gives the per-direction bound on the box.

• poincare_slice_iterated: the bound in iterated form, for a general measure on the remaining variables. This is the Fubini-decomposed statement.
• poincare_slice_box: the same bound written as a single integral over the box B ×ˢ (a, b), obtained from the iterated form by Fubini (setIntegral_prod).

theorem EllipticPdes.Poincare.poincare_slice_iterated {β : Type u_1} [MeasurableSpace β] {ν : MeasureTheory.Measure β} {a b : ℝ} (hab : a ≤ b) {Φ Φ' : β → ℝ → ℝ} (hderiv : ∀ (y : β), ∀ x ∈ Set.uIcc a b, HasDerivAt (Φ y) (Φ' y x) x) (hcont : ∀ (y : β), ContinuousOn (Φ' y) (Set.uIcc a b)) (hzero : ∀ (y : β), Φ y a = 0) (hg : MeasureTheory.Integrable (fun (y : β) => ∫ (x : ℝ) in a..b, Φ y x ^ 2) ν) (hh : MeasureTheory.Integrable (fun (y : β) => ∫ (x : ℝ) in a..b, Φ' y x ^ 2) ν) : ∫ (y : β), ∫ (x : ℝ) in a..b, Φ y x ^ 2 ∂ν ≤ (b - a) ^ 2 / 2 * ∫ (y : β), ∫ (x : ℝ) in a..b, Φ' y x ^ 2 ∂ν

The per-direction Poincaré bound in iterated form. For a family of one-dimensional slices x ↦ Φ y x, each satisfying the Poincaré hypotheses on [a, b] (a derivative Φ' y continuous on [a, b], vanishing at a), the integral over the remaining variables y of the slice L² norms is bounded by the same integral of the slice derivative L² norms.

theorem EllipticPdes.Poincare.poincare_slice_box {β : Type u_1} [MeasurableSpace β] {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {a b : ℝ} (hab : a ≤ b) {s : Set β} (hs : MeasurableSet s) {Φ Φ' : β × ℝ → ℝ} (hderiv : ∀ (y : β), ∀ x ∈ Set.uIcc a b, HasDerivAt (fun (t : ℝ) => Φ (y, t)) (Φ' (y, x)) x) (hcont : ∀ (y : β), ContinuousOn (fun (t : ℝ) => Φ' (y, t)) (Set.uIcc a b)) (hzero : ∀ (y : β), Φ (y, a) = 0) (hΦ2 : MeasureTheory.IntegrableOn (fun (p : β × ℝ) => Φ p ^ 2) (s ×ˢ Set.Ioo a b) (ν.prod MeasureTheory.volume)) (hΦ'2 : MeasureTheory.IntegrableOn (fun (p : β × ℝ) => Φ' p ^ 2) (s ×ˢ Set.Ioo a b) (ν.prod MeasureTheory.volume)) : ∫ (p : β × ℝ) in s ×ˢ Set.Ioo a b, Φ p ^ 2 ∂ν.prod MeasureTheory.volume ≤ (b - a) ^ 2 / 2 * ∫ (p : β × ℝ) in s ×ˢ Set.Ioo a b, Φ' p ^ 2 ∂ν.prod MeasureTheory.volume

The per-direction Poincaré bound on a box B ×ˢ (a, b) ⊆ β × ℝ, written as a single integral over the box. For a function Φ whose one-dimensional slices x ↦ Φ (y, x) are C¹ on [a, b] with derivative ∂_x Φ = Φ' continuous and Φ (y, a) = 0, ∫_{B ×ˢ (a,b)} Φ² ≤ (b - a)² / 2 * ∫_{B ×ˢ (a,b)} (∂_x Φ)².

Fubini (setIntegral_prod) reduces both sides to iterated integrals; the one-dimensional Poincaré inequality bounds each slice; integrating over B gives the result.

theorem EllipticPdes.Poincare.poincare_slice_box_fst {β : Type u_1} [MeasurableSpace β] {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {a b : ℝ} (hab : a ≤ b) {s : Set β} (hs : MeasurableSet s) {Φ Φ' : ℝ × β → ℝ} (hderiv : ∀ (y : β), ∀ x ∈ Set.uIcc a b, HasDerivAt (fun (t : ℝ) => Φ (t, y)) (Φ' (x, y)) x) (hcont : ∀ (y : β), ContinuousOn (fun (t : ℝ) => Φ' (t, y)) (Set.uIcc a b)) (hzero : ∀ (y : β), Φ (a, y) = 0) (hΦ2 : MeasureTheory.IntegrableOn (fun (p : ℝ × β) => Φ p ^ 2) (Set.Ioo a b ×ˢ s) (MeasureTheory.volume.prod ν)) (hΦ'2 : MeasureTheory.IntegrableOn (fun (p : ℝ × β) => Φ' p ^ 2) (Set.Ioo a b ×ˢ s) (MeasureTheory.volume.prod ν)) : ∫ (p : ℝ × β) in Set.Ioo a b ×ˢ s, Φ p ^ 2 ∂MeasureTheory.volume.prod ν ≤ (b - a) ^ 2 / 2 * ∫ (p : ℝ × β) in Set.Ioo a b ×ˢ s, Φ' p ^ 2 ∂MeasureTheory.volume.prod ν

The per-direction Poincaré bound on a box (a, b) ×ˢ B ⊆ ℝ × β, with the Poincaré direction the first coordinate. This is poincare_slice_box with the two factors swapped; it lets either coordinate of a binary product be the distinguished Poincaré direction.

theorem EllipticPdes.Poincare.poincare_box_dir {n : ℕ} (i : Fin (n + 1)) {a b : Fin (n + 1) → ℝ} (hab : a i ≤ b i) {u u' : (Fin (n + 1) → ℝ) → ℝ} (hderiv : ∀ (y : Fin n → ℝ), ∀ t ∈ Set.uIcc (a i) (b i), HasDerivAt (fun (s : ℝ) => u (i.insertNth s y)) (u' (i.insertNth t y)) t) (hcont : ∀ (y : Fin n → ℝ), ContinuousOn (fun (s : ℝ) => u' (i.insertNth s y)) (Set.uIcc (a i) (b i))) (hzero : ∀ (y : Fin n → ℝ), u (i.insertNth (a i) y) = 0) (hu2 : MeasureTheory.IntegrableOn (fun (x : Fin (n + 1) → ℝ) => u x ^ 2) (Set.univ.pi fun (k : Fin (n + 1)) => Set.Ioo (a k) (b k)) MeasureTheory.volume) (hu'2 : MeasureTheory.IntegrableOn (fun (x : Fin (n + 1) → ℝ) => u' x ^ 2) (Set.univ.pi fun (k : Fin (n + 1)) => Set.Ioo (a k) (b k)) MeasureTheory.volume) : ∫ (x : Fin (n + 1) → ℝ) in Set.univ.pi fun (k : Fin (n + 1)) => Set.Ioo (a k) (b k), u x ^ 2 ≤ (b i - a i) ^ 2 / 2 * ∫ (x : Fin (n + 1) → ℝ) in Set.univ.pi fun (k : Fin (n + 1)) => Set.Ioo (a k) (b k), u' x ^ 2

Per-direction Poincaré bound on a box in Fin (n+1) → ℝ. Isolating coordinate i, the slice through any point y of the remaining coordinates, varying coordinate i over [a i, b i], is C¹ with derivative u' and vanishes at the left face i-th coordinate = a i. Then ∫_Ω u² ≤ (b i - a i)² / 2 * ∫_Ω (u')² over the box Ω = ∏ₖ (a k, b k).

The box integral is transported through MeasurableEquiv.piFinSuccAbove, which isolates coordinate i as the first factor of ℝ × (Fin n → ℝ), and the result follows from poincare_slice_box_fst.