LocalizedInteriorSkew

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

The local antisymmetric identity for bounded H¹ functions

This file upgrades the antisymmetric transfer to the bounded H¹ carrier needed by an interior localization. No trace condition is imposed on the function: every test is compactly supported in the domain.

def DivergenceFormProcess.Decay.clippedSquareSlope (M t : ℝ) : ℝ

The clipped derivative used to form a square with bounded slope.

Equations

• DivergenceFormProcess.Decay.clippedSquareSlope M t = max (-2 * M) (min (2 * t) (2 * M))

noncomputable def DivergenceFormProcess.Decay.boundedSquare (M t : ℝ) : ℝ

The primitive of the clipped square slope, normalized to vanish at zero.

Equations

• DivergenceFormProcess.Decay.boundedSquare M t = ∫ (s : ℝ) in 0..t, DivergenceFormProcess.Decay.clippedSquareSlope M s

theorem DivergenceFormProcess.Decay.boundedSquare_contDiff_one (M : ℝ) : ContDiff ℝ 1 (boundedSquare M)

theorem DivergenceFormProcess.Decay.deriv_boundedSquare (M : ℝ) : deriv (boundedSquare M) = clippedSquareSlope M

theorem DivergenceFormProcess.Decay.abs_clippedSquareSlope_le {M : ℝ} (hM : 0 ≤ M) (t : ℝ) : |clippedSquareSlope M t| ≤ 2 * M

theorem DivergenceFormProcess.Decay.boundedSquare_eq_sq {M t : ℝ} (hM : 0 ≤ M) (ht : |t| ≤ M) : boundedSquare M t = t ^ 2

noncomputable def DivergenceFormProcess.Decay.boundedSquareH1 {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) (u : HCPolySupport.H1Function U) (M : ℝ) (hM : 0 ≤ M) (hu : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, |u.toFun x| ≤ M) : HCPolySupport.H1Function U

The H¹ composition with the bounded-slope square function.

Equations

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

theorem DivergenceFormProcess.Decay.integral_mul_vecDot_matVecMul_eq_half_interior {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {k : HCPolySupport.Vec d → HCPolySupport.Mat d} (hk : ∀ (p q : Fin d), ContDiff ℝ 1 fun (x : HCPolySupport.Vec d) => k x p q) (hskew : ∀ (x : HCPolySupport.Vec d), HCPolySupport.matTranspose (k x) = -k x) (u : HCPolySupport.H1Function U) {w : HCPolySupport.Vec d → ℝ} (hw : ContDiff ℝ (↑⊤) w) (hwc : HasCompactSupport w) (hwU : tsupport w ⊆ U) {M : ℝ} (hM : 0 ≤ M) (hu : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, |u.toFun x| ≤ M) : (∫ (x : HCPolySupport.Vec d) in U, u.toFun x * HCPolySupport.vecDot (HCPolySupport.matVecMul (k x) (u.grad x)) fun (i : Fin d) => (fderiv ℝ w x) (HCPolySupport.basisVec i)) = 1 / 2 * ∫ (x : HCPolySupport.Vec d) in U, u.toFun x ^ 2 * HCPolySupport.vecDot (skewFieldDiv k x) fun (i : Fin d) => (fderiv ℝ w x) (HCPolySupport.basisVec i)

For a bounded H¹ function and a smooth multiplier supported in the domain, a C¹ skew field contributes only through its divergence. The compactly supported multiplier removes the boundary term, so the function itself need not have zero trace.