Coarse-graining support: Support.Sobolev.W1p.ConvexApproxGeometry

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

Convex-domain smoothing geometry

This file isolates the affine sampling map used in the bounded-open-convex domain smooth approximation strategy. The future smoothing operator will sample u at

(1 - ε) • x + ε • (x0 - r • z),

where closedBall x0 r ⊆ U and ‖z‖ ≤ 1. Convexity keeps this sample point inside U.

def HCPolySupport.convexApproxSample {d : ℕ} (x0 z : Vec d) (r ε : ℝ) (x : Vec d) : Vec d

The affine sample point used by the convex-domain smoothing operator.

Equations

• HCPolySupport.convexApproxSample x0 z r ε x = (1 - ε) • x + ε • (x0 - r • z)

@[simp]

theorem HCPolySupport.convexApproxSample_apply {d : ℕ} (x0 z : Vec d) (r ε : ℝ) (x : Vec d) : convexApproxSample x0 z r ε x = (1 - ε) • x + ε • (x0 - r • z)

theorem HCPolySupport.convexApproxSample_eq_segmentBlend {d : ℕ} (x0 z : Vec d) (r ε : ℝ) (x : Vec d) : convexApproxSample x0 z r ε x = segmentBlend (x0 - r • z) ε x

theorem HCPolySupport.continuous_convexApproxSample {d : ℕ} (x0 z : Vec d) (r ε : ℝ) : Continuous (convexApproxSample x0 z r ε)

theorem HCPolySupport.contDiff_convexApproxSample {d : ℕ} (x0 z : Vec d) (r ε : ℝ) {n : ℕ∞} : ContDiff ℝ (↑n) (convexApproxSample x0 z r ε)

theorem HCPolySupport.sub_smul_mem_closedBall {d : ℕ} {x0 z : Vec d} {r : ℝ} (hr : 0 ≤ r) (hz : ‖z‖ ≤ 1) : x0 - r • z ∈ Metric.closedBall x0 r

theorem HCPolySupport.sub_smul_mem_of_closedBall_subset {d : ℕ} {U : Set (Vec d)} {x0 z : Vec d} {r : ℝ} (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 ≤ r) (hz : ‖z‖ ≤ 1) : x0 - r • z ∈ U

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

theorem HCPolySupport.convexApproxSample_mapsTo_of_isOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {x0 z : Vec d} {r ε : ℝ} (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 ≤ r) (hz : ‖z‖ ≤ 1) (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) : Set.MapsTo (convexApproxSample x0 z r ε) U U

theorem HCPolySupport.norm_convexApproxSample_sub {d : ℕ} (x0 z : Vec d) (r ε : ℝ) (x : Vec d) : ‖convexApproxSample x0 z r ε x - x‖ = |ε| * ‖x0 - r • z - x‖

theorem HCPolySupport.norm_sub_convexApproxSample {d : ℕ} (x0 z : Vec d) (r ε : ℝ) (x : Vec d) : ‖x - convexApproxSample x0 z r ε x‖ = |ε| * ‖x0 - r • z - x‖

theorem HCPolySupport.norm_convexApproxSample_sub_le {d : ℕ} (x0 z : Vec d) (r ε : ℝ) (x : Vec d) (hε0 : 0 ≤ ε) : ‖convexApproxSample x0 z r ε x - x‖ ≤ ε * ‖x0 - r • z - x‖

theorem HCPolySupport.norm_sub_convexApproxSample_le {d : ℕ} (x0 z : Vec d) (r ε : ℝ) (x : Vec d) (hε0 : 0 ≤ ε) : ‖x - convexApproxSample x0 z r ε x‖ ≤ ε * ‖x0 - r • z - x‖

theorem HCPolySupport.norm_convexApproxSample_sub_le_two_mul_choose {d : ℕ} {U : Set (Vec d)} (hU : IsBoundedDomain U) {x x0 z : Vec d} {r ε : ℝ} (hx : x ∈ U) (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 ≤ r) (hz : ‖z‖ ≤ 1) (hε0 : 0 ≤ ε) : ‖convexApproxSample x0 z r ε x - x‖ ≤ ε * (2 * Classical.choose hU)

theorem HCPolySupport.norm_sub_convexApproxSample_le_two_mul_choose {d : ℕ} {U : Set (Vec d)} (hU : IsBoundedDomain U) {x x0 z : Vec d} {r ε : ℝ} (hx : x ∈ U) (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 ≤ r) (hz : ‖z‖ ≤ 1) (hε0 : 0 ≤ ε) : ‖x - convexApproxSample x0 z r ε x‖ ≤ ε * (2 * Classical.choose hU)

theorem HCPolySupport.norm_convexApproxSample_sub_le_two_mul_choose_of_isOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {x x0 z : Vec d} {r ε : ℝ} (hx : x ∈ U) (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 ≤ r) (hz : ‖z‖ ≤ 1) (hε0 : 0 ≤ ε) : ‖convexApproxSample x0 z r ε x - x‖ ≤ ε * (2 * Classical.choose ⋯)

theorem HCPolySupport.norm_sub_convexApproxSample_le_two_mul_choose_of_isOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {x x0 z : Vec d} {r ε : ℝ} (hx : x ∈ U) (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 ≤ r) (hz : ‖z‖ ≤ 1) (hε0 : 0 ≤ ε) : ‖x - convexApproxSample x0 z r ε x‖ ≤ ε * (2 * Classical.choose ⋯)