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

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

noncomputable def HCPolySupport.CubeDirichletWeakPoissonProblem.originCubeParentReducedOriginalEnergyBound {d : ℕ} {m : ℤ} (u : H10Function (openCubeSet (originCube d m))) (F : Vec d → ℝ) (_i : Fin d) : ℝ

Original-cube energy bound obtained after reading the fixed-radii odd-reflected parent reduced smooth-test constant through the all-face reflection identities.

Equations

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

noncomputable def HCPolySupport.CubeDirichletWeakPoissonProblem.originCubeParentReducedNormEnergyBound {d : ℕ} {m : ℤ} (u : H10Function (openCubeSet (originCube d m))) (F : Vec d → ℝ) (_i : Fin d) : ℝ

The same reflected-parent reduced energy bound, but with the original-cube forcing, gradient, and value integrals rewritten as normalized/L² realizations.

Equations

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

theorem HCPolySupport.CubeDirichletWeakPoissonProblem.originCubeParentReducedOriginalEnergyBound_eq_normEnergyBound {d : ℕ} {m : ℤ} (u : H10Function (openCubeSet (originCube d m))) {F : Vec d → ℝ} (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure (originCube d m))) (i : Fin d) : originCubeParentReducedOriginalEnergyBound u F i = originCubeParentReducedNormEnergyBound u F i

The raw original-cube Dirichlet reflected-parent energy expression is exactly the same as its norm-realized form.

theorem HCPolySupport.CubeDirichletWeakPoissonProblem.reflectedParent_smoothTestEnergy_le_parentEnergy {d : ℕ} {m : ℤ} {u : H10Function (openCubeSet (originCube d m))} {F : Vec d → ℝ} (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure (originCube d m))) {uP : H1Function (openCubeSet (originCube d (m + 1)))} (huP_toFun : uP.toFun = cubeDirichletOddReflectionScalar (originCube d m) u.toFun) (huP_grad : uP.grad = cubeDirichletOddReflectionVectorField (originCube d m) fun (y : Vec d) => u.grad y) (i : Fin d) : WeakPoissonEquationOn.openCubeInnerQuotientHessianSmoothTestReducedBound uP (cubeDirichletOddReflectionScalar (originCube d m) F) i (originCubeParentThreeQuarterSevenEighthCutoff d m) ≤ originCubeParentReducedOriginalEnergyBound u F i

A fixed-radii reduced smooth-test constant on the odd-reflected parent is bounded by the corresponding original-cube energy expression.

theorem HCPolySupport.CubeDirichletWeakPoissonProblem.exists_hasWeakHessianOn_originCube_canonicalRadii_hessianCoordL2NormSum_le_reducedBound {d : ℕ} {m : ℤ} {u : H10Function (openCubeSet (originCube d m))} {F : Vec 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, WeakPoissonEquationOn.openCubeInnerQuotientHessianSmoothTestReducedBound uP (cubeDirichletOddReflectionScalar (originCube d m) F) i (originCubeParentThreeQuarterSevenEighthCutoff d m)

The fixed-radii reflected-parent Hessian estimate with the raw smooth-test constant replaced by the reduced unweighted H¹ bound.

theorem HCPolySupport.CubeDirichletWeakPoissonProblem.exists_reflectedHessian_originalEnergyBound {d : ℕ} {m : ℤ} {u : H10Function (openCubeSet (originCube d m))} {F : Vec 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, originCubeParentReducedOriginalEnergyBound u F i

The fixed-radii reflected-parent Hessian estimate, with the right-hand side expressed entirely in original-cube energy terms.

theorem HCPolySupport.CubeDirichletWeakPoissonProblem.exists_reflectedHessian_energyBound {d : ℕ} {m : ℤ} {u : H10Function (openCubeSet (originCube d m))} {F : Vec 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, originCubeParentReducedNormEnergyBound u F i

The fixed-radii reflected-parent Hessian estimate with the right-hand side expressed through L² norm realizations of the solution and forcing.