Coarse-graining support: Support.Sobolev.W1p.ConvexApproxSmoothing.WeakDerivComp #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Weak partial derivatives of the convexApproxSample composition #
Establishes HasWeakPartialDerivOn.comp_convexApproxSample (plus the gradient
variant) and the product-measure infrastructure that feeds it:
quasi-measure-preservation of convexApproxSample, strong measurability of
indicator products, and integrability of the kernel × indicator × comp tensor
against a locally integrable datum.
theorem
HCPolySupport.HasWeakPartialDerivOn.comp_convexApproxSample
{d : ℕ}
{U : Set (Vec d)}
(hU : IsOpenBoundedConvexDomain U)
{i : Fin d}
{u gi : Vec d → ℝ}
(hu : HasWeakPartialDerivOn U i u gi)
{x0 z : Vec d}
{r ε : ℝ}
(hball : Metric.closedBall x0 r ⊆ U)
(hr : 0 ≤ r)
(hz : ‖z‖ ≤ 1)
(hε0 : 0 ≤ ε)
(hε1 : ε < 1)
:
HasWeakPartialDerivOn U i (fun (x : Vec d) => u (convexApproxSample x0 z r ε x)) fun (x : Vec d) =>
(1 - ε) * gi (convexApproxSample x0 z r ε x)
theorem
HCPolySupport.HasWeakGradientOn.comp_convexApproxSample
{d : ℕ}
{U : Set (Vec d)}
(hU : IsOpenBoundedConvexDomain U)
{u : Vec d → ℝ}
{Du : Vec d → Vec d}
(hu : HasWeakGradientOn U u Du)
{x0 z : Vec d}
{r ε : ℝ}
(hball : Metric.closedBall x0 r ⊆ U)
(hr : 0 ≤ r)
(hz : ‖z‖ ≤ 1)
(hε0 : 0 ≤ ε)
(hε1 : ε < 1)
:
HasWeakGradientOn U (fun (x : Vec d) => u (convexApproxSample x0 z r ε x)) fun (x : Vec d) (i : Fin d) =>
(1 - ε) * Du (convexApproxSample x0 z r ε x) i
theorem
HCPolySupport.quasiMeasurePreserving_convexApproxSample
{d : ℕ}
(x0 z : Vec d)
(r ε : ℝ)
(hε1 : ε < 1)
:
theorem
HCPolySupport.quasiMeasurePreserving_convexApproxSample_prod
{d : ℕ}
{U : Set (Vec d)}
{ρ : Vec d → ℝ}
(_hρ : IsConvexApproxKernel ρ)
(x0 : Vec d)
(r ε : ℝ)
(hε1 : ε < 1)
:
MeasureTheory.QuasiMeasurePreserving (fun (p : Vec d × Vec d) => convexApproxSample x0 p.2 r ε p.1)
((MeasureTheory.volume.restrict U).prod (MeasureTheory.volume.restrict (tsupport ρ))) MeasureTheory.volume
theorem
HCPolySupport.aestronglyMeasurable_indicator_comp_convexApproxSample_prod
{d : ℕ}
{U : Set (Vec d)}
(hU_meas : MeasurableSet U)
{u ρ : Vec d → ℝ}
(hu : MeasureTheory.AEStronglyMeasurable u (MeasureTheory.volume.restrict U))
(hρ : IsConvexApproxKernel ρ)
{x0 : Vec d}
{r ε : ℝ}
(hε1 : ε < 1)
:
MeasureTheory.AEStronglyMeasurable (fun (p : Vec d × Vec d) => U.indicator u (convexApproxSample x0 p.2 r ε p.1))
((MeasureTheory.volume.restrict U).prod (MeasureTheory.volume.restrict (tsupport ρ)))
theorem
HCPolySupport.aestronglyMeasurable_indicator_comp_convexApproxSample_prod_of_locallyIntegrableOn
{d : ℕ}
{U : Set (Vec d)}
(hU_meas : MeasurableSet U)
{u ρ : Vec d → ℝ}
(hu : MeasureTheory.LocallyIntegrableOn u U MeasureTheory.volume)
(hρ : IsConvexApproxKernel ρ)
{x0 : Vec d}
{r ε : ℝ}
(hε1 : ε < 1)
:
MeasureTheory.AEStronglyMeasurable (fun (p : Vec d × Vec d) => U.indicator u (convexApproxSample x0 p.2 r ε p.1))
((MeasureTheory.volume.restrict U).prod (MeasureTheory.volume.restrict (tsupport ρ)))
theorem
HCPolySupport.aestronglyMeasurable_kernel_mul_indicator_comp_convexApproxSample_prod_mul
{d : ℕ}
{U : Set (Vec d)}
(hU_meas : MeasurableSet U)
{u ρ ψ : Vec d → ℝ}
(hu : MeasureTheory.LocallyIntegrableOn u U MeasureTheory.volume)
(hρ : IsConvexApproxKernel ρ)
(hψ : Continuous ψ)
(hψ_sub : tsupport ψ ⊆ U)
{x0 : Vec d}
{r ε : ℝ}
(hε1 : ε < 1)
:
MeasureTheory.AEStronglyMeasurable
(fun (p : Vec d × Vec d) => ρ p.2 * U.indicator u (convexApproxSample x0 p.2 r ε p.1) * ψ p.1)
((MeasureTheory.volume.restrict (tsupport ψ)).prod (MeasureTheory.volume.restrict (tsupport ρ)))
theorem
HCPolySupport.integrable_kernel_mul_indicator_comp_convexApproxSample_prod_mul_of_integrableOn
{d : ℕ}
{U : Set (Vec d)}
(hU : IsOpenBoundedConvexDomain U)
{u ρ ψ : Vec d → ℝ}
(hu : MeasureTheory.IntegrableOn u U MeasureTheory.volume)
(hρ : IsConvexApproxKernel ρ)
(hψ : Continuous ψ)
(hψ_compact : HasCompactSupport ψ)
(hψ_sub : tsupport ψ ⊆ U)
{x0 : Vec d}
{r ε : ℝ}
(hball : Metric.closedBall x0 r ⊆ U)
(hr : 0 ≤ r)
(hε0 : 0 ≤ ε)
(hε1 : ε < 1)
:
MeasureTheory.Integrable (fun (p : Vec d × Vec d) => ρ p.2 * U.indicator u (convexApproxSample x0 p.2 r ε p.1) * ψ p.1)
((MeasureTheory.volume.restrict (tsupport ψ)).prod (MeasureTheory.volume.restrict (tsupport ρ)))
theorem
HCPolySupport.integrable_kernel_mul_indicator_comp_convexApproxSample_prod_mul_of_locallyIntegrableOn
{d : ℕ}
{U : Set (Vec d)}
(hU : IsOpenBoundedConvexDomain U)
{u ρ ψ : Vec d → ℝ}
(hu : MeasureTheory.LocallyIntegrableOn u U MeasureTheory.volume)
(hρ : IsConvexApproxKernel ρ)
(hψ : Continuous ψ)
(hψ_compact : HasCompactSupport ψ)
(hψ_sub : tsupport ψ ⊆ U)
{x0 : Vec d}
{r ε : ℝ}
(hball : Metric.closedBall x0 r ⊆ U)
(hr : 0 ≤ r)
(hε0 : 0 ≤ ε)
(hε1 : ε < 1)
:
MeasureTheory.Integrable (fun (p : Vec d × Vec d) => ρ p.2 * U.indicator u (convexApproxSample x0 p.2 r ε p.1) * ψ p.1)
((MeasureTheory.volume.restrict (tsupport ψ)).prod (MeasureTheory.volume.restrict (tsupport ρ)))