CutoffTest

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

Smooth localizations of an H¹ function as zero-trace tests

The weighted energy estimates of this directory test the divergence-form equation with phi * u, where u is the solution itself and phi is a smooth compactly supported multiplier whose topological support lies in the domain. This file records that product as an honest H10Function together with its value and its product-rule weak gradient.

There are two ways for a multiplier to be admissible. Either its topological support lies in the domain, in which case the product is a zero-trace function for every H¹ factor; or the factor itself already has zero trace, in which case no support condition on the multiplier is needed. Both are recorded as IsAdmissibleMultiplier, which is what the weighted estimates consume. The first uses the localized product of the cutoff-test module, DivergenceFormProcess.Form.localizedProductToH10.

Main definitions

• DivergenceFormProcess.Decay.IsAdmissibleMultiplier.

Main results

• DivergenceFormProcess.Decay.isAdmissibleMultiplier_of_tsupport_subset
• DivergenceFormProcess.Decay.isAdmissibleMultiplier_of_zeroTrace

def DivergenceFormProcess.Decay.IsAdmissibleMultiplier {d : ℕ} (U : Set (HCPolySupport.Vec d)) (u : HCPolySupport.H1Function U) (phi : HCPolySupport.Vec d → ℝ) : Prop

A multiplier is admissible for u when the product phi * u is realized by a zero-trace function whose weak gradient obeys the product rule. This is the only property of the test function the weighted estimates use.

Equations

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

theorem DivergenceFormProcess.Decay.isAdmissibleMultiplier_of_tsupport_subset {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) (u : HCPolySupport.H1Function U) {phi : HCPolySupport.Vec d → ℝ} (hphi : ContDiff ℝ (↑⊤) phi) (hphiCompact : HasCompactSupport phi) (hphiU : tsupport phi ⊆ U) : IsAdmissibleMultiplier U u phi

A smooth compactly supported multiplier supported in the domain is admissible for every H¹ function.

theorem DivergenceFormProcess.Decay.isAdmissibleMultiplier_of_zeroTrace {d : ℕ} {U : Set (HCPolySupport.Vec d)} (z : HCPolySupport.H10Function U) {phi : HCPolySupport.Vec d → ℝ} (hphi : ContDiff ℝ (↑⊤) phi) (hphiCompact : HasCompactSupport phi) : IsAdmissibleMultiplier U z.toH1Function phi

For a factor with zero trace, every smooth compactly supported multiplier is admissible: no support condition inside the domain is needed.