Coarse-graining support: Support.Sobolev.Foundations.CubeDirichletH2.SolverEnergy

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

noncomputable def HCPolySupport.CubeDirichletWeakPoissonProblem.originCubeUnitZeroTraceH1CoerciveConstant (d : ℕ) [NeZero d] : ℝ

A chosen zero-trace Poincare constant on the unit centered origin cube.

Equations

• HCPolySupport.CubeDirichletWeakPoissonProblem.originCubeUnitZeroTraceH1CoerciveConstant d = Classical.choose ⋯

theorem HCPolySupport.CubeDirichletWeakPoissonProblem.originCubeUnitZeroTraceH1CoerciveConstant_nonneg (d : ℕ) [NeZero d] : 0 ≤ originCubeUnitZeroTraceH1CoerciveConstant d

theorem HCPolySupport.CubeDirichletWeakPoissonProblem.originCubeUnitZeroTraceH1CoerciveConstant_bound {d : ℕ} [NeZero d] (u : H10Function (openCubeSet (originCube d 0))) : ‖u.toScalarL2‖ ≤ originCubeUnitZeroTraceH1CoerciveConstant d * u.gradientCoordL2NormSum

noncomputable def HCPolySupport.CubeDirichletWeakPoissonProblem.originCubeZeroTraceH1CoerciveConstant (d : ℕ) [NeZero d] (m : ℤ) : ℝ

The scale-sharp zero-trace Poincare constant on centered origin cubes, obtained by dilating the unit centered cube estimate.

Equations

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

theorem HCPolySupport.CubeDirichletWeakPoissonProblem.originCubeZeroTraceH1CoerciveConstant_nonneg (d : ℕ) [NeZero d] (m : ℤ) : 0 ≤ originCubeZeroTraceH1CoerciveConstant d m

theorem HCPolySupport.CubeDirichletWeakPoissonProblem.originCubeZeroTraceH1CoerciveConstant_bound {d : ℕ} {m : ℤ} [NeZero d] (u : H10Function (openCubeSet (originCube d m))) : ‖u.toScalarL2‖ ≤ originCubeZeroTraceH1CoerciveConstant d m * u.gradientCoordL2NormSum

noncomputable def HCPolySupport.CubeDirichletWeakPoissonProblem.originCubeZeroTraceH1HilbertCoerciveConstant (d : ℕ) [NeZero d] (m : ℤ) : ℝ

The zero-trace Poincare constant converted to the Hilbert-vector gradient norm used by the interior estimate.

Equations

• HCPolySupport.CubeDirichletWeakPoissonProblem.originCubeZeroTraceH1HilbertCoerciveConstant d m = HCPolySupport.CubeDirichletWeakPoissonProblem.originCubeZeroTraceH1CoerciveConstant d m * ↑d

theorem HCPolySupport.CubeDirichletWeakPoissonProblem.originCubeZeroTraceH1HilbertCoerciveConstant_nonneg (d : ℕ) [NeZero d] (m : ℤ) : 0 ≤ originCubeZeroTraceH1HilbertCoerciveConstant d m

theorem HCPolySupport.CubeDirichletWeakPoissonProblem.originCubeZeroTraceH1HilbertCoerciveConstant_bound {d : ℕ} {m : ℤ} [NeZero d] (u : H10Function (openCubeSet (originCube d m))) : ‖u.toScalarL2‖ ≤ originCubeZeroTraceH1HilbertCoerciveConstant d m * ‖u.gradToHilbertVectorL2‖

theorem HCPolySupport.CubeDirichletWeakPoissonProblem.norm_gradToHilbertVectorL2_le_solverCubeLpNorm_exact {d : ℕ} {m : ℤ} {u : H10Function (openCubeSet (originCube d m))} {F : Vec d → ℝ} [NeZero d] (hweak : CubeDirichletWeakPoissonProblem (originCube d m) u F) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure (originCube d m))) : ‖u.gradToHilbertVectorL2‖ ≤ originCubeZeroTraceH1HilbertCoerciveConstant d m * (cubeVolume (originCube d m) ^ (1 / 2) * cubeLpNorm (originCube d m) 2 F)

Testing the Dirichlet weak equation with the solution and using zero-trace Poincare controls the gradient by the normalized forcing norm.

