DeGiorgiCutoffTest

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

Localized De Giorgi cutoff tests

This file packages the standard positive-part truncation multiplied by the square of a smooth, compactly supported cutoff. It only combines the existing truncation and H¹₀ product APIs. The localized product itself is recorded separately, since the weighted energy estimates use it without any truncation.

noncomputable def DivergenceFormProcess.Form.localizedProductToH10 {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) (v : HCPolySupport.H1Function U) {phi : HCPolySupport.Vec d → ℝ} (hphi : ContDiff ℝ (↑⊤) phi) (hphiCompact : HasCompactSupport phi) (hphiU : tsupport phi ⊆ U) : HCPolySupport.H10Function U

The product of an H¹ function with a smooth compactly supported multiplier supported in the domain, as a zero-trace function.

Equations

• DivergenceFormProcess.Form.localizedProductToH10 hU v hphi hphiCompact hphiU = Classical.choose ⋯

theorem DivergenceFormProcess.Form.localizedProductToH10_toFun {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) (v : HCPolySupport.H1Function U) {phi : HCPolySupport.Vec d → ℝ} (hphi : ContDiff ℝ (↑⊤) phi) (hphiCompact : HasCompactSupport phi) (hphiU : tsupport phi ⊆ U) : (localizedProductToH10 hU v hphi hphiCompact hphiU).toFun = fun (x : HCPolySupport.Vec d) => phi x * v.toFun x

The localized product is pointwise the product of the multiplier with the value of the H¹ function.

theorem DivergenceFormProcess.Form.localizedProductToH10_grad_ae {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) (v : HCPolySupport.H1Function U) {phi : HCPolySupport.Vec d → ℝ} (hphi : ContDiff ℝ (↑⊤) phi) (hphiCompact : HasCompactSupport phi) (hphiU : tsupport phi ⊆ U) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, (localizedProductToH10 hU v hphi hphiCompact hphiU).grad x = (v.mulContDiffHasCompactSupport hphi hphiCompact).grad x

The weak gradient of the localized product agrees almost everywhere with the gradient of the pointwise product.