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

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

Pointwise bounds for convexApproxSmoothing u − u

Constant and zero-smoothing identities, the weighted-difference integral representation of convexApproxSmoothing u − u, pointwise oscillation / modulus / continuous bounds on |convexApproxSmoothing u − u|, and the eventual-in-ε versions (including the one for the unit sequence), capped off by tendsto_unitConvexApproxSequence_of_continuous.

theorem HCPolySupport.norm_le_one_of_mem_closedBall_zero_one {d : ℕ} {z : Vec d} (hz : z ∈ Metric.closedBall 0 1) : ‖z‖ ≤ 1

theorem HCPolySupport.convexApproxSample_mem_of_tsupport_subset_closedBall {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {ρ : Vec d → ℝ} {x x0 z : Vec d} {r ε : ℝ} (hx : x ∈ U) (hball : Metric.closedBall x0 r ⊆ U) (hρ_sub : tsupport ρ ⊆ Metric.closedBall 0 1) (hz : z ∈ tsupport ρ) (hr : 0 ≤ r) (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) : convexApproxSample x0 z r ε x ∈ U

theorem HCPolySupport.convexApproxSmoothing_const {d : ℕ} {ρ : Vec d → ℝ} (hρ : IsConvexApproxKernel ρ) (c : ℝ) (x0 : Vec d) (r ε : ℝ) (x : Vec d) : convexApproxSmoothing ρ (fun (x : Vec d) => c) x0 r ε x = c

theorem HCPolySupport.convexApproxSmoothing_zero {d : ℕ} {ρ u : Vec d → ℝ} (hρ : IsConvexApproxKernel ρ) (x0 : Vec d) (r : ℝ) (x : Vec d) : convexApproxSmoothing ρ u x0 r 0 x = u x

theorem HCPolySupport.convexApproxSmoothing_sub_eq_setIntegral_weightedDiff {d : ℕ} {ρ u : Vec d → ℝ} (hρ : IsConvexApproxKernel ρ) (hu : Continuous u) (x0 : Vec d) (r ε : ℝ) (x : Vec d) : convexApproxSmoothing ρ u x0 r ε x - u x = ∫ (z : Vec d) in tsupport ρ, ρ z * (u (convexApproxSample x0 z r ε x) - u x)

theorem HCPolySupport.abs_convexApproxSmoothing_sub_le_setIntegral_weightedOscillation {d : ℕ} {ρ u : Vec d → ℝ} (hρ : IsConvexApproxKernel ρ) (hu : Continuous u) (x0 : Vec d) (r ε : ℝ) (x : Vec d) : |convexApproxSmoothing ρ u x0 r ε x - u x| ≤ ∫ (z : Vec d) in tsupport ρ, ρ z * |u (convexApproxSample x0 z r ε x) - u x|

theorem HCPolySupport.abs_convexApproxSmoothing_sub_le_of_pointwiseOscillation {d : ℕ} {ρ u : Vec d → ℝ} (hρ : IsConvexApproxKernel ρ) (hu : Continuous u) (x0 : Vec d) (r ε : ℝ) (x : Vec d) {δ : ℝ} (hosc : ∀ z ∈ tsupport ρ, |u (convexApproxSample x0 z r ε x) - u x| ≤ δ) : |convexApproxSmoothing ρ u x0 r ε x - u x| ≤ δ

theorem HCPolySupport.abs_convexApproxSmoothing_sub_le_of_modulus {d : ℕ} {U : Set (Vec d)} {ρ u : Vec d → ℝ} (hU : IsOpenBoundedConvexDomain U) (hρ : IsConvexApproxKernel ρ) (hu : Continuous u) {x x0 : Vec d} {r ε : ℝ} (hx : x ∈ U) (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 ≤ r) (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) {δ : ℝ} (hmod : ∀ y ∈ U, ‖y - x‖ ≤ ε * (2 * Classical.choose ⋯) → |u y - u x| ≤ δ) : |convexApproxSmoothing ρ u x0 r ε x - u x| ≤ δ

theorem HCPolySupport.exists_pos_forall_abs_convexApproxSmoothing_sub_le_of_continuous {d : ℕ} {U : Set (Vec d)} {ρ u : Vec d → ℝ} (hU : IsOpenBoundedConvexDomain U) (hρ : IsConvexApproxKernel ρ) (hu : Continuous u) {x0 : Vec d} {r : ℝ} (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 ≤ r) {δ : ℝ} (hδ : 0 < δ) : ∃ η > 0, ∀ ⦃x : Vec d⦄, x ∈ U → ∀ ⦃ε : ℝ⦄, 0 ≤ ε → ε ≤ 1 → ε * (2 * Classical.choose ⋯) ≤ η → |convexApproxSmoothing ρ u x0 r ε x - u x| ≤ δ

theorem HCPolySupport.two_mul_choose_isBoundedDomain_nonneg {d : ℕ} {U : Set (Vec d)} (hU : IsBoundedDomain U) : 0 ≤ 2 * Classical.choose hU

theorem HCPolySupport.eventually_forall_abs_convexApproxSmoothing_sub_le_of_continuous {d : ℕ} {U : Set (Vec d)} {ρ u : Vec d → ℝ} (hU : IsOpenBoundedConvexDomain U) (hρ : IsConvexApproxKernel ρ) (hu : Continuous u) {x0 : Vec d} {r : ℝ} (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 ≤ r) {ε : ℕ → ℝ} (hε : Filter.Tendsto ε Filter.atTop (nhds 0)) (hε_nonneg : ∀ᶠ (n : ℕ) in Filter.atTop, 0 ≤ ε n) (hε_le_one : ∀ᶠ (n : ℕ) in Filter.atTop, ε n ≤ 1) {δ : ℝ} (hδ : 0 < δ) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ ⦃x : Vec d⦄, x ∈ U → |convexApproxSmoothing ρ u x0 r (ε n) x - u x| ≤ δ

theorem HCPolySupport.eventually_forall_abs_unitConvexApproxSequence_sub_le_of_continuous {d : ℕ} {U : Set (Vec d)} {u : Vec d → ℝ} (hU : IsOpenBoundedConvexDomain U) (hu : Continuous u) {x0 : Vec d} {r : ℝ} (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 ≤ r) {δ : ℝ} (hδ : 0 < δ) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ ⦃x : Vec d⦄, x ∈ U → |unitConvexApproxSequence u x0 r n x - u x| ≤ δ

theorem HCPolySupport.tendsto_unitConvexApproxSequence_of_continuous {d : ℕ} {U : Set (Vec d)} {u : Vec d → ℝ} (hU : IsOpenBoundedConvexDomain U) (hu : Continuous u) {x0 : Vec d} {r : ℝ} (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 ≤ r) {x : Vec d} (hx : x ∈ U) : Filter.Tendsto (fun (n : ℕ) => unitConvexApproxSequence u x0 r n x) Filter.atTop (nhds (u x))