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

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

Cube-local Poisson solver and normalized-norm bridges

This file records the Poisson-solver structure used by the cube-local Poincare arguments, together with the bridges between MemL2On (openCubeSet Q) and the normalized-cube MemLp measure that make the variational layer applicable.

theorem HCPolySupport.nonneg_le_of_sq_le_mul_self {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) (h : x ^ 2 ≤ y * x) : x ≤ y

structure HCPolySupport.MeanZeroNeumannPoissonSolution {d : ℕ} (Q : TriadicCube d) (F : Vec d → ℝ) : Type

A mean-zero Neumann solution of -Δw = F on a cube, in weak form. The test space is mean-zero H¹, which fixes the additive constant.

• w : H1MeanZeroFunction (openCubeSet Q)

  The mean-zero H¹ solution of the weak Neumann Poisson equation on the open cube.

• equation (φ : H1MeanZeroFunction (openCubeSet Q)) : ∫ (x : Vec d) in openCubeSet Q, vecDot (self.w.toH1Function.grad x) (φ.toH1Function.grad x) = ∫ (x : Vec d) in openCubeSet Q, F x * φ.toH1Function.toFun x

@[simp]

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.equation_self {d : ℕ} {Q : TriadicCube d} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution Q F) : ∫ (x : Vec d) in openCubeSet Q, vecDot (W.w.toH1Function.grad x) (W.w.toH1Function.grad x) = ∫ (x : Vec d) in openCubeSet Q, F x * W.w.toH1Function.toFun x

def HCPolySupport.HasMeanZeroNeumannPoissonSolverOnCube {d : ℕ} (Q : TriadicCube d) : Prop

Existence of the mean-zero Neumann Poisson solver on a cube for normalized L² right-hand sides with zero normalized average.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.memL2On_openCubeSet_of_memLp_normalizedCubeMeasure {d : ℕ} (Q : TriadicCube d) {F : Vec d → ℝ} (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) : MemL2On (openCubeSet Q) F

theorem HCPolySupport.cubeLpNorm_two_le_volume_inv_add_one_mul_norm_toScalarL2_openCubeSet {d : ℕ} (Q : TriadicCube d) {f : Vec d → ℝ} (hf : MeasureTheory.MemLp f 2 (normalizedCubeMeasure Q)) : cubeLpNorm Q 2 f ≤ ((cubeVolume Q)⁻¹ + 1) * ‖toScalarL2 ⋯‖

theorem HCPolySupport.cubeLpNorm_two_eq_volume_inv_rpow_half_mul_norm_toScalarL2_openCubeSet {d : ℕ} (Q : TriadicCube d) {f : Vec d → ℝ} (hf : MeasureTheory.MemLp f 2 (normalizedCubeMeasure Q)) : cubeLpNorm Q 2 f = (cubeVolume Q)⁻¹ ^ (1 / 2) * ‖toScalarL2 ⋯‖

Exact normalized-to-unnormalized L² conversion on an open cube.

The older inequality above uses the harmless but scale-wasteful factor (cubeVolume Q)⁻¹ + 1. For the q=2 Calderon-Zygmund path we need the exact probability-measure normalization factor.

theorem HCPolySupport.norm_toScalarL2_openCubeSet_le_volume_add_one_mul_cubeLpNorm_two {d : ℕ} (Q : TriadicCube d) {f : Vec d → ℝ} (hf : MeasureTheory.MemLp f 2 (normalizedCubeMeasure Q)) : ‖toScalarL2 ⋯‖ ≤ (cubeVolume Q + 1) * cubeLpNorm Q 2 f

theorem HCPolySupport.norm_toScalarL2_openCubeSet_eq_volume_rpow_half_mul_cubeLpNorm_two {d : ℕ} (Q : TriadicCube d) {f : Vec d → ℝ} (hf : MeasureTheory.MemLp f 2 (normalizedCubeMeasure Q)) : ‖toScalarL2 ⋯‖ = cubeVolume Q ^ (1 / 2) * cubeLpNorm Q 2 f

noncomputable def HCPolySupport.meanZeroNeumannPoissonSolutionOfCoerciveEstimate {d : ℕ} (Q : TriadicCube d) (F : Vec d → ℝ) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) : MeanZeroNeumannPoissonSolution Q F

The mean-zero weak Neumann Poisson solution constructed using the open cube's H¹ coercive estimate for an L² forcing.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.cubeMeanZeroNeumannPoissonSolverOnCube {d : ℕ} (Q : TriadicCube d) : HasMeanZeroNeumannPoissonSolverOnCube Q

Mean-zero Neumann Poisson existence on cubes, constructed from the coercive Hilbert variational layer and the bounded-open-convex Poincare estimate for cubes.

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

The mean-zero H¹ coercivity constant of the scaled and translated cube estimate.

Equations

• HCPolySupport.cubeMeanZeroH1CoerciveConstant Q = (HCPolySupport.scaledTranslatedCubeMeanZeroH1CoerciveEstimate Q).constantValue

theorem HCPolySupport.cubeMeanZeroH1CoerciveConstant_nonneg {d : ℕ} (Q : TriadicCube d) : 0 ≤ cubeMeanZeroH1CoerciveConstant Q

theorem HCPolySupport.cubeMeanZeroH1CoerciveConstant_eq_scale_mul_unit {d : ℕ} (Q : TriadicCube d) : cubeMeanZeroH1CoerciveConstant Q = cubeScaleFactor Q * (originCubeMeanZeroH1CoerciveEstimate d 0).constantValue

theorem HCPolySupport.meanZeroNeumannPoissonSolution_norm_gradToHilbertVectorL2_le {d : ℕ} (Q : TriadicCube d) {F : Vec d → ℝ} (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) (W : MeanZeroNeumannPoissonSolution Q F) : ‖W.w.gradToHilbertVectorL2‖ ≤ cubeMeanZeroH1CoerciveConstant Q * ‖toScalarL2 ⋯‖

theorem HCPolySupport.meanZeroNeumannPoissonSolution_sum_cubeLpNorm_grad_le {d : ℕ} (Q : TriadicCube d) {F : Vec d → ℝ} (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) (W : MeanZeroNeumannPoissonSolution Q F) : (∑ i : Fin d, cubeLpNorm Q 2 fun (x : Vec d) => W.w.toH1Function.grad x i) ≤ ((cubeVolume Q)⁻¹ + 1) * ↑d * cubeMeanZeroH1CoerciveConstant Q * (cubeVolume Q + 1) * cubeLpNorm Q 2 F

theorem HCPolySupport.meanZeroNeumannPoissonSolution_sum_cubeLpNorm_grad_le_exact {d : ℕ} (Q : TriadicCube d) {F : Vec d → ℝ} (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) (W : MeanZeroNeumannPoissonSolution Q F) : (∑ i : Fin d, cubeLpNorm Q 2 fun (x : Vec d) => W.w.toH1Function.grad x i) ≤ (cubeVolume Q)⁻¹ ^ (1 / 2) * ↑d * cubeMeanZeroH1CoerciveConstant Q * cubeVolume Q ^ (1 / 2) * cubeLpNorm Q 2 F