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

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

noncomputable def HCPolySupport.CubeFullVectorPoincareL2AnalyticInput.poissonSolutionFor {d : ℕ} {Q : TriadicCube d} (h : CubeFullVectorPoincareL2AnalyticInput 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 with the direct L² endpoint input.

Equations

• h.poissonSolutionFor u = Classical.choose ⋯

theorem HCPolySupport.CubeFullVectorPoincareL2AnalyticInput.poissonSolutionFor_equation {d : ℕ} {Q : TriadicCube d} (h : CubeFullVectorPoincareL2AnalyticInput 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.CubeFullVectorPoincareL2AnalyticInput.poissonSolutionFor_equation_toMeanZeroOnCube {d : ℕ} {Q : TriadicCube d} (h : CubeFullVectorPoincareL2AnalyticInput 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 direct-L² Poisson equation tested against the mean-zero representative of u.

theorem HCPolySupport.CubeFullVectorPoincareL2AnalyticInput.integral_poissonGradient_vecDot_grad_eq_sum_coord {d : ℕ} {Q : TriadicCube d} (h : CubeFullVectorPoincareL2AnalyticInput 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 direct-L² Poisson-gradient energy pairing.

theorem HCPolySupport.CubeFullVectorPoincareL2AnalyticInput.poissonSolutionFor_equation_toMeanZeroOnCube_sum_coord {d : ℕ} {Q : TriadicCube d} (h : CubeFullVectorPoincareL2AnalyticInput 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 direct-L² tested Poisson equation in coordinate-sum form.

theorem HCPolySupport.CubeFullVectorPoincareL2AnalyticInput.poissonSolutionFor_equation_toMeanZeroOnCube_sum_pairing {d : ℕ} {Q : TriadicCube d} (h : CubeFullVectorPoincareL2AnalyticInput 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 direct-L² tested Poisson equation rewritten in normalized Besov-pairing form.

theorem HCPolySupport.CubeFullVectorPoincareL2AnalyticInput.gradient_l2Endpoint_poissonSolutionFor {d : ℕ} {Q : TriadicCube d} (h : CubeFullVectorPoincareL2AnalyticInput 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.endpointConstant * ∑ i : Fin d, cubeBesovDualFullNorm Q 1 2 1 fun (x : Vec d) => u.grad x i) * cubeLpNorm Q 2 (H1Function.cubePoissonRhs Q u)

Direct L² endpoint control for an H¹ gradient paired against the chosen Neumann Poisson gradient.

theorem HCPolySupport.CubeFullVectorPoincareL2AnalyticInput.abs_gradient_pairing_sum_poissonSolutionFor_le_l2Endpoint {d : ℕ} {Q : TriadicCube d} (h : CubeFullVectorPoincareL2AnalyticInput 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.endpointConstant * ∑ i : Fin d, cubeBesovDualFullNorm Q 1 2 1 fun (x : Vec d) => u.grad x i) * cubeLpNorm Q 2 (H1Function.cubePoissonRhs Q u)

Absolute-value bound for the full gradient pairing sum from the direct L² endpoint.

theorem HCPolySupport.CubeFullVectorPoincareL2AnalyticInput.poissonEnergy_le_cubeVolume_mul_abs_gradient_pairing_sum {d : ℕ} {Q : TriadicCube d} (h : CubeFullVectorPoincareL2AnalyticInput 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 for the direct L² endpoint route.

theorem HCPolySupport.CubeFullVectorPoincareL2AnalyticInput.poissonEnergy_le_full_l2Endpoint {d : ℕ} {Q : TriadicCube d} (h : CubeFullVectorPoincareL2AnalyticInput Q) (u : H1Function (openCubeSet Q)) : ∫ (x : Vec d) in openCubeSet Q, H1Function.cubePoissonRhs Q u x * H1Function.cubePoissonRhs Q u x ≤ cubeVolume Q * ((h.endpointConstant * ∑ 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 direct full-dual L² endpoint constant.

theorem HCPolySupport.CubeFullVectorPoincareL2AnalyticInput.cubeLpNorm_cubePoissonRhs_le_full_l2Endpoint {d : ℕ} {Q : TriadicCube d} (h : CubeFullVectorPoincareL2AnalyticInput 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.endpointConstant * ∑ i : Fin d, cubeBesovDualFullNorm Q 1 2 1 fun (x : Vec d) => u.grad x i

Normalized L² fluctuation estimate obtained directly from the full-dual L² endpoint package.

theorem HCPolySupport.CubeFullVectorPoincareL2AnalyticInput.dualFullVectorPoincareEstimate_of_h1Function {d : ℕ} {Q : TriadicCube d} (h : CubeFullVectorPoincareL2AnalyticInput 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.endpointConstant (fun (x : Vec d) => u.toFun x) fun (x : Vec d) => u.grad x

Infinite-depth full-dual vector Poincare estimate from the direct L² endpoint input bundle.