theorem HCPolySupport.CubeDirichletWeakPoissonProblem.norm_toScalarL2_le_solverCubeLpNorm_exact {d : ℕ} {m : ℤ} {u : H10Function (openCubeSet (originCube d m))} {F : Vec d → ℝ} [NeZero d] (hweak : CubeDirichletWeakPoissonProblem (originCube d m) u F) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure (originCube d m))) : ‖u.toScalarL2‖ ≤ originCubeZeroTraceH1HilbertCoerciveConstant d m * (originCubeZeroTraceH1HilbertCoerciveConstant d m * (cubeVolume (originCube d m) ^ (1 / 2) * cubeLpNorm (originCube d m) 2 F))

The solution value is controlled by the forcing norm after one additional zero-trace Poincare step.

noncomputable def HCPolySupport.CubeDirichletWeakPoissonProblem.originCubeParentReducedSolverEnergyBoundExact (d : ℕ) [NeZero d] (m : ℤ) (F : Vec d → ℝ) (_i : Fin d) : ℝ

Scale-sharp forcing-facing odd-reflected parent reduced energy expression for Dirichlet solutions, using the chosen zero-trace Poincare constant.

Equations

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

noncomputable def HCPolySupport.CubeDirichletWeakPoissonProblem.originCubeParentReducedSolverEnergyInsideExact (d : ℕ) [NeZero d] (m : ℤ) : ℝ

The forcing-independent factor under the square root in the exact reflected Dirichlet solver bound, using the square root of cube volume.

Equations

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

noncomputable def HCPolySupport.CubeDirichletWeakPoissonProblem.originCubeParentReducedSolverEnergyConstantExact (d : ℕ) [NeZero d] (m : ℤ) : ℝ

The coefficient obtained by factoring the normalized forcing norm out of the exact Dirichlet solver-energy bound.

Equations

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

theorem HCPolySupport.CubeDirichletWeakPoissonProblem.originCubeParentReducedSolverEnergyConstantExact_nonneg (d : ℕ) [NeZero d] (m : ℤ) : 0 ≤ originCubeParentReducedSolverEnergyConstantExact d m

theorem HCPolySupport.CubeDirichletWeakPoissonProblem.parentSolverEnergyConstant_volumeCancel (d : ℕ) [NeZero d] (m : ℤ) : (cubeVolume (originCube d m))⁻¹ ^ (1 / 2) * originCubeParentReducedSolverEnergyConstantExact d m = originCubeParentReducedSolverEnergyConstantExact d 0

theorem HCPolySupport.CubeDirichletWeakPoissonProblem.originCubeParentReducedSolverEnergyBoundExact_eq_constant_mul_cubeLpNorm (d : ℕ) [NeZero d] (m : ℤ) (F : Vec d → ℝ) (i : Fin d) : originCubeParentReducedSolverEnergyBoundExact d m F i = originCubeParentReducedSolverEnergyConstantExact d m * cubeLpNorm (originCube d m) 2 F

theorem HCPolySupport.CubeDirichletWeakPoissonProblem.originCubeParentReducedNormEnergyBound_le_solverEnergyBoundExact {d : ℕ} {m : ℤ} {u : H10Function (openCubeSet (originCube d m))} {F : Vec d → ℝ} [NeZero d] (hweak : CubeDirichletWeakPoissonProblem (originCube d m) u F) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure (originCube d m))) (i : Fin d) : originCubeParentReducedNormEnergyBound u F i ≤ originCubeParentReducedSolverEnergyBoundExact d m F i

The norm-energy bound is controlled by the explicit forcing-facing Dirichlet solver energy expression.

theorem HCPolySupport.CubeDirichletWeakPoissonProblem.exists_reflected_parent_weakHessian_energyBound {d : ℕ} {m : ℤ} {u : H10Function (openCubeSet (originCube d m))} {F : Vec d → ℝ} [NeZero d] (hweak : CubeDirichletWeakPoissonProblem (originCube d m) u F) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure (originCube d m))) : ∃ (uP : H1Function (openCubeSet (originCube d (m + 1)))), uP.toFun = cubeDirichletOddReflectionScalar (originCube d m) u.toFun ∧ (uP.grad = cubeDirichletOddReflectionVectorField (originCube d m) fun (y : Vec d) => u.grad y) ∧ ∃ (H : HasWeakHessianOn (openCubeSet (originCube d m)) u.toH1Function), H.hessianCoordL2NormSum ≤ ∑ i : Fin d, ∑ _j : Fin d, originCubeParentReducedSolverEnergyBoundExact d m F i

The fixed-radii reflected-parent Hessian estimate controlled by the forcing-facing Dirichlet solver energy expression.