Coarse-graining support: Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInterior

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

Weak interior interface for the cube Neumann CZ discharge

This file starts the difference-quotient route for the cube Neumann W2,2 / Calderon-Zygmund estimate. The reusable interior theorem consumes a weak Poisson equation for an H1Function; the first bridge below packages the already-proved reflected-block weak equation in exactly that form.

def HCPolySupport.WeakPoissonEquationOn {d : ℕ} (U : Set (Vec d)) (u : H1Function U) (f : Vec d → ℝ) : Prop

Weak equation -Delta u = f on an open set, tested against smooth compactly supported functions whose topological support lies in the set.

Equations

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

structure HCPolySupport.HasWeakHessianOn {d : ℕ} (U : Set (Vec d)) (u : H1Function U) : Type

A weak L² Hessian witness for an H¹ function on U.

The second derivative convention is: hess i j is the weak jth derivative of the ith gradient coordinate.

• hess : Fin d → Fin d → Vec d → ℝ

  L² representatives of the weak derivatives of gradient coordinates: hess i j differentiates the ith coordinate in direction j.

• hess_memL2 (i j : Fin d) : MemScalarL2 U (self.hess i j)
• weak_second (i j : Fin d) : HasWeakPartialDerivOn U j (fun (x : Vec d) => u.grad x i) (self.hess i j)

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

Unpack the weak second-derivative identity for one Hessian coordinate.

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

The L²(U) realization of one Hessian coordinate.

Equations

• H.hessCoordToScalarL2 i j = HCPolySupport.toScalarL2 ⋯

noncomputable def HCPolySupport.HasWeakHessianOn.hessianCoordL2NormSum {d : ℕ} {U : Set (Vec d)} {u : H1Function U} (H : HasWeakHessianOn U u) : ℝ

Sum of scalar L² norms over all Hessian coordinates. This is the quantity the interior estimate should bound.

Equations

• H.hessianCoordL2NormSum = ∑ i : Fin d, ∑ j : Fin d, ‖H.hessCoordToScalarL2 i j‖

theorem HCPolySupport.HasWeakHessianOn.hessianCoordL2NormSum_nonneg {d : ℕ} {U : Set (Vec d)} {u : H1Function U} (H : HasWeakHessianOn U u) : 0 ≤ H.hessianCoordL2NormSum

noncomputable def HCPolySupport.HasWeakHessianOn.restrict {d : ℕ} {U : Set (Vec d)} {u : H1Function U} (H : HasWeakHessianOn U u) {V : Set (Vec d)} (hVopen : IsOpen V) (hVU : V ⊆ U) : HasWeakHessianOn V (u.restrict hVopen hVU)

Restrict a weak Hessian witness to a smaller open set.

Equations

• H.restrict hVopen hVU = { hess := H.hess, hess_memL2 := ⋯, weak_second := ⋯ }

noncomputable def HCPolySupport.weakHessianOfSmoothCompactSupport {d : ℕ} {U : Set (Vec d)} (hU : IsOpen U) {f : Vec d → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hfs : HasCompactSupport f) : HasWeakHessianOn U (H1Function.ofContDiff hU ⋯ hfs)

Smooth compactly supported functions carry the classical Hessian as a weak L² Hessian witness. This fixes the sign and coordinate convention for the future nonsmooth interior theorem.

Equations

• HCPolySupport.weakHessianOfSmoothCompactSupport hU hf hfs = { hess := fun (i j : Fin d) => HCPolySupport.euclideanCoordSecondDeriv i j f, hess_memL2 := ⋯, weak_second := ⋯ }

theorem HCPolySupport.WeakPoissonEquationOn.test {d : ℕ} {U : Set (Vec d)} {u : H1Function U} {f : Vec d → ℝ} (h : WeakPoissonEquationOn U u f) (φ : Vec d → ℝ) (hφ : ContDiff ℝ (↑⊤) φ) (hφs : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ U) : ∫ (x : Vec d) in U, vecDot (u.grad x) (euclideanGradient φ x) = ∫ (x : Vec d) in U, f x * φ x

Unpack a weak Poisson equation at a smooth compactly supported test.

theorem HCPolySupport.WeakPoissonEquationOn.restrict {d : ℕ} {U : Set (Vec d)} {u : H1Function U} {f : Vec d → ℝ} (h : WeakPoissonEquationOn U u f) {V : Set (Vec d)} (hVopen : IsOpen V) (hVU : V ⊆ U) : WeakPoissonEquationOn V (u.restrict hVopen hVU) f

Restrict a weak Poisson equation to a smaller open set.

theorem HCPolySupport.WeakPoissonEquationOn.translate {d : ℕ} {U : Set (Vec d)} {u : H1Function U} {f : Vec d → ℝ} (h : WeakPoissonEquationOn U u f) (z : Vec d) : WeakPoissonEquationOn (translateSet z U) (u.translate z) fun (x : Vec d) => f (x - z)

Translate a weak Poisson equation.

theorem HCPolySupport.WeakPoissonEquationOn.smul {d : ℕ} {U : Set (Vec d)} {u : H1Function U} {f : Vec d → ℝ} (h : WeakPoissonEquationOn U u f) (c : ℝ) : WeakPoissonEquationOn U (c • u) fun (x : Vec d) => c * f x

Scale a weak Poisson equation by a real constant.

theorem HCPolySupport.WeakPoissonEquationOn.h10 {d : ℕ} {U : Set (Vec d)} {u : H1Function U} {f : Vec d → ℝ} (h : WeakPoissonEquationOn U u f) (hU : IsOpen U) (hf : MemScalarL2 U f) (φ : H10Function U) : ∫ (x : Vec d) in U, vecDot (u.grad x) (φ.grad x) = ∫ (x : Vec d) in U, f x * φ.toFun x

Extend a weak Poisson equation from smooth compactly supported tests to all H¹₀ tests. This is the legal-testing bridge needed by the difference-quotient interior estimate.

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.weakPoissonEquationOnCube {d : ℕ} {Q : TriadicCube d} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution Q F) (hmean : cubeAverage Q F = 0) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) : WeakPoissonEquationOn (openCubeSet Q) W.w.toH1Function F

The original cube Neumann solution is a weak Poisson solution on the cube, packaged in the WeakPoissonEquationOn interface used by the difference quotient interior estimates.

theorem HCPolySupport.MeanZeroNeumannPoissonSolution.cubeFaceReflectionBlockFold_weakPoissonEquationOn {d : ℕ} {Q : TriadicCube d} {F : Vec d → ℝ} (W : MeanZeroNeumannPoissonSolution Q F) (hmean : cubeAverage Q F = 0) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) : WeakPoissonEquationOn (cubeFaceReflectionBlockSet Q) W.w.toH1Function.cubeFaceReflectionBlockFold (cubeCoordinateFoldReflectedScalar Q F)

The all-coordinate even reflection of a cube Neumann solution is a weak Poisson solution on the full reflection block.

This is the first bridge needed by the difference-quotient proof: the hard future theorem should consume WeakPoissonEquationOn; the reflection stack already proves the same identity in reflected-vector-field notation.