Coarse-graining support: Support.Sobolev.Foundations.Cutoff.Euclidean

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

Explicit Euclidean geometry on Vec d

The project uses Vec d = Fin d → ℝ, whose default metric is the product/sup metric. This file defines the Euclidean squared distance and Euclidean balls explicitly on the same underlying type, so later cutoff statements can be about round Euclidean balls without changing ambient type to EuclideanSpace.

def HCPolySupport.euclideanSqDist {d : ℕ} (x y : Vec d) : ℝ

Euclidean squared distance on Vec d, independent of the default Vec d metric.

Equations

• HCPolySupport.euclideanSqDist x y = HCPolySupport.vecNormSq (x - y)

theorem HCPolySupport.euclideanSqDist_eq_euclideanDist_sq {d : ℕ} (x y : Vec d) : euclideanSqDist x y = euclideanDist x y ^ 2

The legacy squared-distance expression is the square of the explicit Euclidean distance.

def HCPolySupport.euclideanBall {d : ℕ} (x₀ : Vec d) (R : ℝ) : Set (Vec d)

Explicit Euclidean open ball on Vec d.

Equations

• HCPolySupport.euclideanBall x₀ R = {x : HCPolySupport.Vec d | HCPolySupport.euclideanSqDist x x₀ < R ^ 2}

def HCPolySupport.euclideanClosedBall {d : ℕ} (x₀ : Vec d) (R : ℝ) : Set (Vec d)

Explicit Euclidean closed ball on Vec d.

Equations

• HCPolySupport.euclideanClosedBall x₀ R = {x : HCPolySupport.Vec d | HCPolySupport.euclideanSqDist x x₀ ≤ R ^ 2}

def HCPolySupport.euclideanSphere {d : ℕ} (x₀ : Vec d) (R : ℝ) : Set (Vec d)

Explicit Euclidean sphere on Vec d.

Equations

• HCPolySupport.euclideanSphere x₀ R = {x : HCPolySupport.Vec d | HCPolySupport.euclideanSqDist x x₀ = R ^ 2}

@[simp]

theorem HCPolySupport.euclideanSqDist_self {d : ℕ} (x : Vec d) : euclideanSqDist x x = 0

theorem HCPolySupport.euclideanSqDist_zero_zero {d : ℕ} : euclideanSqDist 0 0 = 0

theorem HCPolySupport.euclideanSqDist_add_right {d : ℕ} (x y z : Vec d) : euclideanSqDist (x + z) (y + z) = euclideanSqDist x y

theorem HCPolySupport.euclideanSqDist_smul_smul {d : ℕ} (r : ℝ) (x y : Vec d) : euclideanSqDist (r • x) (r • y) = r ^ 2 * euclideanSqDist x y

theorem HCPolySupport.euclideanSqDist_smul_zero {d : ℕ} (r : ℝ) (x : Vec d) : euclideanSqDist (r • x) 0 = r ^ 2 * euclideanSqDist x 0

theorem HCPolySupport.euclideanSqDist_affine_center {d : ℕ} (x₀ y : Vec d) (r : ℝ) : euclideanSqDist (r • y + x₀) x₀ = r ^ 2 * euclideanSqDist y 0

theorem HCPolySupport.euclideanSqDist_sub_left_self {d : ℕ} (x z : Vec d) : euclideanSqDist (x - z) x = euclideanSqDist z 0

Translating a point by -z from the center has the same explicit Euclidean squared distance as z from the origin.

theorem HCPolySupport.sub_mem_euclideanBall_center_of_mem_zero {d : ℕ} {x z : Vec d} {R : ℝ} (hz : z ∈ euclideanBall 0 R) : x - z ∈ euclideanBall x R

If z lies in the explicit Euclidean ball about the origin, then x - z lies in the corresponding explicit Euclidean ball about x.

theorem HCPolySupport.affine_mem_euclideanBall_iff_of_pos {d : ℕ} (x₀ y : Vec d) {r : ℝ} (hr : 0 < r) : r • y + x₀ ∈ euclideanBall x₀ r ↔ y ∈ euclideanBall 0 1

theorem HCPolySupport.affine_mem_euclideanClosedBall_iff_of_pos {d : ℕ} (x₀ y : Vec d) {r : ℝ} (hr : 0 < r) : r • y + x₀ ∈ euclideanClosedBall x₀ r ↔ y ∈ euclideanClosedBall 0 1

theorem HCPolySupport.euclideanBall_eq_translateSet_smul_unit_of_pos {d : ℕ} (x₀ : Vec d) {r : ℝ} (hr : 0 < r) : euclideanBall x₀ r = translateSet x₀ (r • euclideanBall 0 1)

theorem HCPolySupport.euclideanClosedBall_eq_translateSet_smul_unit_of_pos {d : ℕ} (x₀ : Vec d) {r : ℝ} (hr : 0 < r) : euclideanClosedBall x₀ r = translateSet x₀ (r • euclideanClosedBall 0 1)

theorem HCPolySupport.euclideanSqDist_nonneg {d : ℕ} (x y : Vec d) : 0 ≤ euclideanSqDist x y

