Coarse-graining support:

Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.HessianGradientH1

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

Gradient-coordinate H¹ functions from weak Hessians

The Hessian-to-Besov part of C.2 needs to apply one-cube Poincare to each component of the Poisson gradient on descendant cubes. This file packages the basic Sobolev witness: a weak Hessian on u makes every coordinate ∂ᵢu into an H¹ function with weak gradient given by the ith Hessian row.

noncomputable def HCPolySupport.HasWeakHessianOn.gradCoordH1Function {d : ℕ} {U : Set (Vec d)} {u : H1Function U} (H : HasWeakHessianOn U u) (i : Fin d) : H1Function U

The ith weak-gradient coordinate as an H¹ function. Its weak gradient is the ith row of the weak Hessian.

Equations

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

@[simp]

theorem HCPolySupport.HasWeakHessianOn.gradCoordH1Function_apply {d : ℕ} {U : Set (Vec d)} {u : H1Function U} (H : HasWeakHessianOn U u) (i : Fin d) (x : Vec d) : (H.gradCoordH1Function i).toFun x = u.grad x i

@[simp]

theorem HCPolySupport.HasWeakHessianOn.gradCoordH1Function_grad {d : ℕ} {U : Set (Vec d)} {u : H1Function U} (H : HasWeakHessianOn U u) (i : Fin d) (x : Vec d) : (H.gradCoordH1Function i).grad x = fun (j : Fin d) => H.hess i j x

@[simp]

theorem HCPolySupport.HasWeakHessianOn.gradCoordH1Function_grad_apply {d : ℕ} {U : Set (Vec d)} {u : H1Function U} (H : HasWeakHessianOn U u) (i j : Fin d) (x : Vec d) : (H.gradCoordH1Function i).grad x j = H.hess i j x

theorem HCPolySupport.HasWeakHessianOn.gradCoordH1Function_gradientCoordL2NormSum_eq {d : ℕ} {U : Set (Vec d)} {u : H1Function U} (H : HasWeakHessianOn U u) (i : Fin d) : (H.gradCoordH1Function i).gradientCoordL2NormSum = ∑ j : Fin d, ‖H.hessCoordToScalarL2 i j‖

The coordinate-gradient L² sum of ∂ᵢu is exactly the ith Hessian row sum recorded by the Hessian witness.

theorem HCPolySupport.HasWeakHessianOn.restrict_gradCoordH1Function_gradToVectorL2_norm_le {d : ℕ} {U : Set (Vec d)} {u : H1Function U} (H : HasWeakHessianOn U u) {V : Set (Vec d)} (hVopen : IsOpen V) (hVU : V ⊆ U) (i : Fin d) : ‖((H.restrict hVopen hVU).gradCoordH1Function i).gradToVectorL2‖ ≤ ‖(H.gradCoordH1Function i).gradToVectorL2‖

Restricting the domain does not increase the L² norm of a Hessian row, viewed as the weak gradient of the corresponding gradient coordinate.

theorem HCPolySupport.HasWeakHessianOn.gradCoordH1Function_gradToVectorL2_norm_le_rowCoordL2NormSum {d : ℕ} {U : Set (Vec d)} {u : H1Function U} (H : HasWeakHessianOn U u) (i : Fin d) : ‖(H.gradCoordH1Function i).gradToVectorL2‖ ≤ ∑ j : Fin d, ‖H.hessCoordToScalarL2 i j‖

theorem HCPolySupport.HasWeakHessianOn.gradCoordH1Function_gradToVectorL2_norm_le_hessianCoordL2NormSum {d : ℕ} {U : Set (Vec d)} {u : H1Function U} (H : HasWeakHessianOn U u) (i : Fin d) : ‖(H.gradCoordH1Function i).gradToVectorL2‖ ≤ H.hessianCoordL2NormSum

theorem HCPolySupport.HasWeakHessianOn.cubeBesovOscillation_gradCoord_le_volumeFactor_mul_coerciveConst {d : ℕ} {Q : TriadicCube d} {u : H1Function (openCubeSet Q)} (H : HasWeakHessianOn (openCubeSet Q) u) (i : Fin d) (hC : H1CoerciveEstimate (openCubeSet Q)) : (cubeBesovOscillation Q 2 fun (x : Vec d) => u.grad x i) ≤ ((cubeVolume Q)⁻¹ + 1) * hC.constantValue * ‖(H.gradCoordH1Function i).gradToVectorL2‖

One-cube Poincare applied to a gradient coordinate of a weak-Hessian function, stated in normalized cube-oscillation form.

This is the single-cube ingredient for the later descendant summation: cubeBesovOscillation of ∂ᵢu is controlled by the coercive constant on the cube and the L² norm of the Hessian row.

theorem HCPolySupport.HasWeakHessianOn.cubeBesovOscillation_gradCoord_le_volumeInvRpowHalf_mul_coerciveConst {d : ℕ} {Q : TriadicCube d} {u : H1Function (openCubeSet Q)} (H : HasWeakHessianOn (openCubeSet Q) u) (i : Fin d) (hC : H1CoerciveEstimate (openCubeSet Q)) : (cubeBesovOscillation Q 2 fun (x : Vec d) => u.grad x i) ≤ (cubeVolume Q)⁻¹ ^ (1 / 2) * hC.constantValue * ‖(H.gradCoordH1Function i).gradToVectorL2‖

Scale-sharp one-cube Poincare handoff for a gradient coordinate.

This is the same estimate as cubeBesovOscillation_gradCoord_le_volumeFactor_mul_coerciveConst, but with the exact q=2 normalized L² conversion factor volume^{-1/2}. This is the form needed for the C.2 depth summation, where the descendant-count factor cancels this normalization.

theorem HCPolySupport.HasWeakHessianOn.cubeBesovOscillation_gradCoord_descendant_le_volumeFactor_mul_coerciveConst {d : ℕ} {Q : TriadicCube d} {u : H1Function (openCubeSet Q)} {R : TriadicCube d} {j : ℕ} (H : HasWeakHessianOn (openCubeSet Q) u) (hR : R ∈ descendantsAtDepth Q j) (i : Fin d) (hC : H1CoerciveEstimate (openCubeSet R)) : (cubeBesovOscillation R 2 fun (x : Vec d) => u.grad x i) ≤ ((cubeVolume R)⁻¹ + 1) * hC.constantValue * ‖((H.restrict ⋯ ⋯).gradCoordH1Function i).gradToVectorL2‖

Descendant-cube form of cubeBesovOscillation_gradCoord_le_volumeFactor_mul_coerciveConst, obtained by restricting the Hessian witness to the descendant open cube.

theorem HCPolySupport.HasWeakHessianOn.cubeBesovOscillation_gradCoord_descendant_le_volumeInvRpowHalf_mul_coerciveConst {d : ℕ} {Q : TriadicCube d} {u : H1Function (openCubeSet Q)} {R : TriadicCube d} {j : ℕ} (H : HasWeakHessianOn (openCubeSet Q) u) (hR : R ∈ descendantsAtDepth Q j) (i : Fin d) (hC : H1CoerciveEstimate (openCubeSet R)) : (cubeBesovOscillation R 2 fun (x : Vec d) => u.grad x i) ≤ (cubeVolume R)⁻¹ ^ (1 / 2) * hC.constantValue * ‖((H.restrict ⋯ ⋯).gradCoordH1Function i).gradToVectorL2‖

Descendant-cube form of the scale-sharp one-cube Poincare handoff.