Coarse-graining support:

Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.LimitHessianPointwise

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

Hlim-free limiting Hessian representatives

The theorems in LimitHessian.lean deliberately take the smooth-test pairing limit as a hypothesis. SmoothPointwise.lean proves that hypothesis from the standard small-step geometry. This file packages the combination in an existence form that downstream interior H² estimates can consume without threading a separate hlim.

theorem HCPolySupport.WeakPoissonEquationOn.exists_openCubeInnerOpenCubeLimitHessianRieszRep_hasWeakPartialDerivOn_grad_of_step_abs {d : ℕ} {V : Set (Vec d)} {Q : TriadicCube d} {uQ : H1Function (openCubeSet Q)} {f : Vec d → ℝ} (h : WeakPoissonEquationOn (openCubeSet Q) uQ f) (hf : MemScalarL2 (openCubeSet Q) f) (hV : IsOpenBoundedConvexDomain V) (stepSeq : ℕ → ℝ) (hstep_ne : ∀ (n : ℕ), stepSeq n ≠ 0) (hstep_tendsto : Filter.Tendsto stepSeq Filter.atTop (nhds 0)) (i j : Fin d) {ρ₁ ρ₂ σ₁ σ₂ ν : ℝ} (η : QuantitativeCubeCutoff Q ρ₁ ρ₂) (hη_sub : tsupport η.toFun ⊆ V) (hinnerV : scaledClosedCubeSet Q ρ₁ ⊆ V) (θ : QuantitativeCubeCutoff Q σ₁ σ₂) (hVν : V ⊆ scaledClosedCubeSet Q ν) (hν_nonneg : 0 ≤ ν) (hνσ : ν ≤ σ₁) (hσ₁_lt_one : σ₁ < 1) (hσ₂_nonneg : 0 ≤ σ₂) (hσ₂_lt_one : σ₂ < 1) (hstep_abs : ∀ (n : ℕ), |stepSeq n| ≤ (σ₁ - ν) * cubeRadius Q) (hρ₁_nonneg : 0 ≤ ρ₁) : ∃ (R : ↥(ScalarL2 (scaledOpenCubeSet Q ρ₁))), ‖R‖ ≤ openCubeInnerQuotientHessianSmoothTestBound uQ f i θ ∧ HasWeakPartialDerivOn (scaledOpenCubeSet Q ρ₁) j (fun (x : Vec d) => uQ.grad x i) fun (x : Vec d) => ↑↑R x

Under the standard local DQ geometry, each Hessian coordinate of uQ exists on the open inner cube as a weak derivative of uQ.grad i; the representative inherits the same explicit quotient-Hessian bound.

theorem HCPolySupport.WeakPoissonEquationOn.exists_hasWeakHessianOn_restrict_of_step_abs {d : ℕ} {V : Set (Vec d)} {Q : TriadicCube d} {uQ : H1Function (openCubeSet Q)} {f : Vec d → ℝ} (h : WeakPoissonEquationOn (openCubeSet Q) uQ f) (hf : MemScalarL2 (openCubeSet Q) f) (hV : IsOpenBoundedConvexDomain V) (stepSeq : ℕ → ℝ) (hstep_ne : ∀ (n : ℕ), stepSeq n ≠ 0) (hstep_tendsto : Filter.Tendsto stepSeq Filter.atTop (nhds 0)) {ρ₁ ρ₂ σ₁ σ₂ ν : ℝ} (η : QuantitativeCubeCutoff Q ρ₁ ρ₂) (hη_sub : tsupport η.toFun ⊆ V) (hinnerV : scaledClosedCubeSet Q ρ₁ ⊆ V) (θ : QuantitativeCubeCutoff Q σ₁ σ₂) (hVν : V ⊆ scaledClosedCubeSet Q ν) (hν_nonneg : 0 ≤ ν) (hνσ : ν ≤ σ₁) (hσ₁_lt_one : σ₁ < 1) (hσ₂_nonneg : 0 ≤ σ₂) (hσ₂_lt_one : σ₂ < 1) (hstep_abs : ∀ (n : ℕ), |stepSeq n| ≤ (σ₁ - ν) * cubeRadius Q) (hρ₁_nonneg : 0 ≤ ρ₁) : ∃ (uS : H1Function (scaledOpenCubeSet Q ρ₁)), uS.toFun = uQ.toFun ∧ uS.grad = uQ.grad ∧ ∃ (H : HasWeakHessianOn (scaledOpenCubeSet Q ρ₁) uS), ∀ (i j : Fin d), ‖H.hessCoordToScalarL2 i j‖ ≤ openCubeInnerQuotientHessianSmoothTestBound uQ f i θ

