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

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

Analytic-input bundles, integral helpers, and H1Function Poisson surface

This file packages the analytic-input bundles used by the cube-local vector Poincare proofs (full, full-L², and projected), the cubeAverage ↔ integralAverage and setIntegral ↔ cubeBesovPairing identities, and the H1Function-side Poisson right-hand side and mean-zero representative.

structure HCPolySupport.CubeFullVectorPoincareAnalyticInput {d : ℕ} (Q : TriadicCube d) : Type

Corrected analytic input bundle for the full-dual vector Poincare theorem. It keeps the same Poisson solver and Neumann CZ field as the legacy bundle, but uses the full endpoint-duality surface that retains constant modes.

• poisson : HasMeanZeroNeumannPoissonSolverOnCube Q
• czConstant : ℝ

  The nonnegative constant bounding the summed positive Besov norms of a Neumann Poisson gradient by the L² norm of the forcing.

• cz : CubeNeumannPoissonGradientBesovEstimate Q self.czConstant
• dualityConstant : ℝ

  The nonnegative constant in full endpoint duality for pairings with a Neumann Poisson gradient.

• duality : CubePoissonGradientFullEndpointDuality Q self.dualityConstant

structure HCPolySupport.CubeFullVectorPoincareL2AnalyticInput {d : ℕ} (Q : TriadicCube d) : Type

Slim corrected analytic input bundle for the full-dual vector Poincare theorem after the Poisson-gradient endpoint estimate has already been combined with the Neumann CZ estimate. This is the interface downstream arguments should aim to use: a solver plus one direct L² endpoint constant.

• poisson : HasMeanZeroNeumannPoissonSolverOnCube Q
• endpointConstant : ℝ

  The nonnegative constant bounding the Poisson-gradient pairing by the full dual norm of the vector field and the L² norm of the forcing.

• endpoint : CubePoissonGradientFullL2EndpointDuality Q self.endpointConstant

theorem HCPolySupport.CubeFullVectorPoincareL2AnalyticInput.endpointConstant_nonneg {d : ℕ} {Q : TriadicCube d} (h : CubeFullVectorPoincareL2AnalyticInput Q) : 0 ≤ h.endpointConstant

theorem HCPolySupport.CubeFullVectorPoincareAnalyticInput.czConstant_nonneg {d : ℕ} {Q : TriadicCube d} (h : CubeFullVectorPoincareAnalyticInput Q) : 0 ≤ h.czConstant

theorem HCPolySupport.CubeFullVectorPoincareAnalyticInput.dualityConstant_nonneg {d : ℕ} {Q : TriadicCube d} (h : CubeFullVectorPoincareAnalyticInput Q) : 0 ≤ h.dualityConstant

noncomputable def HCPolySupport.CubeFullVectorPoincareAnalyticInput.toL2AnalyticInput {d : ℕ} {Q : TriadicCube d} (h : CubeFullVectorPoincareAnalyticInput Q) : CubeFullVectorPoincareL2AnalyticInput Q

Collapse the split corrected full endpoint plus Neumann CZ bundle into the direct L² endpoint bundle.

Equations

• h.toL2AnalyticInput = { poisson := ⋯, endpointConstant := h.dualityConstant * h.czConstant, endpoint := ⋯ }

structure HCPolySupport.CubeProjectedVectorPoincareAnalyticInput {d : ℕ} (Q : TriadicCube d) : Type

A bundled interface for the classical analytic ingredients behind the single-cube projected vector Poincare theorem.

• poisson : HasMeanZeroNeumannPoissonSolverOnCube Q
• czConstant : ℝ

  The nonnegative constant bounding the summed positive Besov norms of a Neumann Poisson gradient by the L² norm of the forcing.

• cz : CubeNeumannPoissonGradientBesovEstimate Q self.czConstant
• dualityConstant : ℝ

  The nonnegative constant in endpoint duality for projected vector-field components.

• duality : CubeProjectedGradientEndpointDuality Q self.dualityConstant
• fullDualityConstant : ℝ

  The nonnegative constant in endpoint duality for unprojected vector-field components.

• fullDuality : CubeGradientEndpointDuality Q self.fullDualityConstant

theorem HCPolySupport.CubeProjectedVectorPoincareAnalyticInput.czConstant_nonneg {d : ℕ} {Q : TriadicCube d} (h : CubeProjectedVectorPoincareAnalyticInput Q) : 0 ≤ h.czConstant

theorem HCPolySupport.CubeProjectedVectorPoincareAnalyticInput.dualityConstant_nonneg {d : ℕ} {Q : TriadicCube d} (h : CubeProjectedVectorPoincareAnalyticInput Q) : 0 ≤ h.dualityConstant

theorem HCPolySupport.CubeProjectedVectorPoincareAnalyticInput.fullDualityConstant_nonneg {d : ℕ} {Q : TriadicCube d} (h : CubeProjectedVectorPoincareAnalyticInput Q) : 0 ≤ h.fullDualityConstant

