OneStepEvenBoundHessian

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The two analytic atoms of the even-part bound (★)

The boundary branch of the Schauder gradient-Hölder estimate closes its even part by comparing the harmonic competitor with its own first-order Taylor polynomial at a point of the window and paying the resulting quadratic remainder against the Hessian. This module supplies the two atoms that argument consumes:

1. Second-order Taylor with a Hessian remainder on a convex set. For u twice differentiable on a convex S with ‖D²u‖ ≤ M there,

     |u(q) − u(p) − Du(p)(q − p)| ≤ M · ‖q − p‖² ,     p, q ∈ S .
   

   The route is the mean-value inequality applied twice on the segment [p, q] ⊆ S: once to Du (giving ‖Du(z) − Du(p)‖ ≤ M‖q − p‖ along the segment) and once, in the φ-corrected form Convex.norm_image_sub_le_of_norm_fderiv_le', to u itself. The constant is M rather than the sharp M/2; the even-part bound is insensitive to that factor. A Vec d shape is provided as well, obtained by transporting the convex set through the coordinate identification toEuc.

2. The interior Hessian estimate re-read against the volume-normalized L² seminorm. The transplanted native estimate interiorSecondDerivEstimateL2 measures the data by the CoarseGraining mean-square deviation on the concentric Euclidean ball. The boundary branch instead carries its data as Support.normalizedL2On W V on an arbitrary window W that merely contains a sup-ball Metric.ball p r at the point. Rebasing costs exactly the volume ratio |W| / |euclideanBall p (r/2)|, which the scale-free lower bound volume_toReal_euclideanBall_ge converts into the explicit factor (|W| / rᵈ) · (2(d+1))ᵈ; taking square roots gives

     ‖D²V(p)‖ ≤ C(d) · r⁻¹ · r⁻¹ · √(|W| / rᵈ) · ‖V‖_{L²(W)} ,
   

   with C(d) = 4 · C_native(d) · √((2(d+1))ᵈ), the 4 absorbing (r/2)⁻¹(r/2)⁻¹ = 4r⁻¹r⁻¹.

1. Differentiability from harmonicity

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.differentiableAt_of_harmonicAt {d : ℕ} {u : EuclideanSpace ℝ (Fin d) → ℝ} {z : EuclideanSpace ℝ (Fin d)} (h : InnerProductSpace.HarmonicAt u z) : DifferentiableAt ℝ u z

A harmonic function is differentiable at each point of harmonicity.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.differentiableAt_fderiv_of_harmonicAt {d : ℕ} {u : EuclideanSpace ℝ (Fin d) → ℝ} {z : EuclideanSpace ℝ (Fin d)} (h : InnerProductSpace.HarmonicAt u z) : DifferentiableAt ℝ (fderiv ℝ u) z

The derivative of a harmonic function is differentiable at each point of harmonicity.

2. Second-order Taylor with a Hessian remainder

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.abs_sub_fderiv_apply_le_of_hessian_bound {d : ℕ} {u : EuclideanSpace ℝ (Fin d) → ℝ} {S : Set (EuclideanSpace ℝ (Fin d))} (hS : Convex ℝ S) (hdiff : ∀ z ∈ S, DifferentiableAt ℝ u z) (hdiff2 : ∀ z ∈ S, DifferentiableAt ℝ (fderiv ℝ u) z) {M : ℝ} (hM : ∀ z ∈ S, ‖fderiv ℝ (fderiv ℝ u) z‖ ≤ M) {p q : EuclideanSpace ℝ (Fin d)} (hp : p ∈ S) (hq : q ∈ S) : |u q - u p - (fderiv ℝ u p) (q - p)| ≤ M * ‖q - p‖ ^ 2

Second-order Taylor with a Hessian remainder on a convex set.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.abs_sub_fderiv_apply_le_of_hessian_bound_vec {d : ℕ} {V : HCPolySupport.Vec d → ℝ} {S : Set (HCPolySupport.Vec d)} (hS : Convex ℝ S) (hharm : ∀ z ∈ S, InnerProductSpace.HarmonicAt (V ∘ ⇑toEuc.symm) (toEuc z)) {M : ℝ} (hM : ∀ z ∈ S, ‖fderiv ℝ (fderiv ℝ (V ∘ ⇑toEuc.symm)) (toEuc z)‖ ≤ M) {p q : HCPolySupport.Vec d} (hp : p ∈ S) (hq : q ∈ S) : |V q - V p - (fderiv ℝ (V ∘ ⇑toEuc.symm) (toEuc p)) (toEuc q - toEuc p)| ≤ M * ‖toEuc q - toEuc p‖ ^ 2

Second-order Taylor, Vec d shape.

3. Coefficient algebra for the normalized Hessian estimate

4. The interior Hessian estimate against the normalized L² seminorm

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.exists_hessian_normalizedL2On_bound (d : ℕ) [NeZero d] : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (W : Set (HCPolySupport.Vec d)) (V : HCPolySupport.Vec d → ℝ) (p : HCPolySupport.Vec d) (r : ℝ), MeasureTheory.volume W ≠ ⊤ → 0 < (MeasureTheory.volume W).toReal → InnerProductSpace.HarmonicOnNhd (V ∘ ⇑toEuc.symm) (⇑toEuc '' W) → MeasureTheory.IntegrableOn (fun (y : HCPolySupport.Vec d) => V y ^ 2) W MeasureTheory.volume → 0 < r → Metric.ball p r ⊆ W → ‖fderiv ℝ (fderiv ℝ (V ∘ ⇑toEuc.symm)) (toEuc p)‖ ≤ C * r⁻¹ * r⁻¹ * √((MeasureTheory.volume W).toReal / r ^ d) * Support.normalizedL2On W V

The interior Hessian estimate against the normalized L² seminorm of the window. For V classically harmonic on W and a point p carrying a sup-ball of radius r inside W.