Coarse-graining support: Support.Sobolev.W1p.ConvexApproxSmoothing.WeakDerivSmoothing #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Weak derivatives of the convex smoothing operator #
Lifts HasWeakPartialDerivOn (and the HasWeakGradientOn gradient variant)
through convexApproxSmoothing and the globally smooth representative
convexApproxSmoothRepresentative.
theorem
HCPolySupport.HasWeakPartialDerivOn.convexApproxSmoothing
{d : ℕ}
{U : Set (Vec d)}
(hU : IsOpenBoundedConvexDomain U)
{i : Fin d}
{u gi ρ : Vec d → ℝ}
(huLoc : MeasureTheory.LocallyIntegrableOn u U MeasureTheory.volume)
(hgiLoc : MeasureTheory.LocallyIntegrableOn gi U MeasureTheory.volume)
(hu : HasWeakPartialDerivOn U i u gi)
(hρ : IsConvexApproxKernel ρ)
{x0 : Vec d}
{r ε : ℝ}
(hball : Metric.closedBall x0 r ⊆ U)
(hr : 0 ≤ r)
(hε0 : 0 ≤ ε)
(hε1 : ε < 1)
:
HasWeakPartialDerivOn U i (HCPolySupport.convexApproxSmoothing ρ u x0 r ε) fun (x : Vec d) =>
(1 - ε) * HCPolySupport.convexApproxSmoothing ρ gi x0 r ε x
theorem
HCPolySupport.HasWeakGradientOn.convexApproxSmoothing
{d : ℕ}
{U : Set (Vec d)}
(hU : IsOpenBoundedConvexDomain U)
{u : Vec d → ℝ}
{Du : Vec d → Vec d}
{ρ : Vec d → ℝ}
(huLoc : MeasureTheory.LocallyIntegrableOn u U MeasureTheory.volume)
(hDuLoc : ∀ (i : Fin d), MeasureTheory.LocallyIntegrableOn (fun (x : Vec d) => Du x i) U MeasureTheory.volume)
(hu : HasWeakGradientOn U u Du)
(hρ : IsConvexApproxKernel ρ)
{x0 : Vec d}
{r ε : ℝ}
(hball : Metric.closedBall x0 r ⊆ U)
(hr : 0 ≤ r)
(hε0 : 0 ≤ ε)
(hε1 : ε < 1)
:
HasWeakGradientOn U (HCPolySupport.convexApproxSmoothing ρ u x0 r ε) fun (x : Vec d) (i : Fin d) =>
(1 - ε) * HCPolySupport.convexApproxSmoothing ρ (fun (y : Vec d) => Du y i) x0 r ε x
theorem
HCPolySupport.HasWeakPartialDerivOn.convexApproxSmoothRepresentative
{d : ℕ}
{U : Set (Vec d)}
(hU : IsOpenBoundedConvexDomain U)
{i : Fin d}
{u gi ρ : Vec d → ℝ}
(huLoc : MeasureTheory.LocallyIntegrableOn u U MeasureTheory.volume)
(hgiLoc : MeasureTheory.LocallyIntegrableOn gi U MeasureTheory.volume)
(hu : HasWeakPartialDerivOn U i u gi)
(hρ : IsConvexApproxKernel ρ)
{x0 : Vec d}
{r ε : ℝ}
(hball : Metric.closedBall x0 r ⊆ U)
(hr : 0 < r)
(hε0 : 0 < ε)
(hε1 : ε < 1)
:
HasWeakPartialDerivOn U i (HCPolySupport.convexApproxSmoothRepresentative U ρ u x0 r ε) fun (x : Vec d) =>
(1 - ε) * HCPolySupport.convexApproxSmoothRepresentative U ρ gi x0 r ε x
theorem
HCPolySupport.HasWeakGradientOn.convexApproxSmoothRepresentative
{d : ℕ}
{U : Set (Vec d)}
(hU : IsOpenBoundedConvexDomain U)
{u : Vec d → ℝ}
{Du : Vec d → Vec d}
{ρ : Vec d → ℝ}
(huLoc : MeasureTheory.LocallyIntegrableOn u U MeasureTheory.volume)
(hDuLoc : ∀ (i : Fin d), MeasureTheory.LocallyIntegrableOn (fun (x : Vec d) => Du x i) U MeasureTheory.volume)
(hu : HasWeakGradientOn U u Du)
(hρ : IsConvexApproxKernel ρ)
{x0 : Vec d}
{r ε : ℝ}
(hball : Metric.closedBall x0 r ⊆ U)
(hr : 0 < r)
(hε0 : 0 < ε)
(hε1 : ε < 1)
:
HasWeakGradientOn U (HCPolySupport.convexApproxSmoothRepresentative U ρ u x0 r ε) fun (x : Vec d) (i : Fin d) =>
(1 - ε) * HCPolySupport.convexApproxSmoothRepresentative U ρ (fun (y : Vec d) => Du y i) x0 r ε x