Coarse-graining support: Support.Besov.Poincare.HarmonicGradient.Definitions

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

Vector projected dual mean-zero Poincare estimate

The note-facing Caccioppoli wrappers need a Poincare estimate that controls the oscillation of a scalar field by the dual norm of its full gradient on each descendant.

The pre-existing scalar/componentwise version CubeDescendantProjectedDualMeanZeroPoincareEstimate is mathematically too strong when applied to a single coordinate of a gradient: an affine function u(x) = x_j (with j ≠ i) has zero i-th partial derivative but nonzero oscillation, so the componentwise statement is false in general.

This file introduces the correct vector replacement: a sum-over-coordinates form whose right-hand side controls every component of the gradient. It mirrors the scalar to_localEstimate consumer pattern from Poincare/Descendants.lean so the existing multiscale corridor can absorb it after summing the per-component bounds.

The underlying inequality ‖u − ⟨u⟩_R‖_{L²(R)} ≲ ∑_i ‖∂_i u‖_{B^{-1}_{2,1}(R)} is a pure duality fact about H¹ (proved by pairing against mean-zero L² test, integration by parts, and constant-coefficient Dirichlet regularity). Harmonicity is not required.

This file is layered under Besov/, so it does not import any PDE/, Sobolev/, or Deterministic/ content. The load-bearing analytic constructor of_h1Function, together with the harmonic-function corollary of_aHarmonicFunction, lives downstream in Deterministic/CoarseCaccioppoli/SingleCubeToRaw/HarmonicCanonicalGradient.lean (where the H1Function and AHarmonicFunction types are in scope).

def HCPolySupport.CubeDescendantProjectedDualMeanZeroVectorPoincareEstimate {d : ℕ} (Q : TriadicCube d) (C : ℝ) (u : Vec d → ℝ) (G : Vec d → Vec d) (M : ℕ) : Prop

The L² oscillation of u on each descendant through depth M is bounded by C times the sum of the dual mean-zero seminorms of the projected components of G.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.CubeProjectedDualMeanZeroVectorPoincareEstimate {d : ℕ} (Q : TriadicCube d) (C : ℝ) (u : Vec d → ℝ) (G : Vec d → Vec d) (N : ℕ) : Prop

The single-cube projected vector dual mean-zero Poincare estimate. This is the local theorem that the descendant estimate applies on each subcube.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.CubeDualMeanZeroVectorPoincareEstimate {d : ℕ} (Q : TriadicCube d) (C : ℝ) (u : Vec d → ℝ) (G : Vec d → Vec d) : Prop

Infinite-depth vector dual mean-zero Poincare estimate.

This is the analytically natural target for general H¹ functions: the oscillation is controlled by the full negative Besov seminorm of each gradient component, not by a fixed finite projection depth.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.CubeDescendantDualMeanZeroVectorPoincareEstimate {d : ℕ} (Q : TriadicCube d) (C : ℝ) (u : Vec d → ℝ) (G : Vec d → Vec d) (M : ℕ) : Prop

Descendant form of the infinite-depth vector dual mean-zero Poincare estimate.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.CubeDualFullVectorPoincareEstimate {d : ℕ} (Q : TriadicCube d) (C : ℝ) (u : Vec d → ℝ) (G : Vec d → Vec d) : Prop

Constant-mode-safe infinite-depth vector Poincare estimate.

The right-hand side uses the full dual norm of each gradient component. Unlike the mean-zero-dual-only target, this norm sees constant gradient modes and is therefore the corrected surface for arbitrary H¹ inputs.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.CubeDescendantDualFullVectorPoincareEstimate {d : ℕ} (Q : TriadicCube d) (C : ℝ) (u : Vec d → ℝ) (G : Vec d → Vec d) (M : ℕ) : Prop

Descendant form of the constant-mode-safe full-dual vector Poincare estimate.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.CubeLocalMultiscalePoincareVectorEstimate {d : ℕ} (Q : TriadicCube d) (C : ℝ) (u : Vec d → ℝ) (G : Vec d → Vec d) (M : ℕ) : Prop

Vector analogue of CubeLocalMultiscalePoincareEstimate: oscillation of the scalar u is controlled by C times the sum over coordinates of the local q = 1 partial circ norm at the matching multiscale depth.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.CubeLocalFullCircPoincareVectorEstimate {d : ℕ} (Q : TriadicCube d) (C : ℝ) (u : Vec d → ℝ) (G : Vec d → Vec d) (M : ℕ) : Prop

Vector local Poincare estimate with the full local circ norm on each descendant. This is the honest bridge target produced by a full-dual Poincare estimate; passing from this to the finite-partial multiscale corridor requires a separate infinite-to-finite summation argument.

Equations

• One or more equations did not get rendered due to their size.