Coarse-graining support: Support.Sobolev.Foundations.CubePoisson.FullVectorPoincare

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

noncomputable def HCPolySupport.CubeFullVectorPoincareAnalyticInput.poissonSolutionFor {d : ℕ} {Q : TriadicCube d} (h : CubeFullVectorPoincareAnalyticInput Q) (u : H1Function (openCubeSet Q)) : MeanZeroNeumannPoissonSolution Q (H1Function.cubePoissonRhs Q u)

The chosen Neumann Poisson solution for the fluctuation right-hand side of an H¹ function, using the solver bundled in the full-dual analytic input.

Equations

• h.poissonSolutionFor u = Classical.choose ⋯

theorem HCPolySupport.CubeFullVectorPoincareAnalyticInput.poissonSolutionFor_equation {d : ℕ} {Q : TriadicCube d} (h : CubeFullVectorPoincareAnalyticInput Q) (u : H1Function (openCubeSet Q)) (φ : H1MeanZeroFunction (openCubeSet Q)) : ∫ (x : Vec d) in openCubeSet Q, vecDot ((h.poissonSolutionFor u).w.toH1Function.grad x) (φ.toH1Function.grad x) = ∫ (x : Vec d) in openCubeSet Q, H1Function.cubePoissonRhs Q u x * φ.toH1Function.toFun x

theorem HCPolySupport.CubeFullVectorPoincareAnalyticInput.poissonSolutionFor_equation_toMeanZeroOnCube {d : ℕ} {Q : TriadicCube d} (h : CubeFullVectorPoincareAnalyticInput Q) (u : H1Function (openCubeSet Q)) : ∫ (x : Vec d) in openCubeSet Q, vecDot ((h.poissonSolutionFor u).w.toH1Function.grad x) (u.grad x) = ∫ (x : Vec d) in openCubeSet Q, H1Function.cubePoissonRhs Q u x * H1Function.cubePoissonRhs Q u x

The Poisson equation tested against the mean-zero representative of u.

theorem HCPolySupport.CubeFullVectorPoincareAnalyticInput.integral_poissonGradient_vecDot_grad_eq_sum_coord {d : ℕ} {Q : TriadicCube d} (h : CubeFullVectorPoincareAnalyticInput Q) (u : H1Function (openCubeSet Q)) : ∫ (x : Vec d) in openCubeSet Q, vecDot ((h.poissonSolutionFor u).w.toH1Function.grad x) (u.grad x) = ∑ i : Fin d, ∫ (x : Vec d) in openCubeSet Q, (h.poissonSolutionFor u).w.toH1Function.grad x i * u.grad x i

Coordinate expansion of the Poisson-gradient energy pairing.

theorem HCPolySupport.CubeFullVectorPoincareAnalyticInput.poissonSolutionFor_equation_toMeanZeroOnCube_sum_coord {d : ℕ} {Q : TriadicCube d} (h : CubeFullVectorPoincareAnalyticInput Q) (u : H1Function (openCubeSet Q)) : ∑ i : Fin d, ∫ (x : Vec d) in openCubeSet Q, (h.poissonSolutionFor u).w.toH1Function.grad x i * u.grad x i = ∫ (x : Vec d) in openCubeSet Q, H1Function.cubePoissonRhs Q u x * H1Function.cubePoissonRhs Q u x

The tested Poisson equation in coordinate-sum form.

theorem HCPolySupport.CubeFullVectorPoincareAnalyticInput.poissonSolutionFor_equation_toMeanZeroOnCube_sum_pairing {d : ℕ} {Q : TriadicCube d} (h : CubeFullVectorPoincareAnalyticInput Q) (u : H1Function (openCubeSet Q)) : (cubeVolume Q * ∑ i : Fin d, cubeBesovPairing Q (fun (x : Vec d) => u.grad x i) fun (x : Vec d) => (h.poissonSolutionFor u).w.toH1Function.grad x i) = ∫ (x : Vec d) in openCubeSet Q, H1Function.cubePoissonRhs Q u x * H1Function.cubePoissonRhs Q u x

