High-contrast homogenization: Analytic.EuclideanAmbient

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

The Euclidean structure of the ambient space

The ambient norm of Vec d = Fin d → ℝ is the supremum norm, so every Euclidean quantity entering the volume-normalized spaces of s.introduction is carried by vecDot and vecNormSq, and the bilinear identities behind it have to be supplied by hand: the expansion of vecNormSq on sums and differences, Cauchy–Schwarz, and the triangle inequality, direct and reverse, for Real.sqrt ∘ vecNormSq.

The second half describes the Euclidean ball euclideanBallAt c r: it is open, it contains its centre, its frontier lies on the Euclidean sphere, and it is compared in both directions with the ambient Metric.ball, which is the ball of the supremum norm — an open cube — and not a Euclidean ball. The outward comparison costs a factor √d.

A last section records the two facts about matVecMul needed when a linear image of a domain is taken: it is continuous, and the identity matrix acts trivially.

Elementary real scaffolding

theorem HCPolySupport.HighContrast.lt_of_sq_lt_sq' {a b : ℝ} (hb : 0 ≤ b) (h : a ^ 2 < b ^ 2) : a < b

A real number is dominated by a nonnegative real whose square dominates its square.

Euclidean bilinear algebra on Vec d

The ambient norm of Vec d is the supremum norm, so every Euclidean quantity is written through vecDot/vecNormSq and the bilinear identities have to be supplied by hand.

theorem HCPolySupport.HighContrast.vecDot_sub_left {d : ℕ} (x y z : Vec d) : vecDot (x - y) z = vecDot x z - vecDot y z

theorem HCPolySupport.HighContrast.vecDot_sub_right {d : ℕ} (x y z : Vec d) : vecDot x (y - z) = vecDot x y - vecDot x z

theorem HCPolySupport.HighContrast.vecNormSq_add {d : ℕ} (x y : Vec d) : vecNormSq (x + y) = vecNormSq x + 2 * vecDot x y + vecNormSq y

theorem HCPolySupport.HighContrast.vecNormSq_sub {d : ℕ} (x y : Vec d) : vecNormSq (x - y) = vecNormSq x - 2 * vecDot x y + vecNormSq y

theorem HCPolySupport.HighContrast.vecNormSq_neg {d : ℕ} (x : Vec d) : vecNormSq (-x) = vecNormSq x

theorem HCPolySupport.HighContrast.vecNormSq_eq_sum_sq {d : ℕ} (x : Vec d) : vecNormSq x = ∑ i : Fin d, x i ^ 2

theorem HCPolySupport.HighContrast.vecDot_le_sqrt_mul_sqrt {d : ℕ} (x y : Vec d) : vecDot x y ≤ √(vecNormSq x) * √(vecNormSq y)

Cauchy–Schwarz in the form used for the Euclidean triangle inequality.

theorem HCPolySupport.HighContrast.sqrt_vecNormSq_add_le {d : ℕ} (x y : Vec d) : √(vecNormSq (x + y)) ≤ √(vecNormSq x) + √(vecNormSq y)

The Euclidean triangle inequality for Real.sqrt ∘ vecNormSq.

theorem HCPolySupport.HighContrast.abs_sqrt_vecNormSq_sub_le {d : ℕ} (x y : Vec d) : |√(vecNormSq x) - √(vecNormSq y)| ≤ √(vecNormSq (x - y))

The reverse Euclidean triangle inequality for Real.sqrt ∘ vecNormSq.

The Euclidean ball euclideanBallAt

theorem HCPolySupport.HighContrast.mem_euclideanBallAt_iff {d : ℕ} {c : Vec d} {r : ℝ} (x : Vec d) : x ∈ euclideanBallAt c r ↔ vecNormSq (x - c) < r ^ 2

theorem HCPolySupport.HighContrast.mem_euclideanBall_iff {d : ℕ} {R : ℝ} (x : Vec d) : x ∈ euclideanBall d R ↔ vecNormSq x < R ^ 2

theorem HCPolySupport.HighContrast.center_mem_euclideanBallAt {d : ℕ} (c : Vec d) {r : ℝ} (hr : 0 < r) : c ∈ euclideanBallAt c r

theorem HCPolySupport.HighContrast.continuous_vecNormSq {d : ℕ} : Continuous fun (x : Vec d) => vecNormSq x

theorem HCPolySupport.HighContrast.continuous_vecNormSq_sub {d : ℕ} (c : Vec d) : Continuous fun (x : Vec d) => vecNormSq (x - c)

theorem HCPolySupport.HighContrast.isOpen_euclideanBallAt {d : ℕ} (c : Vec d) (r : ℝ) : IsOpen (euclideanBallAt c r)

theorem HCPolySupport.HighContrast.isOpen_euclideanBall (d : ℕ) (R : ℝ) : IsOpen (euclideanBall d R)

theorem HCPolySupport.HighContrast.vecNormSq_of_mem_frontier_euclideanBall {d : ℕ} {R : ℝ} {c : Vec d} (hc : c ∈ frontier (euclideanBall d R)) : vecNormSq c = R ^ 2

The easy half of the boundary description of the Euclidean ball: every frontier point lies on the Euclidean sphere. (The reverse inclusion is not needed anywhere.)

Comparison of the Euclidean ball with the ambient (sup-norm) ball

Metric.ball on Vec d = Fin d → ℝ is the ball of the SUP norm — an open cube — not the Euclidean ball. These are the two comparison inclusions.

theorem HCPolySupport.HighContrast.euclideanBallAt_subset_metricBall {d : ℕ} (c : Vec d) {r : ℝ} (hr : 0 < r) : euclideanBallAt c r ⊆ Metric.ball c r

theorem HCPolySupport.HighContrast.vecNormSq_sub_le_of_mem_metricBall {d : ℕ} {c x : Vec d} {r : ℝ} (hx : x ∈ Metric.ball c r) : vecNormSq (x - c) ≤ ↑d * r ^ 2

theorem HCPolySupport.HighContrast.vecNormSq_sub_lt_of_mem_metricBall {d : ℕ} {c x : Vec d} {r : ℝ} (hd : 0 < d) (hx : x ∈ Metric.ball c r) : vecNormSq (x - c) < ↑d * r ^ 2

Linear maps on Vec d

theorem HCPolySupport.HighContrast.matVecMul_one {d : ℕ} (x : Vec d) : matVecMul 1 x = x

theorem HCPolySupport.HighContrast.continuous_matVecMul {d : ℕ} (M : Mat d) : Continuous fun (x : Vec d) => matVecMul M x