Coarse-graining support: Support.Sobolev.Foundations.CubeBesovPoincare

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

Cube Besov-Poincare bridge for H¹ functions

This file exposes the constant-mode-safe full-dual vector Poincare interface for scalar H¹ functions on cubes. It is deliberately upstream of the deterministic Caccioppoli files: the theorem is a pure Sobolev/Besov statement, with the Neumann/CZ input isolated in the cube Poisson endpoint package.

theorem HCPolySupport.h1Function_dualFullGradientSum_nonneg {d : ℕ} (Q : TriadicCube d) (u : H1Function (openCubeSet Q)) : 0 ≤ ∑ i : Fin d, cubeBesovDualFullNorm Q 1 2 1 fun (x : Vec d) => u.grad x i

theorem HCPolySupport.CubeDualFullVectorPoincareEstimate.of_h1Function_of_analyticInput {d : ℕ} (Q : TriadicCube d) (u : H1Function (openCubeSet Q)) (h : CubeFullVectorPoincareAnalyticInput Q) (C : ℝ) (hC : h.dualityConstant * h.czConstant ≤ C) : CubeDualFullVectorPoincareEstimate Q C (fun (x : Vec d) => u.toFun x) fun (x : Vec d) => u.grad x

theorem HCPolySupport.CubeDualFullVectorPoincareEstimate.of_h1Function_of_l2AnalyticInput {d : ℕ} (Q : TriadicCube d) (u : H1Function (openCubeSet Q)) (h : CubeFullVectorPoincareL2AnalyticInput Q) (C : ℝ) (hC : h.endpointConstant ≤ C) : CubeDualFullVectorPoincareEstimate Q C (fun (x : Vec d) => u.toFun x) fun (x : Vec d) => u.grad x

Full-dual vector Poincare from the direct L² endpoint analytic bundle. This is the corrected package boundary after the endpoint estimate has already absorbed the Neumann CZ bound.

theorem HCPolySupport.exists_cubeNeumannPoissonGradientBesovEstimate {d : ℕ} (Q : TriadicCube d) : ∃ (C : ℝ), CubeNeumannPoissonGradientBesovEstimate Q C

Constant for the cube Neumann Calderon-Zygmund B¹_{2,∞} estimate.

noncomputable def HCPolySupport.cubeNeumannPoissonGradientBesovConstant {d : ℕ} (Q : TriadicCube d) : ℝ

Chosen constant for the cube Neumann Calderon-Zygmund B¹_{2,∞} estimate.

Equations

• HCPolySupport.cubeNeumannPoissonGradientBesovConstant Q = Classical.choose ⋯

theorem HCPolySupport.cubeNeumannPoissonGradientBesovEstimate {d : ℕ} (Q : TriadicCube d) : CubeNeumannPoissonGradientBesovEstimate Q (cubeNeumannPoissonGradientBesovConstant Q)

Cube Neumann Calderon-Zygmund B¹_{2,∞} estimate.

noncomputable def HCPolySupport.cubePoissonGradientDualTestNormL2CoreConstant {d : ℕ} (_Q : TriadicCube d) : ℝ

Chosen constant for the direct L² Poisson-gradient positive dual test-norm core estimate.

Equations

• HCPolySupport.cubePoissonGradientDualTestNormL2CoreConstant _Q = HCPolySupport.Legacy.cubeNeumannW22CalderonZygmundConstant d

theorem HCPolySupport.cubePoissonGradientDualTestNormL2CoreEstimate {d : ℕ} (Q : TriadicCube d) : CubePoissonGradientDualTestNormL2CoreEstimate Q (cubePoissonGradientDualTestNormL2CoreConstant Q)

Direct L² positive dual test-norm core estimate for Poisson gradients.

noncomputable def HCPolySupport.cubePoissonGradientDualTestNormL2Constant {d : ℕ} (Q : TriadicCube d) : ℝ

Chosen constant for the direct L² Poisson-gradient positive dual test-norm estimate. The factor d is the cost of converting a componentwise core bound into the summed strictly positive B package.

Equations

• HCPolySupport.cubePoissonGradientDualTestNormL2Constant Q = ↑d * HCPolySupport.cubePoissonGradientDualTestNormL2CoreConstant Q

theorem HCPolySupport.cubePoissonGradientDualTestNormL2Estimate {d : ℕ} (Q : TriadicCube d) : CubePoissonGradientDualTestNormL2Estimate Q (cubePoissonGradientDualTestNormL2Constant Q)

Direct L² positive dual test-norm estimate for Poisson gradients, including the strict-positive B packaging used by endpoint duality.

noncomputable def HCPolySupport.cubePoissonGradientFullL2EndpointDualityConstant {d : ℕ} (Q : TriadicCube d) : ℝ