The tested Poisson equation rewritten in normalized Besov-pairing form.

theorem HCPolySupport.CubeFullVectorPoincareAnalyticInput.poissonSolutionFor_cz {d : ℕ} {Q : TriadicCube d} (h : CubeFullVectorPoincareAnalyticInput Q) (u : H1Function (openCubeSet Q)) : (∑ i : Fin d, cubeBesovCircNorm Q 1 2 ⊤ fun (x : Vec d) => (h.poissonSolutionFor u).w.toH1Function.grad x i) ≤ h.czConstant * cubeLpNorm Q 2 (H1Function.cubePoissonRhs Q u)

Calderon-Zygmund control for the chosen Poisson solution associated to an H¹ function's fluctuation right-hand side.

theorem HCPolySupport.CubeFullVectorPoincareAnalyticInput.gradient_duality_poissonSolutionFor {d : ℕ} {Q : TriadicCube d} (h : CubeFullVectorPoincareAnalyticInput Q) (u : H1Function (openCubeSet Q)) : ∑ i : Fin d, |cubeBesovPairing Q (fun (x : Vec d) => u.grad x i) fun (x : Vec d) => (h.poissonSolutionFor u).w.toH1Function.grad x i| ≤ (h.dualityConstant * ∑ i : Fin d, cubeBesovDualFullNorm Q 1 2 1 fun (x : Vec d) => u.grad x i) * ∑ i : Fin d, cubeBesovCircNorm Q 1 2 ⊤ fun (x : Vec d) => (h.poissonSolutionFor u).w.toH1Function.grad x i

Endpoint Besov duality between an H¹ gradient and the gradient of the chosen Neumann Poisson solution, using the full negative Besov norm.

theorem HCPolySupport.CubeFullVectorPoincareAnalyticInput.abs_gradient_pairing_sum_poissonSolutionFor_le {d : ℕ} {Q : TriadicCube d} (h : CubeFullVectorPoincareAnalyticInput Q) (u : H1Function (openCubeSet Q)) : |∑ i : Fin d, cubeBesovPairing Q (fun (x : Vec d) => u.grad x i) fun (x : Vec d) => (h.poissonSolutionFor u).w.toH1Function.grad x i| ≤ (h.dualityConstant * ∑ i : Fin d, cubeBesovDualFullNorm Q 1 2 1 fun (x : Vec d) => u.grad x i) * ∑ i : Fin d, cubeBesovCircNorm Q 1 2 ⊤ fun (x : Vec d) => (h.poissonSolutionFor u).w.toH1Function.grad x i

Endpoint-duality bound for the full gradient pairing sum against the chosen Poisson solution.

theorem HCPolySupport.CubeFullVectorPoincareAnalyticInput.abs_gradient_pairing_sum_poissonSolutionFor_le_cz {d : ℕ} {Q : TriadicCube d} (h : CubeFullVectorPoincareAnalyticInput Q) (u : H1Function (openCubeSet Q)) (hdualNonneg : 0 ≤ ∑ i : Fin d, cubeBesovDualFullNorm Q 1 2 1 fun (x : Vec d) => u.grad x i) : |∑ i : Fin d, cubeBesovPairing Q (fun (x : Vec d) => u.grad x i) fun (x : Vec d) => (h.poissonSolutionFor u).w.toH1Function.grad x i| ≤ (h.dualityConstant * ∑ i : Fin d, cubeBesovDualFullNorm Q 1 2 1 fun (x : Vec d) => u.grad x i) * (h.czConstant * cubeLpNorm Q 2 (H1Function.cubePoissonRhs Q u))

Full-gradient Poisson pairing bound after inserting the Calderon-Zygmund estimate for the chosen Poisson solution.