Bundle the coordinate-wise limiting representatives into a weak Hessian witness for the restriction of uQ to the open inner cube.

theorem HCPolySupport.WeakPoissonEquationOn.exists_hasWeakHessianOn_restrict_hessianCoordL2NormSum_le_of_step_abs {d : ℕ} {V : Set (Vec d)} {Q : TriadicCube d} {uQ : H1Function (openCubeSet Q)} {f : Vec d → ℝ} (h : WeakPoissonEquationOn (openCubeSet Q) uQ f) (hf : MemScalarL2 (openCubeSet Q) f) (hV : IsOpenBoundedConvexDomain V) (stepSeq : ℕ → ℝ) (hstep_ne : ∀ (n : ℕ), stepSeq n ≠ 0) (hstep_tendsto : Filter.Tendsto stepSeq Filter.atTop (nhds 0)) {ρ₁ ρ₂ σ₁ σ₂ ν : ℝ} (η : QuantitativeCubeCutoff Q ρ₁ ρ₂) (hη_sub : tsupport η.toFun ⊆ V) (hinnerV : scaledClosedCubeSet Q ρ₁ ⊆ V) (θ : QuantitativeCubeCutoff Q σ₁ σ₂) (hVν : V ⊆ scaledClosedCubeSet Q ν) (hν_nonneg : 0 ≤ ν) (hνσ : ν ≤ σ₁) (hσ₁_lt_one : σ₁ < 1) (hσ₂_nonneg : 0 ≤ σ₂) (hσ₂_lt_one : σ₂ < 1) (hstep_abs : ∀ (n : ℕ), |stepSeq n| ≤ (σ₁ - ν) * cubeRadius Q) (hρ₁_nonneg : 0 ≤ ρ₁) : ∃ (uS : H1Function (scaledOpenCubeSet Q ρ₁)), uS.toFun = uQ.toFun ∧ uS.grad = uQ.grad ∧ ∃ (H : HasWeakHessianOn (scaledOpenCubeSet Q ρ₁) uS), H.hessianCoordL2NormSum ≤ ∑ i : Fin d, ∑ _j : Fin d, openCubeInnerQuotientHessianSmoothTestBound uQ f i θ

Sum-form version of the bundled weak Hessian estimate.

theorem HCPolySupport.WeakPoissonEquationOn.exists_hasWeakHessianOn_restrict_hessianCoordL2NormSum_le_of_strict_inner_margin {d : ℕ} {V : Set (Vec d)} {Q : TriadicCube d} {uQ : H1Function (openCubeSet Q)} {f : Vec d → ℝ} (h : WeakPoissonEquationOn (openCubeSet Q) uQ f) (hf : MemScalarL2 (openCubeSet Q) f) (hV : IsOpenBoundedConvexDomain V) {ρ₁ ρ₂ σ₁ σ₂ ν : ℝ} (η : QuantitativeCubeCutoff Q ρ₁ ρ₂) (hη_sub : tsupport η.toFun ⊆ V) (hinnerV : scaledClosedCubeSet Q ρ₁ ⊆ V) (θ : QuantitativeCubeCutoff Q σ₁ σ₂) (hVν : V ⊆ scaledClosedCubeSet Q ν) (hν_nonneg : 0 ≤ ν) (hνσ : ν < σ₁) (hσ₁_lt_one : σ₁ < 1) (hσ₂_nonneg : 0 ≤ σ₂) (hσ₂_lt_one : σ₂ < 1) (hρ₁_nonneg : 0 ≤ ρ₁) : ∃ (uS : H1Function (scaledOpenCubeSet Q ρ₁)), uS.toFun = uQ.toFun ∧ uS.grad = uQ.grad ∧ ∃ (H : HasWeakHessianOn (scaledOpenCubeSet Q ρ₁) uS), H.hessianCoordL2NormSum ≤ ∑ i : Fin d, ∑ _j : Fin d, openCubeInnerQuotientHessianSmoothTestBound uQ f i θ

Sum-form weak Hessian estimate with a canonical small-step sequence chosen from the strict geometric margin between the ambient convex set and the cutoff support scale.