Coarse-graining support:

Support.Sobolev.Foundations.CubeCalderonZygmund.ReflectedHessianRowOneLevelTail

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

One-level tails for Hessian rows of scalar Dirichlet solutions

This file crosses the global good-lambda seam for one weak-Hessian row. It constructs both the source Hessian and the canonical half-parent Hessian, identifies their rows by mixed-parity reflection, and transfers the interior one-level estimate back to the source cube. No regularity, comparison, or reflection premise is exposed to the caller.

noncomputable def HCPolySupport.CubeCalderonZygmund.reflectedHessianRowGoodLambdaCutoff {d : ℕ} {m : ℤ} (depth : ℕ) (eps : ℝ) {u : H1Function (openCubeSet (originCube d m))} (H : HasWeakHessianOn (openCubeSet (originCube d m)) u) (F : Vec d → ℝ) : ℝ

A source-facing large-scale cutoff for one reflected Hessian row. The first energy is bounded by the source weak-H² coordinate sum; the second is the exact raw source scalar L² energy.

Equations

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

theorem HCPolySupport.CubeCalderonZygmund.reflectedHessianRowGoodLambdaCutoff_nonneg {d : ℕ} {m : ℤ} (depth : ℕ) (eps : ℝ) {u : H1Function (openCubeSet (originCube d m))} (H : HasWeakHessianOn (openCubeSet (originCube d m)) u) (F : Vec d → ℝ) : 0 ≤ reflectedHessianRowGoodLambdaCutoff depth eps H F

theorem HCPolySupport.CubeCalderonZygmund.exists_hasWeakHessianOn_sqWeightedMeasure_oneLevel_tail_originCube {d : ℕ} [NeZero d] {q : FiniteLpExponent} {depth : ℕ} (G : INTERNAL.HarmonicEuclideanGradientGain d q depth) (hq : 2 < q.exponent.toReal) {m : ℤ} {eps M : ℝ} (heps : 0 < eps) (heps_one : eps ≤ 1) (hM : 1 ≤ M) (F : Vec d → ℝ) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure (originCube d m))) (u : H10Function (openCubeSet (originCube d m))) (hweak : CubeDirichletWeakPoissonProblem (originCube d m) u F) : ∃ (H : HasWeakHessianOn (openCubeSet (originCube d m)) u.toH1Function), H.hessianCoordL2NormSum ≤ CubeDirichletWeakPoissonProblem.cubeDirichletH2RegularityConstantExact (originCube d m) * cubeLpNorm (originCube d m) 2 F ∧ ∀ (i : Fin d) (level : ℝ), reflectedHessianRowGoodLambdaCutoff depth eps H F < level → (sqWeightedMeasure (hilbertifyVecField fun (x : Vec d) (j : Fin d) => H.hess i j x) MeasureTheory.volume) ({x : Vec d | M * level < ‖hilbertifyVecField (fun (y : Vec d) (j : Fin d) => H.hess i j y) x‖} ∩ openCubeSet (originCube d m)) ≤ 3 ^ d * oneStoppingBallCoefficient depth G * (ENNReal.ofReal ((M / 2) ^ (2 - q.exponent.toReal)) + ENNReal.ofReal (eps ^ 2)) * ((sqWeightedMeasure (hilbertifyVecField fun (x : Vec d) (j : Fin d) => H.hess i j x) MeasureTheory.volume) ({x : Vec d | level / 2 < ‖hilbertifyVecField (fun (y : Vec d) (j : Fin d) => H.hess i j y) x‖} ∩ openCubeSet (originCube d m)) + ENNReal.ofReal (eps⁻¹ ^ 2) * (sqWeightedMeasure F MeasureTheory.volume) ({x : Vec d | eps * level / 2 < ‖F x‖} ∩ openCubeSet (originCube d m)))

The global source-cube one-level good-lambda estimate for every Hessian row of a scalar Dirichlet Poisson solution. All weak Hessians, reflected representatives, local equations, and tail transfers are constructed inside the theorem.