Coarse-graining support: Support.Sobolev.W1p.ConvexApproxSmoothing.SmoothRepresentative

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Smooth representative, measurability, and L^p bounds for the convex smoothing

Defines the globally smooth representative convexApproxSmoothRepresentative and collects the measurability, eLpNorm control, and integrability lemmas needed downstream: measurable-embedding of convexApproxSample, map of the restricted volume measure, eLpNorm_comp_convexApproxSample_le, eLpNorm_convexApproxSmoothing_le, aestronglyMeasurable_/memLpOn_ variants, the a.e. equality of smoothing vs. its representative, and integrability of fun y => u ∘ convexApproxSample y against a finite measure.

noncomputable def HCPolySupport.convexApproxSmoothRepresentative {d : ℕ} (U : Set (Vec d)) (ρ u : Vec d → ℝ) (x0 : Vec d) (r ε : ℝ) : Vec d → ℝ

A globally defined smooth representative for the convex-domain smoothing operator.

Equations

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

theorem HCPolySupport.contDiff_convexApproxSmoothRepresentative {d : ℕ} {U : Set (Vec d)} {ρ u : Vec d → ℝ} {p : ENNReal} (hU : MeasurableSet U) (hρ : IsConvexApproxKernel ρ) (hp1 : 1 ≤ p) (hu : MemLpOn U p u) {x0 : Vec d} {r ε : ℝ} (hr : 0 < r) (hε0 : 0 < ε) : ContDiff ℝ (↑⊤) (convexApproxSmoothRepresentative U ρ u x0 r ε)

theorem HCPolySupport.convexApproxSmoothRepresentative_eq_convexApproxSmoothing_of_mem {d : ℕ} {U : Set (Vec d)} {ρ u : Vec d → ℝ} (hU : IsOpenBoundedConvexDomain U) (hρ : IsConvexApproxKernel ρ) {x0 x : Vec d} {r ε : ℝ} (hx : x ∈ U) (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 < r) (hε0 : 0 < ε) (hε1 : ε < 1) : convexApproxSmoothRepresentative U ρ u x0 r ε x = convexApproxSmoothing ρ u x0 r ε x

theorem HCPolySupport.measurableEmbedding_convexApproxSample {d : ℕ} (x0 z : Vec d) (r ε : ℝ) (hε1 : ε < 1) : MeasurableEmbedding (convexApproxSample x0 z r ε)

theorem HCPolySupport.map_restrict_convexApproxSample {d : ℕ} {U : Set (Vec d)} (_hU : MeasurableSet U) (x0 z : Vec d) (r ε : ℝ) (hε1 : ε < 1) : MeasureTheory.Measure.map (convexApproxSample x0 z r ε) (MeasureTheory.volume.restrict U) = ENNReal.ofReal ((1 - ε) ^ d)⁻¹ • MeasureTheory.volume.restrict (convexApproxSample x0 z r ε '' U)

theorem HCPolySupport.eLpNorm_comp_convexApproxSample_le {d : ℕ} {U : Set (Vec d)} {u : Vec d → ℝ} {p : ENNReal} (hp : p ≠ ⊤) (hU : MeasurableSet U) (x0 z : Vec d) (r ε : ℝ) (hε1 : ε < 1) (hmap : convexApproxSample x0 z r ε '' U ⊆ U) : MeasureTheory.eLpNorm (fun (x : Vec d) => u (convexApproxSample x0 z r ε x)) p (MeasureTheory.volume.restrict U) ≤ ENNReal.ofReal ((1 - ε) ^ d)⁻¹ ^ (1 / p).toReal * MeasureTheory.eLpNorm u p (MeasureTheory.volume.restrict U)

theorem HCPolySupport.eLpNorm_convexApproxSmoothing_le {d : ℕ} {U : Set (Vec d)} {ρ u : Vec d → ℝ} {p : ENNReal} (hU : IsOpenBoundedConvexDomain U) (hρ : IsConvexApproxKernel ρ) (hp1 : 1 ≤ p) (hp : p ≠ ⊤) (hu : MemLpOn U p u) {x0 : Vec d} {r ε : ℝ} (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 < r) (hε0 : 0 < ε) (hε1 : ε < 1) : MeasureTheory.eLpNorm (convexApproxSmoothing ρ u x0 r ε) p (MeasureTheory.volume.restrict U) ≤ ENNReal.ofReal ((1 - ε) ^ d)⁻¹ ^ (1 / p).toReal * MeasureTheory.eLpNorm u p (MeasureTheory.volume.restrict U)

theorem HCPolySupport.aestronglyMeasurable_convexApproxSmoothing {d : ℕ} {U : Set (Vec d)} {ρ u : Vec d → ℝ} {p : ENNReal} (hU : IsOpenBoundedConvexDomain U) (hρ : IsConvexApproxKernel ρ) (hp1 : 1 ≤ p) (hu : MemLpOn U p u) {x0 : Vec d} {r ε : ℝ} (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 < r) (hε0 : 0 < ε) (hε1 : ε < 1) : MeasureTheory.AEStronglyMeasurable (convexApproxSmoothing ρ u x0 r ε) (MeasureTheory.volume.restrict U)

