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

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

noncomputable def HCPolySupport.CubeProjectedVectorPoincareAnalyticInput.poissonSolutionFor {d : ℕ} {Q : TriadicCube d} (h : CubeProjectedVectorPoincareAnalyticInput 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 analytic input.

Equations

• h.poissonSolutionFor u = Classical.choose ⋯

theorem HCPolySupport.CubeProjectedVectorPoincareAnalyticInput.poissonSolutionFor_equation {d : ℕ} {Q : TriadicCube d} (h : CubeProjectedVectorPoincareAnalyticInput 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.CubeProjectedVectorPoincareAnalyticInput.poissonSolutionFor_equation_toMeanZeroOnCube {d : ℕ} {Q : TriadicCube d} (h : CubeProjectedVectorPoincareAnalyticInput 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. This is the integration-by-parts entry point for the single-cube Poincare proof.

theorem HCPolySupport.CubeProjectedVectorPoincareAnalyticInput.integral_poissonGradient_vecDot_grad_eq_sum_coord {d : ℕ} {Q : TriadicCube d} (h : CubeProjectedVectorPoincareAnalyticInput 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.CubeProjectedVectorPoincareAnalyticInput.poissonSolutionFor_equation_toMeanZeroOnCube_sum_coord {d : ℕ} {Q : TriadicCube d} (h : CubeProjectedVectorPoincareAnalyticInput 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.CubeProjectedVectorPoincareAnalyticInput.poissonSolutionFor_equation_toMeanZeroOnCube_sum_pairing {d : ℕ} {Q : TriadicCube d} (h : CubeProjectedVectorPoincareAnalyticInput 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. The remaining analytic step is to replace the unprojected u-gradient pairings by their projected limits.

theorem HCPolySupport.CubeProjectedVectorPoincareAnalyticInput.tendsto_projectedGradient_pairing_sum_poissonSolutionFor {d : ℕ} {Q : TriadicCube d} (h : CubeProjectedVectorPoincareAnalyticInput Q) (u : H1Function (openCubeSet Q)) : Filter.Tendsto (fun (n : ℕ) => ∑ i : Fin d, cubeBesovPairing Q (cubeProjection Q (n + 1) fun (x : Vec d) => u.grad x i) fun (x : Vec d) => (h.poissonSolutionFor u).w.toH1Function.grad x i) Filter.atTop (nhds (∑ 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 finite-depth projected gradient pairings converge to the unprojected pairing sum appearing in the tested Poisson identity.

theorem HCPolySupport.CubeProjectedVectorPoincareAnalyticInput.poissonSolutionFor_cz {d : ℕ} {Q : TriadicCube d} (h : CubeProjectedVectorPoincareAnalyticInput 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.CubeProjectedVectorPoincareAnalyticInput.projectedGradient_duality_poissonSolutionFor {d : ℕ} {Q : TriadicCube d} (h : CubeProjectedVectorPoincareAnalyticInput Q) (u : H1Function (openCubeSet Q)) (N : ℕ) : ∑ i : Fin d, |cubeBesovPairing Q (cubeProjection Q N 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, cubeBesovDualMeanZeroSeminorm Q 1 2 1 (cubeProjection Q N 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 projected Besov duality between an H¹ gradient and the gradient of the chosen Neumann Poisson solution.

theorem HCPolySupport.CubeProjectedVectorPoincareAnalyticInput.gradient_duality_poissonSolutionFor {d : ℕ} {Q : TriadicCube d} (h : CubeProjectedVectorPoincareAnalyticInput 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.fullDualityConstant * ∑ i : Fin d, cubeBesovDualMeanZeroSeminorm 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 seminorm.

theorem HCPolySupport.CubeProjectedVectorPoincareAnalyticInput.abs_projectedGradient_pairing_sum_poissonSolutionFor_le {d : ℕ} {Q : TriadicCube d} (h : CubeProjectedVectorPoincareAnalyticInput Q) (u : H1Function (openCubeSet Q)) (N : ℕ) : |∑ i : Fin d, cubeBesovPairing Q (cubeProjection Q N 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, cubeBesovDualMeanZeroSeminorm Q 1 2 1 (cubeProjection Q N 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

Fixed-depth endpoint-duality bound for the projected gradient pairing sum against the chosen Poisson solution.

theorem HCPolySupport.CubeProjectedVectorPoincareAnalyticInput.abs_gradient_pairing_sum_poissonSolutionFor_le {d : ℕ} {Q : TriadicCube d} (h : CubeProjectedVectorPoincareAnalyticInput 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.fullDualityConstant * ∑ i : Fin d, cubeBesovDualMeanZeroSeminorm 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.CubeProjectedVectorPoincareAnalyticInput.abs_projectedGradient_pairing_sum_poissonSolutionFor_le_cz {d : ℕ} {Q : TriadicCube d} (h : CubeProjectedVectorPoincareAnalyticInput Q) (u : H1Function (openCubeSet Q)) (N : ℕ) (hdualNonneg : 0 ≤ ∑ i : Fin d, cubeBesovDualMeanZeroSeminorm Q 1 2 1 (cubeProjection Q N fun (x : Vec d) => u.grad x i)) : |∑ i : Fin d, cubeBesovPairing Q (cubeProjection Q N 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, cubeBesovDualMeanZeroSeminorm Q 1 2 1 (cubeProjection Q N fun (x : Vec d) => u.grad x i)) * (h.czConstant * cubeLpNorm Q 2 (H1Function.cubePoissonRhs Q u))

Fixed-depth projected Poisson pairing bound after inserting the Calderon-Zygmund estimate for the chosen Poisson solution. The nonnegativity hypothesis is the only algebraic side condition needed to multiply the CZ inequality into the endpoint-duality bound.

theorem HCPolySupport.CubeProjectedVectorPoincareAnalyticInput.abs_gradient_pairing_sum_poissonSolutionFor_le_cz {d : ℕ} {Q : TriadicCube d} (h : CubeProjectedVectorPoincareAnalyticInput Q) (u : H1Function (openCubeSet Q)) (hdualNonneg : 0 ≤ ∑ i : Fin d, cubeBesovDualMeanZeroSeminorm 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.fullDualityConstant * ∑ i : Fin d, cubeBesovDualMeanZeroSeminorm 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.CubeProjectedVectorPoincareAnalyticInput.abs_projectedGradient_pairing_sum_poissonSolutionFor_le_cz_grouped {d : ℕ} {Q : TriadicCube d} (h : CubeProjectedVectorPoincareAnalyticInput Q) (u : H1Function (openCubeSet Q)) (N : ℕ) (hdualNonneg : 0 ≤ ∑ i : Fin d, cubeBesovDualMeanZeroSeminorm Q 1 2 1 (cubeProjection Q N fun (x : Vec d) => u.grad x i)) : |∑ i : Fin d, cubeBesovPairing Q (cubeProjection Q N 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, cubeBesovDualMeanZeroSeminorm Q 1 2 1 (cubeProjection Q N fun (x : Vec d) => u.grad x i)) * cubeLpNorm Q 2 (H1Function.cubePoissonRhs Q u)

Constant-grouped version of abs_projectedGradient_pairing_sum_poissonSolutionFor_le_cz.

theorem HCPolySupport.CubeProjectedVectorPoincareAnalyticInput.abs_gradient_pairing_sum_poissonSolutionFor_le_cz_grouped {d : ℕ} {Q : TriadicCube d} (h : CubeProjectedVectorPoincareAnalyticInput Q) (u : H1Function (openCubeSet Q)) (hdualNonneg : 0 ≤ ∑ i : Fin d, cubeBesovDualMeanZeroSeminorm 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.fullDualityConstant * h.czConstant * ∑ i : Fin d, cubeBesovDualMeanZeroSeminorm 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.CubeProjectedVectorPoincareAnalyticInput.poissonEnergy_le_cubeVolume_mul_abs_gradient_pairing_sum {d : ℕ} {Q : TriadicCube d} (h : CubeProjectedVectorPoincareAnalyticInput 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.CubeProjectedVectorPoincareAnalyticInput.poissonEnergy_le_full_duality_cz {d : ℕ} {Q : TriadicCube d} (h : CubeProjectedVectorPoincareAnalyticInput Q) (u : H1Function (openCubeSet Q)) (hdualNonneg : 0 ≤ ∑ i : Fin d, cubeBesovDualMeanZeroSeminorm 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.fullDualityConstant * h.czConstant * ∑ i : Fin d, cubeBesovDualMeanZeroSeminorm 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.CubeProjectedVectorPoincareAnalyticInput.cubeLpNorm_cubePoissonRhs_le_full_duality_cz {d : ℕ} {Q : TriadicCube d} (h : CubeProjectedVectorPoincareAnalyticInput Q) (u : H1Function (openCubeSet Q)) (hdualNonneg : 0 ≤ ∑ i : Fin d, cubeBesovDualMeanZeroSeminorm Q 1 2 1 fun (x : Vec d) => u.grad x i) : cubeLpNorm Q 2 (H1Function.cubePoissonRhs Q u) ≤ h.fullDualityConstant * h.czConstant * ∑ i : Fin d, cubeBesovDualMeanZeroSeminorm 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 infinite-depth vector Poincare theorem.

theorem HCPolySupport.CubeProjectedVectorPoincareAnalyticInput.dualMeanZeroVectorPoincareEstimate_of_h1Function {d : ℕ} {Q : TriadicCube d} (h : CubeProjectedVectorPoincareAnalyticInput Q) (u : H1Function (openCubeSet Q)) (hdualNonneg : 0 ≤ ∑ i : Fin d, cubeBesovDualMeanZeroSeminorm Q 1 2 1 fun (x : Vec d) => u.grad x i) : CubeDualMeanZeroVectorPoincareEstimate Q (h.fullDualityConstant * 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 analytic input bundle.