Product of pseudometric spaces

This file constructs the infinity distance on finite products of pseudometric spaces.

@[instance_reducible]

instance pseudoMetricSpacePi {β : Type u_2} {X : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (X b)] : PseudoMetricSpace ((b : β) → X b)

A finite product of pseudometric spaces is a pseudometric space, with the sup distance.

Equations

• pseudoMetricSpacePi = (PseudoEMetricSpace.toPseudoMetricSpaceOfDist (fun (f g : (b : β) → X b) => ↑(Finset.univ.sup fun (b : β) => nndist (f b) (g b))) ⋯ ⋯).replaceBornology ⋯

theorem nndist_pi_def {β : Type u_2} {X : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (X b)] (f g : (b : β) → X b) : nndist f g = Finset.univ.sup fun (b : β) => nndist (f b) (g b)

theorem dist_pi_def {β : Type u_2} {X : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (X b)] (f g : (b : β) → X b) : dist f g = ↑(Finset.univ.sup fun (b : β) => nndist (f b) (g b))

theorem nndist_pi_le_iff {β : Type u_2} {X : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (X b)] {f g : (b : β) → X b} {r : NNReal} : nndist f g ≤ r ↔ ∀ (b : β), nndist (f b) (g b) ≤ r

theorem nndist_pi_lt_iff {β : Type u_2} {X : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (X b)] {f g : (b : β) → X b} {r : NNReal} (hr : 0 < r) : nndist f g < r ↔ ∀ (b : β), nndist (f b) (g b) < r

theorem nndist_pi_eq_iff {β : Type u_2} {X : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (X b)] {f g : (b : β) → X b} {r : NNReal} (hr : 0 < r) : nndist f g = r ↔ (∃ (i : β), nndist (f i) (g i) = r) ∧ ∀ (b : β), nndist (f b) (g b) ≤ r

theorem dist_pi_lt_iff {β : Type u_2} {X : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (X b)] {f g : (b : β) → X b} {r : ℝ} (hr : 0 < r) : dist f g < r ↔ ∀ (b : β), dist (f b) (g b) < r

theorem dist_pi_le_iff {β : Type u_2} {X : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (X b)] {f g : (b : β) → X b} {r : ℝ} (hr : 0 ≤ r) : dist f g ≤ r ↔ ∀ (b : β), dist (f b) (g b) ≤ r

theorem dist_pi_eq_iff {β : Type u_2} {X : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (X b)] {f g : (b : β) → X b} {r : ℝ} (hr : 0 < r) : dist f g = r ↔ (∃ (i : β), dist (f i) (g i) = r) ∧ ∀ (b : β), dist (f b) (g b) ≤ r

theorem dist_pi_le_iff' {β : Type u_2} {X : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (X b)] [Nonempty β] {f g : (b : β) → X b} {r : ℝ} : dist f g ≤ r ↔ ∀ (b : β), dist (f b) (g b) ≤ r

theorem dist_pi_const_le {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [Fintype β] (a b : α) : (dist (fun (x : β) => a) fun (x : β) => b) ≤ dist a b

theorem nndist_pi_const_le {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [Fintype β] (a b : α) : (nndist (fun (x : β) => a) fun (x : β) => b) ≤ nndist a b

@[simp]

theorem dist_pi_const {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [Fintype β] [Nonempty β] (a b : α) : (dist (fun (x : β) => a) fun (x : β) => b) = dist a b

@[simp]

theorem nndist_pi_const {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [Fintype β] [Nonempty β] (a b : α) : (nndist (fun (x : β) => a) fun (x : β) => b) = nndist a b

theorem nndist_le_pi_nndist {β : Type u_2} {X : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (X b)] (f g : (b : β) → X b) (b : β) : nndist (f b) (g b) ≤ nndist f g

theorem dist_le_pi_dist {β : Type u_2} {X : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (X b)] (f g : (b : β) → X b) (b : β) : dist (f b) (g b) ≤ dist f g

theorem ball_pi {β : Type u_2} {X : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (X b)] (x : (b : β) → X b) {r : ℝ} (hr : 0 < r) : Metric.ball x r = Set.univ.pi fun (b : β) => Metric.ball (x b) r

An open ball in a product space is a product of open balls. See also ball_pi' for a version assuming Nonempty β instead of 0 < r.

theorem ball_pi' {β : Type u_2} {X : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (X b)] [Nonempty β] (x : (b : β) → X b) (r : ℝ) : Metric.ball x r = Set.univ.pi fun (b : β) => Metric.ball (x b) r

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 β.

theorem closedBall_pi {β : Type u_2} {X : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (X b)] (x : (b : β) → X b) {r : ℝ} (hr : 0 ≤ r) : Metric.closedBall x r = Set.univ.pi fun (b : β) => Metric.closedBall (x b) r

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.

theorem closedBall_pi' {β : Type u_2} {X : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (X b)] [Nonempty β] (x : (b : β) → X b) (r : ℝ) : Metric.closedBall x r = Set.univ.pi fun (b : β) => Metric.closedBall (x b) r

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 β.

theorem sphere_pi {β : Type u_2} {X : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (X b)] (x : (b : β) → X b) {r : ℝ} (h : 0 < r ∨ Nonempty β) : Metric.sphere x r = (⋃ (i : β), Function.eval i ⁻¹' Metric.sphere (x i) r) ∩ Metric.closedBall x r

A sphere in a product space is a union of spheres on each component restricted to the closed ball.

@[simp]

theorem Fin.nndist_insertNth_insertNth {n : ℕ} {α : Fin (n + 1) → Type u_4} [(i : Fin (n + 1)) → PseudoMetricSpace (α i)] (i : Fin (n + 1)) (x y : α i) (f g : (j : Fin n) → α (i.succAbove j)) : nndist (i.insertNth x f) (i.insertNth y g) = max (nndist x y) (nndist f g)

@[simp]

theorem Fin.dist_insertNth_insertNth {n : ℕ} {α : Fin (n + 1) → Type u_4} [(i : Fin (n + 1)) → PseudoMetricSpace (α i)] (i : Fin (n + 1)) (x y : α i) (f g : (j : Fin n) → α (i.succAbove j)) : dist (i.insertNth x f) (i.insertNth y g) = max (dist x y) (dist f g)

theorem nndist_single_single {β : Type u_2} [Fintype β] {Y : Type u_4} [PseudoMetricSpace Y] [Zero Y] [DecidableEq β] (i j : β) (a b : Y) (h : i ≠ j) : nndist (Pi.single i a) (Pi.single j b) = max (nndist a 0) (nndist b 0)

The (sup metric) nonnegative distance between Pi.single i a and Pi.single j b for i ≠ j is max (nndist a 0) (nndist b 0).

theorem dist_single_single {β : Type u_2} [Fintype β] {Y : Type u_4} [PseudoMetricSpace Y] [Zero Y] [DecidableEq β] (i j : β) (a b : Y) (h : i ≠ j) : dist (Pi.single i a) (Pi.single j b) = max (dist a 0) (dist b 0)

The (sup metric) distance between Pi.single i a and Pi.single j b for i ≠ j is max (dist a 0) (dist b 0).