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

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

def HCPolySupport.CubeDirichletWeakPoissonProblem.OriginCubeDirichletCalderonZygmundRegularityQTwo (d : ℕ) (C : ℝ) : Prop

A stronger regularity-producing centered-cube q = 2 Dirichlet result.

Unlike the manuscript statement, this compatibility predicate concludes the existence of a weak Hessian. The source-facing predicate below instead takes a supplied weak-Hessian witness and estimates that witness.

Equations

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

theorem HCPolySupport.CubeDirichletWeakPoissonProblem.OriginCubeDirichletCalderonZygmundRegularityQTwo.constant_nonneg {d : ℕ} {C : ℝ} (h : OriginCubeDirichletCalderonZygmundRegularityQTwo d C) : 0 ≤ C

theorem HCPolySupport.CubeDirichletWeakPoissonProblem.OriginCubeDirichletCalderonZygmundRegularityQTwo.apply {d : ℕ} {C : ℝ} (h : OriginCubeDirichletCalderonZygmundRegularityQTwo d C) (m : ℤ) (u : H10Function (openCubeSet (originCube d m))) (F : Vec d → ℝ) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure (originCube d m))) (hweak : CubeDirichletWeakPoissonProblem (originCube d m) u F) : ∃ (H : HasWeakHessianOn (openCubeSet (originCube d m)) u.toH1Function), HasWeakHessianOn.frobeniusNormalizedL2 (originCube d m) H ≤ C * (cubeBoundedMeasurableDomain (originCube d m)).normalizedLpNorm 2 F ⋯

theorem HCPolySupport.CubeDirichletWeakPoissonProblem.exists_originCube_dirichlet_calderon_zygmund_regularity_q_two {d : ℕ} [NeZero d] (m : ℤ) (u : H10Function (openCubeSet (originCube d m))) (F : Vec d → ℝ) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure (originCube d m))) (hweak : CubeDirichletWeakPoissonProblem (originCube d m) u F) : ∃ (H : HasWeakHessianOn (openCubeSet (originCube d m)) u.toH1Function), HasWeakHessianOn.frobeniusNormalizedL2 (originCube d m) H ≤ cubeDirichletH2VolumeL2Constant d * (cubeBoundedMeasurableDomain (originCube d m)).normalizedLpNorm 2 F ⋯

The regularity-producing centered-cube Dirichlet q = 2 endpoint.

theorem HCPolySupport.CubeDirichletWeakPoissonProblem.originCubeDirichletCalderonZygmundRegularityQTwo_exact (d : ℕ) [NeZero d] : OriginCubeDirichletCalderonZygmundRegularityQTwo d (cubeDirichletH2VolumeL2Constant d)

The explicit dimension-only constant inhabits the stronger regularity-producing centered-cube Dirichlet q = 2 predicate.

def HCPolySupport.CubeDirichletWeakPoissonProblem.OriginCubeDirichletCalderonZygmundQTwo (d : ℕ) (C : ℝ) : Prop

The literal centered-cube q = 2 Dirichlet Calderón--Zygmund branch in the source: a weak Hessian is supplied as part of the W^{2,2} hypothesis, and the conclusion estimates that supplied Hessian.

Equations

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

theorem HCPolySupport.CubeDirichletWeakPoissonProblem.OriginCubeDirichletCalderonZygmundQTwo.constant_nonneg {d : ℕ} {C : ℝ} (h : OriginCubeDirichletCalderonZygmundQTwo d C) : 0 ≤ C

theorem HCPolySupport.CubeDirichletWeakPoissonProblem.OriginCubeDirichletCalderonZygmundQTwo.apply {d : ℕ} {C : ℝ} (h : OriginCubeDirichletCalderonZygmundQTwo d C) (m : ℤ) (u : H10Function (openCubeSet (originCube d m))) (F : Vec d → ℝ) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure (originCube d m))) (hweak : CubeDirichletWeakPoissonProblem (originCube d m) u F) (H : HasWeakHessianOn (openCubeSet (originCube d m)) u.toH1Function) : HasWeakHessianOn.frobeniusNormalizedL2 (originCube d m) H ≤ C * (cubeBoundedMeasurableDomain (originCube d m)).normalizedLpNorm 2 F ⋯

Apply the literal Dirichlet branch to a supplied weak-Hessian witness.

theorem HCPolySupport.CubeDirichletWeakPoissonProblem.originCubeDirichletCalderonZygmundQTwo_exact (d : ℕ) [NeZero d] : OriginCubeDirichletCalderonZygmundQTwo d (cubeDirichletH2VolumeL2Constant d)

The explicit dimension-only constant proves the literal source-facing Dirichlet branch. Its implementation first produces one weak Hessian and then uses weak-derivative uniqueness to transfer the bound to every supplied witness.