Chosen constant for the full-dual L² endpoint estimate.

Equations

• HCPolySupport.cubePoissonGradientFullL2EndpointDualityConstant Q = HCPolySupport.cubePoissonGradientDualTestNormL2Constant Q

theorem HCPolySupport.cubePoissonGradientFullL2EndpointDuality {d : ℕ} (Q : TriadicCube d) : CubePoissonGradientFullL2EndpointDuality Q (cubePoissonGradientFullL2EndpointDualityConstant Q)

Full-dual Poisson-gradient endpoint estimate with the Poisson-gradient side already controlled by the normalized L² size of the right-hand side.

noncomputable def HCPolySupport.cubeFullVectorPoincareL2AnalyticInput {d : ℕ} (Q : TriadicCube d) : CubeFullVectorPoincareL2AnalyticInput Q

Assemble the direct L² endpoint analytic input from its named field-level dependencies.

Equations

• HCPolySupport.cubeFullVectorPoincareL2AnalyticInput Q = { poisson := ⋯, endpointConstant := HCPolySupport.cubePoissonGradientFullL2EndpointDualityConstant Q, endpoint := ⋯ }

noncomputable def HCPolySupport.cubeFullVectorPoincareAnalyticConstant {d : ℕ} (Q : TriadicCube d) : ℝ

Exact one-cube constant selected by the corrected direct L² endpoint input.

Equations

• HCPolySupport.cubeFullVectorPoincareAnalyticConstant Q = HCPolySupport.cubePoissonGradientFullL2EndpointDualityConstant Q

theorem HCPolySupport.cubeFullVectorPoincareAnalyticConstant_nonneg {d : ℕ} (Q : TriadicCube d) : 0 ≤ cubeFullVectorPoincareAnalyticConstant Q

theorem HCPolySupport.cubeFullVectorPoincareAnalyticConstant_eq_fullL2EndpointDualityConstant {d : ℕ} (Q : TriadicCube d) : cubeFullVectorPoincareAnalyticConstant Q = cubePoissonGradientFullL2EndpointDualityConstant Q

theorem HCPolySupport.cubeFullVectorPoincareAnalyticConstant_eq_dimensionConstant {d : ℕ} (Q : TriadicCube d) : cubeFullVectorPoincareAnalyticConstant Q = ↑d * Legacy.cubeNeumannW22CalderonZygmundConstant d

theorem HCPolySupport.cubeFullVectorPoincareAnalyticConstant_eq_of_same_dimension {d : ℕ} (Q R : TriadicCube d) : cubeFullVectorPoincareAnalyticConstant Q = cubeFullVectorPoincareAnalyticConstant R

theorem HCPolySupport.CubeDualFullVectorPoincareEstimate.of_h1Function_analyticConstant {d : ℕ} (Q : TriadicCube d) (u : H1Function (openCubeSet Q)) : CubeDualFullVectorPoincareEstimate Q (cubeFullVectorPoincareAnalyticConstant Q) (fun (x : Vec d) => u.toFun x) fun (x : Vec d) => u.grad x

Single-cube full-dual vector Poincare with the exact selected corrected analytic constant.

theorem HCPolySupport.CubeDualFullVectorPoincareEstimate.of_h1Function_fullL2EndpointConstant {d : ℕ} (Q : TriadicCube d) (u : H1Function (openCubeSet Q)) : CubeDualFullVectorPoincareEstimate Q (cubePoissonGradientFullL2EndpointDualityConstant Q) (fun (x : Vec d) => u.toFun x) fun (x : Vec d) => u.grad x

Single-cube full-dual vector Poincare stated with the selected direct L² endpoint constant. This is definitionally the same constant as cubeFullVectorPoincareAnalyticConstant, but the statement exposes the endpoint package that future proofs should aim to discharge.

theorem HCPolySupport.CubeDualFullVectorPoincareEstimate.of_h1Function_of_analyticConstant_le {d : ℕ} (Q : TriadicCube d) (u : H1Function (openCubeSet Q)) {C : ℝ} (hC : cubeFullVectorPoincareAnalyticConstant Q ≤ C) : CubeDualFullVectorPoincareEstimate Q C (fun (x : Vec d) => u.toFun x) fun (x : Vec d) => u.grad x

Single-cube full-dual vector Poincare with any constant dominating the exact selected corrected analytic constant.

theorem HCPolySupport.CubeDescendantDualFullVectorPoincareEstimate.of_h1Function_of_descendant_analyticConstant_le {d : ℕ} (Q : TriadicCube d) (u : H1Function (openCubeSet Q)) (N : ℕ) {C : ℝ} (hC : ∀ j ∈ Finset.range (N + 1), ∀ R ∈ descendantsAtDepth Q j, cubeFullVectorPoincareAnalyticConstant R ≤ C) : CubeDescendantDualFullVectorPoincareEstimate Q C (cubeFluctuation Q fun (x : Vec d) => u.toFun x) (fun (x : Vec d) => u.grad x) N

