Coarse-graining support: Support.Sobolev.Foundations.CubeDirichletH2.ArbitraryCubeEndpoint #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.CubeDirichletWeakPoissonProblem.exists_hasWeakHessianOn_cube_canonicalRadii_hessianCoordL2NormSum_le_smoothTestBound
{d : ℕ}
{Q : TriadicCube d}
{u : H10Function (openCubeSet Q)}
{F : Vec d → ℝ}
(hweak : CubeDirichletWeakPoissonProblem Q u F)
(hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q))
:
∃ (uP : H1Function (openCubeSet (originCube d (Q.scale + 1)))),
uP.toFun = cubeDirichletOddReflectionScalar (originCube d Q.scale) (untranslateToOriginFunction Q u).toFun ∧ (uP.grad = cubeDirichletOddReflectionVectorField (originCube d Q.scale) fun (y : Vec d) =>
(untranslateToOriginFunction Q u).grad y) ∧ ∃ (H : HasWeakHessianOn (openCubeSet Q) u.toH1Function),
H.hessianCoordL2NormSum ≤ ∑ i : Fin d,
∑ _j : Fin d,
WeakPoissonEquationOn.openCubeInnerQuotientHessianSmoothTestBound uP
(cubeDirichletOddReflectionScalar (originCube d Q.scale) fun (x : Vec d) => F (x + triadicCubeShift Q))
i (originCubeParentThreeQuarterSevenEighthCutoff d Q.scale)
Transport the centered-cube reflected-parent Hessian estimate back to an
arbitrary cube of the same scale. The right-hand side is still the canonical
origin-cube smooth-test bound for the translated forcing; a later quantitative
lemma collapses it to a dimension-only multiple of the cube L² norm.
theorem
HCPolySupport.CubeDirichletWeakPoissonProblem.exists_hasWeakHessianOn_cube_canonicalRadii_hessianCoordL2NormSum_le_normEnergyBound
{d : ℕ}
{Q : TriadicCube d}
{u : H10Function (openCubeSet Q)}
{F : Vec d → ℝ}
(hweak : CubeDirichletWeakPoissonProblem Q u F)
(hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q))
:
∃ (uP : H1Function (openCubeSet (originCube d (Q.scale + 1)))),
uP.toFun = cubeDirichletOddReflectionScalar (originCube d Q.scale) (untranslateToOriginFunction Q u).toFun ∧ (uP.grad = cubeDirichletOddReflectionVectorField (originCube d Q.scale) fun (y : Vec d) =>
(untranslateToOriginFunction Q u).grad y) ∧ ∃ (H : HasWeakHessianOn (openCubeSet Q) u.toH1Function),
H.hessianCoordL2NormSum ≤ ∑ i : Fin d,
∑ _j : Fin d,
originCubeParentReducedNormEnergyBound (untranslateToOriginFunction Q u)
(fun (x : Vec d) => F (x + triadicCubeShift Q)) i
Transport the centered-cube norm-energy reflected-parent Hessian estimate back to an arbitrary cube of the same scale.
theorem
HCPolySupport.CubeDirichletWeakPoissonProblem.exists_reflectedHessian_solverEnergyBound
{d : ℕ}
{Q : TriadicCube d}
{u : H10Function (openCubeSet Q)}
{F : Vec d → ℝ}
[NeZero d]
(hweak : CubeDirichletWeakPoissonProblem Q u F)
(hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q))
:
∃ (uP : H1Function (openCubeSet (originCube d (Q.scale + 1)))),
uP.toFun = cubeDirichletOddReflectionScalar (originCube d Q.scale) (untranslateToOriginFunction Q u).toFun ∧ (uP.grad = cubeDirichletOddReflectionVectorField (originCube d Q.scale) fun (y : Vec d) =>
(untranslateToOriginFunction Q u).grad y) ∧ ∃ (H : HasWeakHessianOn (openCubeSet Q) u.toH1Function),
H.hessianCoordL2NormSum ≤ ∑ i : Fin d,
∑ _j : Fin d,
originCubeParentReducedSolverEnergyBoundExact d Q.scale (fun (x : Vec d) => F (x + triadicCubeShift Q)) i
Transport the forcing-facing centered-cube Dirichlet solver-energy Hessian estimate back to an arbitrary cube of the same scale.