Module docstring
{"# Product of pseudometric spaces
This file constructs the infinity distance on finite products of pseudometric spaces. "}
pseudoMetricSpacePi
instance
: PseudoMetricSpace (∀ b, π b)
Full source
/-- A finite product of pseudometric spaces is a pseudometric space, with the sup distance. -/
instance pseudoMetricSpacePi : PseudoMetricSpace (∀ b, π b) := by
/- we construct the instance from the pseudoemetric space instance to avoid checking again that
the uniformity is the same as the product uniformity, but we register nevertheless a nice
formula for the distance -/
let i := PseudoEMetricSpace.toPseudoMetricSpaceOfDist
(fun f g : ∀ b, π b => ((sup univ fun b => nndist (f b) (g b) : ℝ≥0) : ℝ))
(fun f g => ((Finset.sup_lt_iff bot_lt_top).2 fun b _ => edist_lt_top _ _).ne)
(fun f g => by
simp only [edist_pi_def, edist_nndist, ← ENNReal.coe_finset_sup, ENNReal.coe_toReal])
refine i.replaceBornology fun s => ?_
simp only [← isBounded_def, isBounded_iff_eventually, ← forall_isBounded_image_eval_iff,
forall_mem_image, ← Filter.eventually_all, Function.eval_apply, @dist_nndist (π _)]
refine eventually_congr ((eventually_ge_atTop 0).mono fun C hC ↦ ?_)
lift C to ℝ≥0 using hC
refine ⟨fun H x hx y hy ↦ NNReal.coe_le_coe.2 <| Finset.sup_le fun b _ ↦ H b hx hy,
fun H b x hx y hy ↦ NNReal.coe_le_coe.2 ?_⟩
simpa only using Finset.sup_le_iff.1 (NNReal.coe_le_coe.1 <| H hx hy) b (Finset.mem_univ b)Informal description
For any family of pseudometric spaces $\{\pi_b\}_{b \in B}$, the product space $\prod_{b \in B} \pi_b$ is a pseudometric space with the supremum distance: for any $f, g \in \prod_{b \in B} \pi_b$, the distance is given by $\text{dist}(f, g) = \sup_{b \in B} \text{dist}(f(b), g(b))$.
nndist_pi_def
theorem
(f g : ∀ b, π b) : nndist f g = sup univ fun b => nndist (f b) (g b)
Informal description
For any two functions $f, g$ in the product space $\prod_{b \in B} \pi_b$ of pseudometric spaces, the non-negative distance between $f$ and $g$ is given by the supremum of the non-negative distances between their components:
\[ \text{nndist}(f, g) = \sup_{b \in B} \text{nndist}(f(b), g(b)). \]
dist_pi_def
theorem
(f g : ∀ b, π b) : dist f g = (sup univ fun b => nndist (f b) (g b) : ℝ≥0)
Informal description
For any two functions $f, g$ in the product space $\prod_{b \in B} \pi_b$ of pseudometric spaces, the distance between them is given by the supremum of the non-negative distances between their components:
\[
\text{dist}(f, g) = \sup_{b \in B} \text{nndist}(f(b), g(b)).
\]
nndist_pi_le_iff
theorem
{f g : ∀ b, π b} {r : ℝ≥0} : nndist f g ≤ r ↔ ∀ b, nndist (f b) (g b) ≤ r
Full source
lemma nndist_pi_le_iff {f g : ∀ b, π b} {r : ℝ≥0} :
nndistnndist f g ≤ r ↔ ∀ b, nndist (f b) (g b) ≤ r := by simp [nndist_pi_def]Informal description
For any two functions $f, g$ in the product space $\prod_{b \in B} \pi_b$ of pseudometric spaces and any non-negative real number $r$, the supremum distance between $f$ and $g$ is less than or equal to $r$ if and only if for every index $b \in B$, the distance between $f(b)$ and $g(b)$ is less than or equal to $r$.
nndist_pi_lt_iff
theorem
{f g : ∀ b, π b} {r : ℝ≥0} (hr : 0 < r) : nndist f g < r ↔ ∀ b, nndist (f b) (g b) < r
Full source
lemma nndist_pi_lt_iff {f g : ∀ b, π b} {r : ℝ≥0} (hr : 0 < r) :
nndistnndist f g < r ↔ ∀ b, nndist (f b) (g b) < r := by
rw [← bot_eq_zero'] at hr
simp [nndist_pi_def, Finset.sup_lt_iff hr]Informal description
For any two functions $f, g$ in the product space $\prod_{b \in B} \pi_b$ of pseudometric spaces and any positive real number $r > 0$, the non-negative distance between $f$ and $g$ is less than $r$ if and only if for every index $b \in B$, the non-negative distance between $f(b)$ and $g(b)$ is less than $r$. In other words:
\[ \text{nndist}(f, g) < r \leftrightarrow \forall b \in B, \text{nndist}(f(b), g(b)) < r. \]
nndist_pi_eq_iff
theorem
{f g : ∀ b, π b} {r : ℝ≥0} (hr : 0 < r) : nndist f g = r ↔ (∃ i, nndist (f i) (g i) = r) ∧ ∀ b, nndist (f b) (g b) ≤ r
Full source
lemma nndist_pi_eq_iff {f g : ∀ b, π b} {r : ℝ≥0} (hr : 0 < r) :
nndistnndist f g = r ↔ (∃ i, nndist (f i) (g i) = r) ∧ ∀ b, nndist (f b) (g b) ≤ r := by
rw [eq_iff_le_not_lt, nndist_pi_lt_iff hr, nndist_pi_le_iff, not_forall, and_comm]
simp_rw [not_lt, and_congr_left_iff, le_antisymm_iff]
intro h
refine exists_congr fun b => ?_
apply (and_iff_right <| h _).symmInformal description
For any two functions $f, g$ in the product space $\prod_{b \in B} \pi_b$ of pseudometric spaces and any positive real number $r > 0$, the non-negative distance between $f$ and $g$ equals $r$ if and only if there exists an index $i \in B$ such that the distance between $f(i)$ and $g(i)$ equals $r$, and for every index $b \in B$, the distance between $f(b)$ and $g(b)$ is less than or equal to $r$. In other words:
\[ \text{nndist}(f, g) = r \leftrightarrow \left(\exists i \in B, \text{nndist}(f(i), g(i)) = r\right) \land \left(\forall b \in B, \text{nndist}(f(b), g(b)) \leq r\right). \]
dist_pi_lt_iff
theorem
{f g : ∀ b, π b} {r : ℝ} (hr : 0 < r) : dist f g < r ↔ ∀ b, dist (f b) (g b) < r
Full source
lemma dist_pi_lt_iff {f g : ∀ b, π b} {r : ℝ} (hr : 0 < r) :
distdist f g < r ↔ ∀ b, dist (f b) (g b) < r := by
lift r to ℝ≥0 using hr.le
exact nndist_pi_lt_iff hrInformal description
For any two functions $f, g$ in the product space $\prod_{b \in B} \pi_b$ of pseudometric spaces and any positive real number $r > 0$, the distance between $f$ and $g$ is less than $r$ if and only if for every index $b \in B$, the distance between $f(b)$ and $g(b)$ is less than $r$. In other words:
\[ \text{dist}(f, g) < r \leftrightarrow \forall b \in B, \text{dist}(f(b), g(b)) < r. \]
dist_pi_le_iff
theorem
{f g : ∀ b, π b} {r : ℝ} (hr : 0 ≤ r) : dist f g ≤ r ↔ ∀ b, dist (f b) (g b) ≤ r
Full source
lemma dist_pi_le_iff {f g : ∀ b, π b} {r : ℝ} (hr : 0 ≤ r) :
distdist f g ≤ r ↔ ∀ b, dist (f b) (g b) ≤ r := by
lift r to ℝ≥0 using hr
exact nndist_pi_le_iffInformal description
For any two functions $f, g$ in the product space $\prod_{b \in B} \pi_b$ of pseudometric spaces and any non-negative real number $r \geq 0$, the supremum distance between $f$ and $g$ is less than or equal to $r$ if and only if for every index $b \in B$, the distance between $f(b)$ and $g(b)$ is less than or equal to $r$.
dist_pi_eq_iff
theorem
{f g : ∀ b, π b} {r : ℝ} (hr : 0 < r) : dist f g = r ↔ (∃ i, dist (f i) (g i) = r) ∧ ∀ b, dist (f b) (g b) ≤ r
Full source
lemma dist_pi_eq_iff {f g : ∀ b, π b} {r : ℝ} (hr : 0 < r) :
distdist f g = r ↔ (∃ i, dist (f i) (g i) = r) ∧ ∀ b, dist (f b) (g b) ≤ r := by
lift r to ℝ≥0 using hr.le
simp_rw [← coe_nndist, NNReal.coe_inj, nndist_pi_eq_iff hr, NNReal.coe_le_coe]Informal description
For any two functions $f, g$ in the product space $\prod_{b \in B} \pi_b$ of pseudometric spaces and any positive real number $r > 0$, the distance between $f$ and $g$ equals $r$ if and only if there exists an index $i \in B$ such that the distance between $f(i)$ and $g(i)$ equals $r$, and for every index $b \in B$, the distance between $f(b)$ and $g(b)$ is less than or equal to $r$. In other words:
\[ \text{dist}(f, g) = r \leftrightarrow \left(\exists i \in B, \text{dist}(f(i), g(i)) = r\right) \land \left(\forall b \in B, \text{dist}(f(b), g(b)) \leq r\right). \]
dist_pi_le_iff'
theorem
[Nonempty β] {f g : ∀ b, π b} {r : ℝ} : dist f g ≤ r ↔ ∀ b, dist (f b) (g b) ≤ r
Full source
lemma dist_pi_le_iff' [Nonempty β] {f g : ∀ b, π b} {r : ℝ} :
distdist f g ≤ r ↔ ∀ b, dist (f b) (g b) ≤ r := by
by_cases hr : 0 ≤ r
· exact dist_pi_le_iff hr
· exact iff_of_false (fun h => hr <| dist_nonneg.trans h) fun h =>
hr <| dist_nonneg.trans <| h <| Classical.arbitrary _Informal description
For a nonempty index set $\beta$ and any two functions $f, g \in \prod_{b \in \beta} \pi_b$ in a product of pseudometric spaces, the supremum distance $\text{dist}(f, g) \leq r$ holds if and only if for every $b \in \beta$, the distance $\text{dist}(f(b), g(b)) \leq r$.
dist_pi_const_le
theorem
(a b : α) : (dist (fun _ : β => a) fun _ => b) ≤ dist a b
Full source
lemma dist_pi_const_le (a b : α) : (dist (fun _ : β => a) fun _ => b) ≤ dist a b :=
(dist_pi_le_iff dist_nonneg).2 fun _ => le_rflInformal description
For any two points $a$ and $b$ in a pseudometric space $\alpha$, the distance between the constant functions $\lambda x : \beta \mapsto a$ and $\lambda x : \beta \mapsto b$ in the product space $\prod_{b \in \beta} \alpha$ is less than or equal to the distance between $a$ and $b$ in $\alpha$, i.e.,
\[ \text{dist}\left( (\lambda x : \beta \mapsto a), (\lambda x : \beta \mapsto b) \right) \leq \text{dist}(a, b). \]
nndist_pi_const_le
theorem
(a b : α) : (nndist (fun _ : β => a) fun _ => b) ≤ nndist a b
Full source
lemma nndist_pi_const_le (a b : α) : (nndist (fun _ : β => a) fun _ => b) ≤ nndist a b :=
nndist_pi_le_iff.2 fun _ => le_rflInformal description
For any two points $a$ and $b$ in a pseudometric space $\alpha$, the non-negative distance between the constant functions $\lambda \_ : \beta \mapsto a$ and $\lambda \_ : \beta \mapsto b$ in the product space $\prod_{b \in \beta} \alpha$ is less than or equal to the non-negative distance between $a$ and $b$ in $\alpha$, i.e.,
\[ \text{nndist}\left( (\lambda \_ : \beta \mapsto a), (\lambda \_ : \beta \mapsto b) \right) \leq \text{nndist}(a, b). \]
dist_pi_const
theorem
[Nonempty β] (a b : α) : (dist (fun _ : β => a) fun _ => b) = dist a b
Full source
@[simp]
lemma dist_pi_const [Nonempty β] (a b : α) : (dist (fun _ : β => a) fun _ => b) = dist a b := by
simpa only [dist_edist] using congr_arg ENNReal.toReal (edist_pi_const a b)Informal description
For a nonempty index set $\beta$ and any two points $a$ and $b$ in a pseudometric space $\alpha$, the distance between the constant functions $\lambda \_ : \beta \mapsto a$ and $\lambda \_ : \beta \mapsto b$ in the product space $\prod_{b \in \beta} \alpha$ is equal to the distance between $a$ and $b$ in $\alpha$, i.e.,
\[ \text{dist}\left( (\lambda \_ : \beta \mapsto a), (\lambda \_ : \beta \mapsto b) \right) = \text{dist}(a, b). \]
nndist_pi_const
theorem
[Nonempty β] (a b : α) : (nndist (fun _ : β => a) fun _ => b) = nndist a b
Full source
@[simp]
lemma nndist_pi_const [Nonempty β] (a b : α) : (nndist (fun _ : β => a) fun _ => b) = nndist a b :=
NNReal.eq <| dist_pi_const a bInformal description
For a nonempty index set $\beta$ and any two points $a$ and $b$ in a pseudometric space $\alpha$, the non-negative distance between the constant functions $\lambda \_ : \beta \mapsto a$ and $\lambda \_ : \beta \mapsto b$ in the product space $\prod_{b \in \beta} \alpha$ is equal to the non-negative distance between $a$ and $b$ in $\alpha$, i.e.,
\[ \text{nndist}\left( (\lambda \_ : \beta \mapsto a), (\lambda \_ : \beta \mapsto b) \right) = \text{nndist}(a, b). \]
nndist_le_pi_nndist
theorem
(f g : ∀ b, π b) (b : β) : nndist (f b) (g b) ≤ nndist f g
Full source
lemma nndist_le_pi_nndist (f g : ∀ b, π b) (b : β) : nndist (f b) (g b) ≤ nndist f g := by
rw [← ENNReal.coe_le_coe, ← edist_nndist, ← edist_nndist]
exact edist_le_pi_edist f g bInformal description
For any two functions $f, g \in \prod_{b \in \beta} \pi_b$ in a product of pseudometric spaces and any index $b \in \beta$, the non-negative distance between $f(b)$ and $g(b)$ is less than or equal to the non-negative distance between $f$ and $g$ in the product space, i.e.,
\[ \text{nndist}(f(b), g(b)) \leq \text{nndist}(f, g). \]
dist_le_pi_dist
theorem
(f g : ∀ b, π b) (b : β) : dist (f b) (g b) ≤ dist f g
Full source
lemma dist_le_pi_dist (f g : ∀ b, π b) (b : β) : dist (f b) (g b) ≤ dist f g := by
simp only [dist_nndist, NNReal.coe_le_coe, nndist_le_pi_nndist f g b]Informal description
For any two functions $f, g \in \prod_{b \in \beta} \pi_b$ in a product of pseudometric spaces and any index $b \in \beta$, the distance between $f(b)$ and $g(b)$ is less than or equal to the distance between $f$ and $g$ in the product space, i.e.,
\[ \text{dist}(f(b), g(b)) \leq \text{dist}(f, g). \]
ball_pi
theorem
(x : ∀ b, π b) {r : ℝ} (hr : 0 < r) : ball x r = Set.pi univ fun b => ball (x b) r
Informal description
For any point $x$ in the product space $\prod_{b \in \beta} \pi_b$ of pseudometric spaces and any positive real number $r > 0$, the open ball $\text{ball}(x, r)$ is equal to the product of open balls $\prod_{b \in \beta} \text{ball}(x(b), r)$. In other words:
\[ \text{ball}(x, r) = \prod_{b \in \beta} \text{ball}(x(b), r). \]
ball_pi'
theorem
[Nonempty β] (x : ∀ b, π b) (r : ℝ) : ball x r = Set.pi univ fun b => ball (x b) r
Full source
/-- An open ball in a product space is a product of open balls. See also `ball_pi`
for a version assuming `0 < r` instead of `Nonempty β`. -/
lemma ball_pi' [Nonempty β] (x : ∀ b, π b) (r : ℝ) :
ball x r = Set.pi univ fun b => ball (x b) r :=
(lt_or_le 0 r).elim (ball_pi x) fun hr => by simp [ball_eq_empty.2 hr]Informal description
For a nonempty index set $\beta$, any point $x$ in the product space $\prod_{b \in \beta} \pi_b$ of pseudometric spaces, and any real number $r \in \mathbb{R}$, the open ball $\text{ball}(x, r)$ is equal to the product of open balls $\prod_{b \in \beta} \text{ball}(x(b), r)$. That is,
\[ \text{ball}(x, r) = \prod_{b \in \beta} \text{ball}(x(b), r). \]
closedBall_pi
theorem
(x : ∀ b, π b) {r : ℝ} (hr : 0 ≤ r) : closedBall x r = Set.pi univ fun b => closedBall (x b) r
Full source
/-- A closed ball in a product space is a product of closed balls. See also `closedBall_pi'`
for a version assuming `Nonempty β` instead of `0 ≤ r`. -/
lemma closedBall_pi (x : ∀ b, π b) {r : ℝ} (hr : 0 ≤ r) :
closedBall x r = Set.pi univ fun b => closedBall (x b) r := by
ext p
simp [dist_pi_le_iff hr]Informal description
For any point $x$ in the product space $\prod_{b \in \beta} \pi_b$ of pseudometric spaces and any non-negative real number $r \geq 0$, the closed ball $\overline{B}(x, r)$ centered at $x$ with radius $r$ is equal to the product of the closed balls $\overline{B}(x(b), r)$ for each component $b \in \beta$. That is,
\[ \overline{B}(x, r) = \prod_{b \in \beta} \overline{B}(x(b), r). \]
closedBall_pi'
theorem
[Nonempty β] (x : ∀ b, π b) (r : ℝ) : closedBall x r = Set.pi univ fun b => closedBall (x b) r
Full source
/-- A closed ball in a product space is a product of closed balls. See also `closedBall_pi`
for a version assuming `0 ≤ r` instead of `Nonempty β`. -/
lemma closedBall_pi' [Nonempty β] (x : ∀ b, π b) (r : ℝ) :
closedBall x r = Set.pi univ fun b => closedBall (x b) r :=
(le_or_lt 0 r).elim (closedBall_pi x) fun hr => by simp [closedBall_eq_empty.2 hr]Informal description
For any nonempty index set $\beta$, any point $x$ in the product space $\prod_{b \in \beta} \pi_b$ of pseudometric spaces, and any real number $r$, the closed ball $\overline{B}(x, r)$ centered at $x$ with radius $r$ is equal to the product of the closed balls $\overline{B}(x(b), r)$ for each component $b \in \beta$. That is,
\[ \overline{B}(x, r) = \prod_{b \in \beta} \overline{B}(x(b), r). \]
sphere_pi
theorem
(x : ∀ b, π b) {r : ℝ} (h : 0 < r ∨ Nonempty β) :
sphere x r = (⋃ i : β, Function.eval i ⁻¹' sphere (x i) r) ∩ closedBall x r
Full source
/-- A sphere in a product space is a union of spheres on each component restricted to the closed
ball. -/
lemma sphere_pi (x : ∀ b, π b) {r : ℝ} (h : 0 < r ∨ Nonempty β) :
sphere x r = (⋃ i : β, Function.eval i ⁻¹' sphere (x i) r) ∩ closedBall x r := by
obtain hr | rfl | hr := lt_trichotomy r 0
· simp [hr]
· rw [closedBall_eq_sphere_of_nonpos le_rfl, eq_comm, Set.inter_eq_right]
letI := h.resolve_left (lt_irrefl _)
inhabit β
refine subset_iUnion_of_subset default ?_
intro x hx
replace hx := hx.le
rw [dist_pi_le_iff le_rfl] at hx
exact le_antisymm (hx default) dist_nonneg
· ext
simp [dist_pi_eq_iff hr, dist_pi_le_iff hr.le]Informal description
For any point $x$ in the product space $\prod_{b \in \beta} \pi_b$ of pseudometric spaces and any positive real number $r > 0$ (or when the index set $\beta$ is nonempty), the sphere centered at $x$ with radius $r$ is equal to the intersection of the closed ball $\overline{B}(x, r)$ with the union of preimages of component spheres. Specifically:
\[
\text{sphere}(x, r) = \left(\bigcup_{i \in \beta} \text{eval}_i^{-1}(\text{sphere}(x(i), r))\right) \cap \overline{B}(x, r),
\]
where $\text{eval}_i$ denotes the evaluation map at index $i$.
Fin.nndist_insertNth_insertNth
theorem
{n : ℕ} {α : Fin (n + 1) → Type*} [∀ i, PseudoMetricSpace (α i)] (i : Fin (n + 1)) (x y : α i)
(f g : ∀ j, α (i.succAbove j)) : nndist (i.insertNth x f) (i.insertNth y g) = max (nndist x y) (nndist f g)
Full source
@[simp]
lemma Fin.nndist_insertNth_insertNth {n : ℕ} {α : Fin (n + 1) → Type*}
[∀ i, PseudoMetricSpace (α i)] (i : Fin (n + 1)) (x y : α i) (f g : ∀ j, α (i.succAbove j)) :
nndist (i.insertNth x f) (i.insertNth y g) = max (nndist x y) (nndist f g) :=
eq_of_forall_ge_iff fun c => by simp [nndist_pi_le_iff, i.forall_iff_succAbove]Informal description
For any natural number $n$, a family of pseudometric spaces $\{\alpha_i\}_{i \in \text{Fin}(n+1)}$, a pivot index $i \in \text{Fin}(n+1)$, elements $x, y \in \alpha_i$, and tuples $f, g \in \prod_{j \in \text{Fin}(n)} \alpha_{i.\text{succAbove}\,j}$, the non-negative distance between the inserted tuples $\text{insertNth}\,i\,x\,f$ and $\text{insertNth}\,i\,y\,g$ is equal to the maximum of the distances between $x$ and $y$ and between $f$ and $g$. That is,
\[
\text{nndist}(\text{insertNth}\,i\,x\,f, \text{insertNth}\,i\,y\,g) = \max(\text{nndist}(x, y), \text{nndist}(f, g)).
\]
Fin.dist_insertNth_insertNth
theorem
{n : ℕ} {α : Fin (n + 1) → Type*} [∀ i, PseudoMetricSpace (α i)] (i : Fin (n + 1)) (x y : α i)
(f g : ∀ j, α (i.succAbove j)) : dist (i.insertNth x f) (i.insertNth y g) = max (dist x y) (dist f g)
Full source
@[simp]
lemma Fin.dist_insertNth_insertNth {n : ℕ} {α : Fin (n + 1) → Type*}
[∀ i, PseudoMetricSpace (α i)] (i : Fin (n + 1)) (x y : α i) (f g : ∀ j, α (i.succAbove j)) :
dist (i.insertNth x f) (i.insertNth y g) = max (dist x y) (dist f g) := by
simp only [dist_nndist, Fin.nndist_insertNth_insertNth, NNReal.coe_max]Informal description
For any natural number $n$, a family of pseudometric spaces $\{\alpha_i\}_{i \in \text{Fin}(n+1)}$, a pivot index $i \in \text{Fin}(n+1)$, elements $x, y \in \alpha_i$, and tuples $f, g \in \prod_{j \in \text{Fin}(n)} \alpha_{i.\text{succAbove}\,j}$, the distance between the inserted tuples $\text{insertNth}\,i\,x\,f$ and $\text{insertNth}\,i\,y\,g$ is equal to the maximum of the distances between $x$ and $y$ and between $f$ and $g$. That is,
\[
\text{dist}(\text{insertNth}\,i\,x\,f, \text{insertNth}\,i\,y\,g) = \max(\text{dist}(x, y), \text{dist}(f, g)).
\]