theorem HCPolySupport.CubeFullVectorPoincareAnalyticInput.abs_gradient_pairing_sum_poissonSolutionFor_le_cz_grouped {d : ℕ} {Q : TriadicCube d} (h : CubeFullVectorPoincareAnalyticInput Q) (u : H1Function (openCubeSet Q)) (hdualNonneg : 0 ≤ ∑ i : Fin d, cubeBesovDualFullNorm Q 1 2 1 fun (x : Vec d) => u.grad x i) : |∑ i : Fin d, cubeBesovPairing Q (fun (x : Vec d) => u.grad x i) fun (x : Vec d) => (h.poissonSolutionFor u).w.toH1Function.grad x i| ≤ (h.dualityConstant * h.czConstant * ∑ i : Fin d, cubeBesovDualFullNorm Q 1 2 1 fun (x : Vec d) => u.grad x i) * cubeLpNorm Q 2 (H1Function.cubePoissonRhs Q u)

Constant-grouped version of abs_gradient_pairing_sum_poissonSolutionFor_le_cz.

theorem HCPolySupport.CubeFullVectorPoincareAnalyticInput.poissonEnergy_le_cubeVolume_mul_abs_gradient_pairing_sum {d : ℕ} {Q : TriadicCube d} (h : CubeFullVectorPoincareAnalyticInput Q) (u : H1Function (openCubeSet Q)) : ∫ (x : Vec d) in openCubeSet Q, H1Function.cubePoissonRhs Q u x * H1Function.cubePoissonRhs Q u x ≤ cubeVolume Q * |∑ i : Fin d, cubeBesovPairing Q (fun (x : Vec d) => u.grad x i) fun (x : Vec d) => (h.poissonSolutionFor u).w.toH1Function.grad x i|

The squared fluctuation energy is bounded by the absolute full-gradient Poisson pairing sum.

theorem HCPolySupport.CubeFullVectorPoincareAnalyticInput.poissonEnergy_le_full_duality_cz {d : ℕ} {Q : TriadicCube d} (h : CubeFullVectorPoincareAnalyticInput Q) (u : H1Function (openCubeSet Q)) (hdualNonneg : 0 ≤ ∑ i : Fin d, cubeBesovDualFullNorm Q 1 2 1 fun (x : Vec d) => u.grad x i) : ∫ (x : Vec d) in openCubeSet Q, H1Function.cubePoissonRhs Q u x * H1Function.cubePoissonRhs Q u x ≤ cubeVolume Q * ((h.dualityConstant * h.czConstant * ∑ i : Fin d, cubeBesovDualFullNorm Q 1 2 1 fun (x : Vec d) => u.grad x i) * cubeLpNorm Q 2 (H1Function.cubePoissonRhs Q u))

Squared fluctuation energy bounded by the full endpoint-duality and Calderon-Zygmund constants.

theorem HCPolySupport.CubeFullVectorPoincareAnalyticInput.cubeLpNorm_cubePoissonRhs_le_full_duality_cz {d : ℕ} {Q : TriadicCube d} (h : CubeFullVectorPoincareAnalyticInput Q) (u : H1Function (openCubeSet Q)) (hdualNonneg : 0 ≤ ∑ i : Fin d, cubeBesovDualFullNorm Q 1 2 1 fun (x : Vec d) => u.grad x i) : cubeLpNorm Q 2 (H1Function.cubePoissonRhs Q u) ≤ h.dualityConstant * h.czConstant * ∑ i : Fin d, cubeBesovDualFullNorm Q 1 2 1 fun (x : Vec d) => u.grad x i

Normalized L² fluctuation estimate obtained from the full endpoint duality and Calderon-Zygmund inputs. This is the analytic core of the full-dual infinite-depth vector Poincare theorem.

theorem HCPolySupport.CubeFullVectorPoincareAnalyticInput.dualFullVectorPoincareEstimate_of_h1Function {d : ℕ} {Q : TriadicCube d} (h : CubeFullVectorPoincareAnalyticInput Q) (u : H1Function (openCubeSet Q)) (hdualNonneg : 0 ≤ ∑ i : Fin d, cubeBesovDualFullNorm Q 1 2 1 fun (x : Vec d) => u.grad x i) : CubeDualFullVectorPoincareEstimate Q (h.dualityConstant * h.czConstant) (fun (x : Vec d) => u.toFun x) fun (x : Vec d) => u.grad x

Infinite-depth vector Poincare estimate with the natural constant supplied by the cube-local full-dual analytic input bundle.