theorem HCPolySupport.vecNormSq_weighted_add_le {d : ℕ} {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (v w : Vec d) : vecNormSq (a • v + b • w) ≤ a * vecNormSq v + b * vecNormSq w

Convexity inequality for the coordinate Euclidean squared norm.

theorem HCPolySupport.euclideanSqDist_weighted_add_le {d : ℕ} {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (x y x₀ : Vec d) : euclideanSqDist (a • x + b • y) x₀ ≤ a * euclideanSqDist x x₀ + b * euclideanSqDist y x₀

Convexity inequality for the coordinate Euclidean squared distance.

theorem HCPolySupport.convex_euclideanClosedBall {d : ℕ} (x₀ : Vec d) (R : ℝ) : Convex ℝ (euclideanClosedBall x₀ R)

Explicit Euclidean closed balls are convex subsets of the project carrier.

theorem HCPolySupport.convex_euclideanBall {d : ℕ} (x₀ : Vec d) (R : ℝ) : Convex ℝ (euclideanBall x₀ R)

Explicit Euclidean open balls are convex subsets of the project carrier.

theorem HCPolySupport.sq_coord_sub_le_euclideanSqDist {d : ℕ} (x y : Vec d) (i : Fin d) : (x i - y i) ^ 2 ≤ euclideanSqDist x y

theorem HCPolySupport.contDiff_vecNormSq {d : ℕ} : ContDiff ℝ ↑⊤ fun (x : Vec d) => vecNormSq x

theorem HCPolySupport.contDiff_euclideanSqDist_left {d : ℕ} (x₀ : Vec d) : ContDiff ℝ ↑⊤ fun (x : Vec d) => euclideanSqDist x x₀

theorem HCPolySupport.continuous_euclideanSqDist_left {d : ℕ} (x₀ : Vec d) : Continuous fun (x : Vec d) => euclideanSqDist x x₀

theorem HCPolySupport.isOpen_euclideanBall {d : ℕ} (x₀ : Vec d) (R : ℝ) : IsOpen (euclideanBall x₀ R)

theorem HCPolySupport.isClosed_euclideanClosedBall {d : ℕ} (x₀ : Vec d) (R : ℝ) : IsClosed (euclideanClosedBall x₀ R)

theorem HCPolySupport.isClosed_euclideanSphere {d : ℕ} (x₀ : Vec d) (R : ℝ) : IsClosed (euclideanSphere x₀ R)

Explicit Euclidean spheres are closed in the default product topology.

theorem HCPolySupport.euclideanSphere_subset_euclideanClosedBall {d : ℕ} (x₀ : Vec d) (R : ℝ) : euclideanSphere x₀ R ⊆ euclideanClosedBall x₀ R

The explicit sphere is contained in the corresponding explicit closed ball.

theorem HCPolySupport.euclideanClosedBall_diff_euclideanBall_eq_euclideanSphere {d : ℕ} (x₀ : Vec d) (R : ℝ) : euclideanClosedBall x₀ R \ euclideanBall x₀ R = euclideanSphere x₀ R

The closed Euclidean ball is the disjoint union of its open ball and sphere, stated as a set-difference identity.

theorem HCPolySupport.euclideanClosedBall_subset_euclideanBall_union_euclideanSphere {d : ℕ} (x₀ : Vec d) (R : ℝ) : euclideanClosedBall x₀ R ⊆ euclideanBall x₀ R ∪ euclideanSphere x₀ R

The closed Euclidean ball is covered by its open ball and sphere.

theorem HCPolySupport.euclideanSphere_subset_frontier_euclideanClosedBall_of_pos {d : ℕ} (x₀ : Vec d) {R : ℝ} (hR : 0 < R) : euclideanSphere x₀ R ⊆ frontier (euclideanClosedBall x₀ R)

A positive-radius explicit Euclidean sphere lies in the frontier of the corresponding explicit closed ball.

theorem HCPolySupport.center_mem_euclideanBall {d : ℕ} (x₀ : Vec d) {R : ℝ} (hR : 0 < R) : x₀ ∈ euclideanBall x₀ R

theorem HCPolySupport.euclideanBall_nonempty {d : ℕ} (x₀ : Vec d) {R : ℝ} (hR : 0 < R) : (euclideanBall x₀ R).Nonempty

theorem HCPolySupport.euclideanBall_subset_euclideanClosedBall_abs {d : ℕ} (x₀ : Vec d) (R : ℝ) : euclideanBall x₀ R ⊆ euclideanClosedBall x₀ |R|

theorem HCPolySupport.euclideanClosedBall_subset_metricClosedBall {d : ℕ} {x₀ : Vec d} {R : ℝ} (hR : 0 ≤ R) : euclideanClosedBall x₀ R ⊆ Metric.closedBall x₀ R

theorem HCPolySupport.euclideanBall_subset_metricBall {d : ℕ} {x₀ : Vec d} {R : ℝ} (hR : 0 < R) : euclideanBall x₀ R ⊆ Metric.ball x₀ R

An explicit coordinate-Euclidean open ball is contained in the default product-metric open ball of the same radius.

theorem HCPolySupport.metricClosedBall_div_two_natCast_succ_subset_euclideanBall {d : ℕ} {x₀ : Vec d} {R : ℝ} (hR : 0 < R) : Metric.closedBall x₀ (R / (2 * (↑d + 1))) ⊆ euclideanBall x₀ R

A positive explicit Euclidean ball contains a small default-metric closed ball around its center. The conservative radius avoids needing a sharp comparison between the product metric and the coordinate Euclidean norm.

theorem HCPolySupport.isCompact_euclideanClosedBall {d : ℕ} (x₀ : Vec d) {R : ℝ} (hR : 0 ≤ R) : IsCompact (euclideanClosedBall x₀ R)

theorem HCPolySupport.euclideanClosedBall_subset_euclideanBall {d : ℕ} {x₀ : Vec d} {s R : ℝ} (hs : 0 ≤ s) (hsR : s < R) : euclideanClosedBall x₀ s ⊆ euclideanBall x₀ R

theorem HCPolySupport.euclideanBall_subset_euclideanBall {d : ℕ} {x₀ : Vec d} {s R : ℝ} (hs : 0 ≤ s) (hsR : s < R) : euclideanBall x₀ s ⊆ euclideanBall x₀ R