Coarse-graining support: Support.Sobolev.Foundations.CubeDirichletH2.OriginCubeEndpoint #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
noncomputable def
HCPolySupport.CubeDirichletWeakPoissonProblem.originCubeParentOneThirdHalfCutoff
(d : ℕ)
(m : ℤ)
:
QuantitativeCubeCutoff (originCube d (m + 1)) (1 / 3) (1 / 2)
Canonical cutoff from the original cube, viewed as the one-third inner cube of its centered parent, to a half-radius parent cube.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
HCPolySupport.CubeDirichletWeakPoissonProblem.originCubeParentThreeQuarterSevenEighthCutoff
(d : ℕ)
(m : ℤ)
:
QuantitativeCubeCutoff (originCube d (m + 1)) (3 / 4) (7 / 8)
Canonical outer cutoff used by the parent-cube interior estimate.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
HCPolySupport.CubeDirichletWeakPoissonProblem.exists_cubeDirichletOddReflectionParent_hasWeakHessianOn_restrict_hessianCoordL2NormSum_le
{d : ℕ}
{m : ℤ}
{V : Set (Vec d)}
{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)))
(hV : IsOpenBoundedConvexDomain V)
{ρ₁ ρ₂ σ₁ σ₂ ν : ℝ}
(η : QuantitativeCubeCutoff (originCube d (m + 1)) ρ₁ ρ₂)
(hη_sub : tsupport η.toFun ⊆ V)
(hinnerV : scaledClosedCubeSet (originCube d (m + 1)) ρ₁ ⊆ V)
(θ : QuantitativeCubeCutoff (originCube d (m + 1)) σ₁ σ₂)
(hVν : V ⊆ scaledClosedCubeSet (originCube d (m + 1)) ν)
(hν_nonneg : 0 ≤ ν)
(hνσ : ν < σ₁)
(hσ₁_lt_one : σ₁ < 1)
(hσ₂_nonneg : 0 ≤ σ₂)
(hσ₂_lt_one : σ₂ < 1)
(hρ₁_nonneg : 0 ≤ ρ₁)
:
∃ (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) ∧ ∃ (uS : H1Function (scaledOpenCubeSet (originCube d (m + 1)) ρ₁)),
uS.toFun = uP.toFun ∧ uS.grad = uP.grad ∧ ∃ (H : HasWeakHessianOn (scaledOpenCubeSet (originCube d (m + 1)) ρ₁) uS),
H.hessianCoordL2NormSum ≤ ∑ i : Fin d,
∑ _j : Fin d,
WeakPoissonEquationOn.openCubeInnerQuotientHessianSmoothTestBound uP
(cubeDirichletOddReflectionScalar (originCube d m) F) i θ
Apply the interior weak-Hessian estimate on the centered parent cube after all-face odd reflection of an origin-cube Dirichlet solution.
theorem
HCPolySupport.CubeDirichletWeakPoissonProblem.exists_reflectionHessian_le_smoothTestBound
{d : ℕ}
{m : ℤ}
{V : Set (Vec d)}
{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)))
(hV : IsOpenBoundedConvexDomain V)
{ρ₂ σ₁ σ₂ ν : ℝ}
(η : QuantitativeCubeCutoff (originCube d (m + 1)) (1 / 3) ρ₂)
(hη_sub : tsupport η.toFun ⊆ V)
(hinnerV : scaledClosedCubeSet (originCube d (m + 1)) (1 / 3) ⊆ V)
(θ : QuantitativeCubeCutoff (originCube d (m + 1)) σ₁ σ₂)
(hVν : V ⊆ scaledClosedCubeSet (originCube d (m + 1)) ν)
(hν_nonneg : 0 ≤ ν)
(hνσ : ν < σ₁)
(hσ₁_lt_one : σ₁ < 1)
(hσ₂_nonneg : 0 ≤ σ₂)
(hσ₂_lt_one : σ₂ < 1)
:
∃ (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) ∧ ∃ (uS : H1Function (openCubeSet (originCube d m))),
uS.toFun = uP.toFun ∧ uS.grad = uP.grad ∧ ∃ (H : HasWeakHessianOn (openCubeSet (originCube d m)) uS),
H.hessianCoordL2NormSum ≤ ∑ i : Fin d,
∑ _j : Fin d,
WeakPoissonEquationOn.openCubeInnerQuotientHessianSmoothTestBound uP
(cubeDirichletOddReflectionScalar (originCube d m) F) i θ
The parent reflected Hessian estimate specialized to the one-third inner cube, read back as an estimate on the original centered cube.
theorem
HCPolySupport.CubeDirichletWeakPoissonProblem.exists_oddReflectionParent_hasWeakHessianOn_cube_hessianCoordinateL2NormSum_le
{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) ∧ ∃ (uS : H1Function (openCubeSet (originCube d m))),
uS.toFun = uP.toFun ∧ uS.grad = uP.grad ∧ ∃ (H : HasWeakHessianOn (openCubeSet (originCube d m)) uS),
H.hessianCoordL2NormSum ≤ ∑ i : Fin d,
∑ _j : Fin d,
WeakPoissonEquationOn.openCubeInnerQuotientHessianSmoothTestBound uP
(cubeDirichletOddReflectionScalar (originCube d m) F) i
(originCubeParentThreeQuarterSevenEighthCutoff d m)
The one-third reflected-parent Hessian estimate with fixed numerical cutoffs.
theorem
HCPolySupport.CubeDirichletWeakPoissonProblem.exists_hasWeakHessianOn_originCube_canonicalRadii_hessianCoordL2NormSum_le
{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.openCubeInnerQuotientHessianSmoothTestBound uP
(cubeDirichletOddReflectionScalar (originCube d m) F) i
(originCubeParentThreeQuarterSevenEighthCutoff d m)
Read the reflected-parent fixed-radii Hessian witness as a weak Hessian of the original Dirichlet solution on the original cube.