Finite-depth descendant full-dual version using an explicit uniform bound on the selected corrected analytic constants over the descendants that occur up to depth N.

Uniform descendant analytic constants

theorem HCPolySupport.exists_cubeFullVectorPoincareUniformAnalyticConstant {d : ℕ} (Q : TriadicCube d) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, cubeFullVectorPoincareAnalyticConstant R ≤ C

Existence of a parent-cube constant that dominates the selected corrected full-dual analytic Poincare constants on all descendants of the parent. This is now a formal consequence of the dimension-uniform Neumann W2,2 / CZ constant.

noncomputable def HCPolySupport.cubeFullVectorPoincareUniformAnalyticConstant {d : ℕ} (_Q : TriadicCube d) : ℝ

Explicit dimension-only parent-cube constant dominating the selected corrected full-dual analytic constants on all descendants of the parent.

Equations

• HCPolySupport.cubeFullVectorPoincareUniformAnalyticConstant _Q = ↑d * HCPolySupport.Legacy.cubeNeumannW22CalderonZygmundConstant d

theorem HCPolySupport.cubeFullVectorPoincareUniformAnalyticConstant_nonneg {d : ℕ} (Q : TriadicCube d) : 0 ≤ cubeFullVectorPoincareUniformAnalyticConstant Q

theorem HCPolySupport.cubeFullVectorPoincareAnalyticConstant_le_uniformAnalyticConstant {d : ℕ} (Q : TriadicCube d) (j : ℕ) (R : TriadicCube d) (_hR : R ∈ descendantsAtDepth Q j) : cubeFullVectorPoincareAnalyticConstant R ≤ cubeFullVectorPoincareUniformAnalyticConstant Q

theorem HCPolySupport.CubeDescendantDualFullVectorPoincareEstimate.of_h1Function_uniformAnalyticConstant {d : ℕ} (Q : TriadicCube d) (u : H1Function (openCubeSet Q)) (N : ℕ) : CubeDescendantDualFullVectorPoincareEstimate Q (cubeFullVectorPoincareUniformAnalyticConstant Q) (cubeFluctuation Q fun (x : Vec d) => u.toFun x) (fun (x : Vec d) => u.grad x) N

All-depth descendant full-dual theorem with the selected corrected uniform analytic constant.

noncomputable def HCPolySupport.fullVectorPoincareCubeConstant {d : ℕ} (Q : TriadicCube d) : ℝ

Public cube Poincare constant for the corrected full-dual theorem. It is the selected parent-cube constant that dominates the exact full-dual analytic constants on all descendants.

Equations

• HCPolySupport.fullVectorPoincareCubeConstant Q = HCPolySupport.cubeFullVectorPoincareUniformAnalyticConstant Q

theorem HCPolySupport.fullVectorPoincareCubeConstant_nonneg {d : ℕ} (Q : TriadicCube d) : 0 ≤ fullVectorPoincareCubeConstant Q

theorem HCPolySupport.fullVectorPoincareCubeConstant_eq_dimensionConstant {d : ℕ} (Q : TriadicCube d) : fullVectorPoincareCubeConstant Q = ↑d * Legacy.cubeNeumannW22CalderonZygmundConstant d

theorem HCPolySupport.cubeFullVectorPoincareAnalyticConstant_le_fullVectorPoincareCubeConstant {d : ℕ} (Q : TriadicCube d) : cubeFullVectorPoincareAnalyticConstant Q ≤ fullVectorPoincareCubeConstant Q

theorem HCPolySupport.CubeDualFullVectorPoincareEstimate.of_h1Function {d : ℕ} (Q : TriadicCube d) (u : H1Function (openCubeSet Q)) : CubeDualFullVectorPoincareEstimate Q (fullVectorPoincareCubeConstant Q) (fun (x : Vec d) => u.toFun x) fun (x : Vec d) => u.grad x

theorem HCPolySupport.CubeDescendantDualFullVectorPoincareEstimate.of_h1Function {d : ℕ} (Q : TriadicCube d) (u : H1Function (openCubeSet Q)) (N : ℕ) : CubeDescendantDualFullVectorPoincareEstimate Q (fullVectorPoincareCubeConstant Q) (cubeFluctuation Q fun (x : Vec d) => u.toFun x) (fun (x : Vec d) => u.grad x) N

Descendant infinite-depth full-dual Poincare for an H¹ function, obtained from the corrected parent-cube uniform analytic constant on each descendant.