theorem HCPolySupport.memLpOn_convexApproxSmoothing {d : ℕ} {U : Set (Vec d)} {ρ u : Vec d → ℝ} {p : ENNReal} (hU : IsOpenBoundedConvexDomain U) (hρ : IsConvexApproxKernel ρ) (hp1 : 1 ≤ p) (hp : p ≠ ⊤) (hu : MemLpOn U p u) {x0 : Vec d} {r ε : ℝ} (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 < r) (hε0 : 0 < ε) (hε1 : ε < 1) : MemLpOn U p (convexApproxSmoothing ρ u x0 r ε)

theorem HCPolySupport.convexApproxSmoothing_sub_ae_eq {d : ℕ} {U : Set (Vec d)} {ρ u v : Vec d → ℝ} {p : ENNReal} (hU : IsOpenBoundedConvexDomain U) (hρ : IsConvexApproxKernel ρ) (hp1 : 1 ≤ p) (hu : MemLpOn U p u) (hv : MemLpOn U p v) {x0 : Vec d} {r ε : ℝ} (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 < r) (hε0 : 0 < ε) (hε1 : ε < 1) : (fun (x : Vec d) => convexApproxSmoothing ρ (fun (y : Vec d) => u y - v y) x0 r ε x) =ᵐ[MeasureTheory.volume.restrict U] fun (x : Vec d) => convexApproxSmoothing ρ u x0 r ε x - convexApproxSmoothing ρ v x0 r ε x

theorem HCPolySupport.eLpNorm_sub_convexApproxSmoothing_le {d : ℕ} {U : Set (Vec d)} {ρ u v : Vec d → ℝ} {p : ENNReal} (hU : IsOpenBoundedConvexDomain U) (hρ : IsConvexApproxKernel ρ) (hp1 : 1 ≤ p) (hp : p ≠ ⊤) (hu : MemLpOn U p u) (hv : MemLpOn U p v) {x0 : Vec d} {r ε : ℝ} (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 < r) (hε0 : 0 < ε) (hε1 : ε < 1) : MeasureTheory.eLpNorm (fun (x : Vec d) => convexApproxSmoothing ρ u x0 r ε x - convexApproxSmoothing ρ v x0 r ε x) p (MeasureTheory.volume.restrict U) ≤ ENNReal.ofReal ((1 - ε) ^ d)⁻¹ ^ (1 / p).toReal * MeasureTheory.eLpNorm (fun (x : Vec d) => u x - v x) p (MeasureTheory.volume.restrict U)

theorem HCPolySupport.integrableOn_comp_smul_add_of_pos {d : ℕ} {s : Set (Vec d)} {u : Vec d → ℝ} {a : ℝ} (ha : 0 < a) (b : Vec d) (hs : MeasurableSet s) (hu : MeasureTheory.IntegrableOn u (translateSet b (a • s)) MeasureTheory.volume) : MeasureTheory.IntegrableOn (fun (x : Vec d) => u (a • x + b)) s MeasureTheory.volume

theorem HCPolySupport.integrableOn_comp_convexApproxSample {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {u : Vec d → ℝ} (hu : MeasureTheory.IntegrableOn u U MeasureTheory.volume) {x0 z : Vec d} {r ε : ℝ} (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 ≤ r) (hz : ‖z‖ ≤ 1) (hε0 : 0 ≤ ε) (hε1 : ε < 1) : MeasureTheory.IntegrableOn (fun (x : Vec d) => u (convexApproxSample x0 z r ε x)) U MeasureTheory.volume

theorem HCPolySupport.integrableOn_comp_convexApproxSample_of_locallyIntegrableOn {d : ℕ} {U K : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {u : Vec d → ℝ} (hu : MeasureTheory.LocallyIntegrableOn u U MeasureTheory.volume) (hK_sub : K ⊆ U) (hK_compact : IsCompact K) {x0 z : Vec d} {r ε : ℝ} (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 ≤ r) (hz : ‖z‖ ≤ 1) (hε0 : 0 ≤ ε) (hε1 : ε < 1) : MeasureTheory.IntegrableOn (fun (x : Vec d) => u (convexApproxSample x0 z r ε x)) K MeasureTheory.volume

theorem HCPolySupport.integrableOn_indicator_comp_convexApproxSample_mul_of_locallyIntegrableOn {d : ℕ} {U K : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {u ψ : Vec d → ℝ} (hu : MeasureTheory.LocallyIntegrableOn u U MeasureTheory.volume) (hψ : Continuous ψ) (hK_sub : K ⊆ U) (hK_compact : IsCompact K) {x0 z : Vec d} {r ε : ℝ} (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 ≤ r) (hz : ‖z‖ ≤ 1) (hε0 : 0 ≤ ε) (hε1 : ε < 1) : MeasureTheory.IntegrableOn (fun (x : Vec d) => U.indicator u (convexApproxSample x0 z r ε x) * ψ x) K MeasureTheory.volume

theorem HCPolySupport.integrableOn_kernel_mul_indicator_comp_convexApproxSample_mul_of_locallyIntegrableOn {d : ℕ} {U K : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {u ρ ψ : Vec d → ℝ} (hu : MeasureTheory.LocallyIntegrableOn u U MeasureTheory.volume) (hψ : Continuous ψ) (hK_sub : K ⊆ U) (hK_compact : IsCompact K) {x0 z : Vec d} {r ε : ℝ} (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 ≤ r) (hz : ‖z‖ ≤ 1) (hε0 : 0 ≤ ε) (hε1 : ε < 1) : MeasureTheory.IntegrableOn (fun (x : Vec d) => ρ z * U.indicator u (convexApproxSample x0 z r ε x) * ψ x) K MeasureTheory.volume