theorem HCPolySupport.cubeAverage_eq_integralAverage_openCubeSet {d : ℕ} (Q : TriadicCube d) (f : Vec d → ℝ) : cubeAverage Q f = integralAverage (openCubeSet Q) f

theorem HCPolySupport.setIntegral_openCubeSet_eq_cubeVolume_mul_cubeAverage {d : ℕ} (Q : TriadicCube d) (f : Vec d → ℝ) : ∫ (x : Vec d) in openCubeSet Q, f x = cubeVolume Q * cubeAverage Q f

theorem HCPolySupport.setIntegral_openCubeSet_mul_eq_cubeVolume_mul_cubeBesovPairing {d : ℕ} (Q : TriadicCube d) (f g : Vec d → ℝ) : ∫ (x : Vec d) in openCubeSet Q, f x * g x = cubeVolume Q * cubeBesovPairing Q f g

theorem HCPolySupport.setIntegral_openCubeSet_sq_eq_cubeVolume_mul_cubeLpNorm_two_rpow {d : ℕ} (Q : TriadicCube d) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f 2 (normalizedCubeMeasure Q)) : ∫ (x : Vec d) in openCubeSet Q, f x * f x = cubeVolume Q * cubeLpNorm Q 2 f ^ 2

The unnormalized square integral on the open cube is the cube volume times the square of the normalized L² norm.

noncomputable def HCPolySupport.H1Function.cubePoissonRhs {d : ℕ} (Q : TriadicCube d) (u : H1Function (openCubeSet Q)) : Vec d → ℝ

The mean-zero right-hand side for the cube Neumann Poisson problem associated to an H¹ function.

Equations

• HCPolySupport.H1Function.cubePoissonRhs Q u = HCPolySupport.cubeFluctuation Q fun (x : HCPolySupport.Vec d) => u.toFun x

@[simp]

theorem HCPolySupport.H1Function.cubePoissonRhs_apply {d : ℕ} {Q : TriadicCube d} (u : H1Function (openCubeSet Q)) (x : Vec d) : cubePoissonRhs Q u x = u.toFun x - cubeAverage Q fun (x : Vec d) => u.toFun x

theorem HCPolySupport.H1Function.cubePoissonRhs_memL2_normalizedCubeMeasure {d : ℕ} {Q : TriadicCube d} (u : H1Function (openCubeSet Q)) : MeasureTheory.MemLp (cubePoissonRhs Q u) 2 (normalizedCubeMeasure Q)

theorem HCPolySupport.H1Function.cubeAverage_cubePoissonRhs {d : ℕ} {Q : TriadicCube d} (u : H1Function (openCubeSet Q)) : cubeAverage Q (cubePoissonRhs Q u) = 0

@[simp]

theorem HCPolySupport.H1Function.cubeBesovOscillation_eq_cubeLpNorm_cubePoissonRhs {d : ℕ} {Q : TriadicCube d} (u : H1Function (openCubeSet Q)) : (cubeBesovOscillation Q 2 fun (x : Vec d) => u.toFun x) = cubeLpNorm Q 2 (cubePoissonRhs Q u)

noncomputable def HCPolySupport.H1Function.toMeanZeroOnCube {d : ℕ} (Q : TriadicCube d) (u : H1Function (openCubeSet Q)) : H1MeanZeroFunction (openCubeSet Q)

The open-cube mean-zero representative of an H¹ function, with the normalization chosen to match cubePoissonRhs.

Equations

• HCPolySupport.H1Function.toMeanZeroOnCube Q u = u.toMeanZero

@[simp]

theorem HCPolySupport.H1Function.toMeanZeroOnCube_apply {d : ℕ} {Q : TriadicCube d} (u : H1Function (openCubeSet Q)) (x : Vec d) : (toMeanZeroOnCube Q u).toH1Function.toFun x = cubePoissonRhs Q u x

@[simp]

theorem HCPolySupport.H1Function.toMeanZeroOnCube_grad {d : ℕ} {Q : TriadicCube d} (u : H1Function (openCubeSet Q)) (x : Vec d) : (toMeanZeroOnCube Q u).toH1Function.grad x = u.grad x

theorem HCPolySupport.H1Function.grad_coord_memL2_normalizedCubeMeasure {d : ℕ} {Q : TriadicCube d} (u : H1Function (openCubeSet Q)) (i : Fin d) : MeasureTheory.MemLp (fun (x : Vec d) => u.grad x i) 2 (normalizedCubeMeasure Q)

theorem HCPolySupport.H1Function.grad_coord_memL2_normalizedCubeMeasure_descendant {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (u : H1Function (openCubeSet Q)) (hR : R ∈ descendantsAtDepth Q j) (i : Fin d) : MeasureTheory.MemLp (fun (x : Vec d) => u.grad x i) 2 (normalizedCubeMeasure R)