Coarse-graining support: Support.Book.Ch03.Theorems.CoarsePoincare

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Section 3.1.1: Coarse-grained Poincare inequality

This file contains the public note-facing coarse Poincare theorem package. Helper estimates live in the CoarsePoincare/ submodules.

Audit tag

Claim: prove and package the Book-facing coarse Poincare estimate for solution gradients and energy density on triadic cubes.

Downstream target: Chapter 3 public theorem aggregation and later inhomogeneous estimates. This file should keep one CoarsePoincareTheory surface; helper estimates belong in the CoarsePoincare/ submodules.

theorem HCPolySupport.Book.Ch03.coarsePoincareGradient_negativeBesov_le {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffFamily d) {s : ℝ} {q : Ch02.MultiscaleExponent} (u : CubeSolution Q a) (hs : 0 < s) (hq : q.IsAdmissible) : scaleNormalizedNegativeBesovVectorNorm Q s q (solutionGradientField u) ≤ coarsePoincareGradientRHS Q a s q u

Gradient part of the note-facing coarse-grained Poincare theorem.

The proved API is uniform for every s > 0, and therefore strengthens the ABK26/source range 0 < s ≤ 1; it is not presented as a literal identity of ranges. In particular, admissible q includes the endpoint s = 1, q = 2.

theorem HCPolySupport.Book.Ch03.coarsePoincareFlux_negativeBesov_le {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffFamily d) {s : ℝ} {q : Ch02.MultiscaleExponent} (u : CubeSolution Q a) (hs : 0 < s) (hq : q.IsAdmissible) : scaleNormalizedNegativeBesovVectorNorm Q s q (solutionFluxField Q a u) ≤ coarsePoincareFluxRHS Q a s q u

Flux part of the note-facing coarse-grained Poincare theorem.

The proved API is uniform for every s > 0, and therefore strengthens the ABK26/source range 0 < s ≤ 1; it is not presented as a literal identity of ranges. In particular, admissible q includes the endpoint s = 1, q = 2.

structure HCPolySupport.Book.Ch03.CoarsePoincareTheory {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffFamily d) : Prop

Public theorem package for the gradient and flux coarse-grained Poincare inequalities.

Its proved API is uniform for every s > 0, hence strengthens the ABK26/source range 0 < s ≤ 1 without claiming literal identity of ranges. Admissible q includes the endpoint s = 1, q = 2.

• gradient_negativeBesov_le {s : ℝ} {q : Ch02.MultiscaleExponent} (u : CubeSolution Q a) : 0 < s → q.IsAdmissible → scaleNormalizedNegativeBesovVectorNorm Q s q (solutionGradientField u) ≤ coarsePoincareGradientRHS Q a s q u
• flux_negativeBesov_le {s : ℝ} {q : Ch02.MultiscaleExponent} (u : CubeSolution Q a) : 0 < s → q.IsAdmissible → scaleNormalizedNegativeBesovVectorNorm Q s q (solutionFluxField Q a u) ≤ coarsePoincareFluxRHS Q a s q u

theorem HCPolySupport.Book.Ch03.coarsePoincareTheory {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffFamily d) : CoarsePoincareTheory Q a

Fully proved public coarse-grained Poincare theorem.