Coarse-graining support:

Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.ReflectionParentInterior

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

noncomputable def HCPolySupport.MeanZeroNeumannPoissonSolution.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.

noncomputable def HCPolySupport.MeanZeroNeumannPoissonSolution.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.

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.exists_cubeFaceReflectionParent_h1_weakPoissonEquationOn_originCube {d : ℕ} {m : ℤ} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution (originCube d m) F) (hmean : cubeAverage (originCube d m) F = 0) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure (originCube d m))) : ∃ (uP : H1Function (openCubeSet (originCube d (m + 1)))), uP.toFun = cubeCoordinateFoldReflectedScalar (originCube d m) W.w.toH1Function.toFun ∧ (uP.grad = cubeCoordinateFoldReflectedVectorField (originCube d m) fun (y : Vec d) => W.w.toH1Function.grad y) ∧ WeakPoissonEquationOn (openCubeSet (originCube d (m + 1))) uP (cubeCoordinateFoldReflectedScalar (originCube d m) F)

Stronger reflected parent package retaining the folded-function equality.

The older handoff only retained the gradient equality, since that was enough to establish the weak equation. For the boundary CZ route we also need the function equality, so that the parent-cube interior Hessian can later be read back on the original cube.

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.exists_cubeFaceReflectionParent_hasWeakHessianOn_restrict_hessianCoordL2NormSum_le {d : ℕ} {m : ℤ} {V : Set (Vec d)} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution (originCube d m) F) (hmean : cubeAverage (originCube d m) F = 0) (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 = cubeCoordinateFoldReflectedScalar (originCube d m) W.w.toH1Function.toFun ∧ (uP.grad = cubeCoordinateFoldReflectedVectorField (originCube d m) fun (y : Vec d) => W.w.toH1Function.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 (cubeCoordinateFoldReflectedScalar (originCube d m) F) i θ

Apply the interior weak-Hessian estimate on the centered parent cube after all-face reflection of an origin-cube Neumann solution.

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.exists_cubeFaceReflectionParent_hasWeakHessianOn_originCube_hessianCoordL2NormSum_le {d : ℕ} {m : ℤ} {V : Set (Vec d)} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution (originCube d m) F) (hmean : cubeAverage (originCube d m) F = 0) (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 = cubeCoordinateFoldReflectedScalar (originCube d m) W.w.toH1Function.toFun ∧ (uP.grad = cubeCoordinateFoldReflectedVectorField (originCube d m) fun (y : Vec d) => W.w.toH1Function.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 (cubeCoordinateFoldReflectedScalar (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.MeanZeroNeumannPoissonSolution.exists_foldedParent_weakHessian_canonicalEnergyBound {d : ℕ} {m : ℤ} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution (originCube d m) F) (hmean : cubeAverage (originCube d m) F = 0) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure (originCube d m))) : ∃ (uP : H1Function (openCubeSet (originCube d (m + 1)))), uP.toFun = cubeCoordinateFoldReflectedScalar (originCube d m) W.w.toH1Function.toFun ∧ (uP.grad = cubeCoordinateFoldReflectedVectorField (originCube d m) fun (y : Vec d) => W.w.toH1Function.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 (cubeCoordinateFoldReflectedScalar (originCube d m) F) i (originCubeParentThreeQuarterSevenEighthCutoff d m)

The one-third reflected-parent Hessian estimate with fixed numerical cutoffs. The remaining right-hand side is the smooth-test constant generated by those canonical cutoffs.

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.exists_hasWeakHessianOn_originCube_canonicalRadii_hessianCoordL2NormSum_le {d : ℕ} {m : ℤ} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution (originCube d m) F) (hmean : cubeAverage (originCube d m) F = 0) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure (originCube d m))) : ∃ (uP : H1Function (openCubeSet (originCube d (m + 1)))), uP.toFun = cubeCoordinateFoldReflectedScalar (originCube d m) W.w.toH1Function.toFun ∧ (uP.grad = cubeCoordinateFoldReflectedVectorField (originCube d m) fun (y : Vec d) => W.w.toH1Function.grad y) ∧ ∃ (H : HasWeakHessianOn (openCubeSet (originCube d m)) W.w.toH1Function), H.hessianCoordL2NormSum ≤ ∑ i : Fin d, ∑ _j : Fin d, WeakPoissonEquationOn.openCubeInnerQuotientHessianSmoothTestBound uP (cubeCoordinateFoldReflectedScalar (originCube d m) F) i (originCubeParentThreeQuarterSevenEighthCutoff d m)

Read the reflected-parent fixed-radii Hessian witness as a weak Hessian of the original Neumann solution on the original cube.