Documentation

LeanPool.HighContrastHomogenization.Support.Ambient.Euclidean

Coarse-graining support: Support.Ambient.Euclidean #

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

Explicit Euclidean magnitude on Vec d #

The project's algebraic carrier Vec d = Fin d → ℝ deliberately retains its default product/sup norm. This file supplies the Euclidean magnitude and distance as explicit real-valued functions on that same carrier, without introducing a competing norm or metric instance.

source
noncomputable def HCPolySupport.euclideanNorm {d : ℕ} (x : Vec d) :
ℝ

The Euclidean magnitude of a project vector.

Equations
Instances For
    source
    noncomputable def HCPolySupport.euclideanDist {d : ℕ} (x y : Vec d) :
    ℝ

    The Euclidean distance between two project vectors.

    Equations
    Instances For
      source
      theorem HCPolySupport.euclideanNorm_nonneg {d : ℕ} (x : Vec d) :
      0 ≤ euclideanNorm x
      source
      @[simp]
      theorem HCPolySupport.euclideanNorm_sq {d : ℕ} (x : Vec d) :
      euclideanNorm x ^ 2 = vecNormSq x
      source
      @[simp]
      theorem HCPolySupport.euclideanNorm_eq_zero_iff {d : ℕ} {x : Vec d} :
      euclideanNorm x = 0 ↔ x = 0
      source
      @[simp]
      theorem HCPolySupport.euclideanNorm_zero {d : ℕ} :
      euclideanNorm 0 = 0
      source
      @[simp]
      theorem HCPolySupport.euclideanNorm_neg {d : ℕ} (x : Vec d) :
      euclideanNorm (-x) = euclideanNorm x
      source
      @[simp]
      theorem HCPolySupport.euclideanNorm_smul {d : ℕ} (c : ℝ) (x : Vec d) :
      euclideanNorm (c • x) = |c| * euclideanNorm x
      source
      theorem HCPolySupport.euclideanNorm_eq_norm_ofVec {d : ℕ} (x : Vec d) :
      euclideanNorm x = ‖HilbertVec.ofVec x‖

      The explicit Euclidean magnitude agrees with the norm on the separate Euclidean Hilbert realization of the same vector.

      source
      theorem HCPolySupport.euclideanDist_nonneg {d : ℕ} (x y : Vec d) :
      0 ≤ euclideanDist x y
      source
      @[simp]
      theorem HCPolySupport.euclideanDist_self {d : ℕ} (x : Vec d) :
      euclideanDist x x = 0
      source
      @[simp]
      theorem HCPolySupport.euclideanDist_eq_zero_iff {d : ℕ} {x y : Vec d} :
      euclideanDist x y = 0 ↔ x = y
      source
      theorem HCPolySupport.euclideanDist_comm {d : ℕ} (x y : Vec d) :
      euclideanDist x y = euclideanDist y x
      source
      @[simp]
      theorem HCPolySupport.euclideanDist_sq {d : ℕ} (x y : Vec d) :
      euclideanDist x y ^ 2 = vecNormSq (x - y)

      Squaring the explicit Euclidean distance recovers the coordinate square sum of the displacement.

      source
      theorem HCPolySupport.euclideanDist_smul {d : ℕ} (c : ℝ) (x y : Vec d) :
      euclideanDist (c • x) (c • y) = |c| * euclideanDist x y

      Scalar dilations scale explicit Euclidean distance by the scalar's absolute value.

      source
      theorem HCPolySupport.euclideanDist_add_right {d : ℕ} (x y z : Vec d) :
      euclideanDist (x + z) (y + z) = euclideanDist x y

      Translating both arguments by the same vector leaves explicit Euclidean distance unchanged.

      source
      theorem HCPolySupport.euclideanDist_eq_norm_sub_ofVec {d : ℕ} (x y : Vec d) :
      euclideanDist x y = ‖HilbertVec.ofVec x - HilbertVec.ofVec y‖

      The explicit Euclidean distance agrees with the Hilbert distance on the separate Euclidean realization of project vectors.

      source
      @[simp]
      theorem HCPolySupport.euclideanDist_zero_left {d : ℕ} (x : Vec d) :
      euclideanDist 0 x = euclideanNorm x
      source
      @[simp]
      theorem HCPolySupport.euclideanDist_zero_right {d : ℕ} (x : Vec d) :
      euclideanDist x 0 = euclideanNorm x