Mathlib.Topology.EMetricSpace.Pi

instEDistForall instance

[∀ b, EDist (π b)] : EDist (∀ b, π b)

Full source

instance [∀ b, EDist (π b)] : EDist (∀ b, π b) where
  edist f g := Finset.sup univ fun b => edist (f b) (g b)

Extended Distance Structure on Indexed Products

Informal description

For any family of types $\pi_b$ indexed by $b$ where each $\pi_b$ is equipped with an extended distance structure, the product type $\forall b, \pi_b$ inherits an extended distance structure defined by taking the supremum of the componentwise extended distances over all indices $b$.

edist_pi_def theorem

[∀ b, EDist (π b)] (f g : ∀ b, π b) : edist f g = Finset.sup univ fun b => edist (f b) (g b)

Full source

theorem edist_pi_def [∀ b, EDist (π b)] (f g : ∀ b, π b) :
    edist f g = Finset.sup univ fun b => edist (f b) (g b) :=
  rfl

Definition of Extended Distance on Product Space via Componentwise Supremum

Informal description

For any family of types $\pi_b$ indexed by $b$ where each $\pi_b$ is equipped with an extended distance structure, the extended distance between two functions $f, g \in \prod_{b} \pi_b$ is given by the supremum of the componentwise extended distances over all indices $b$: \[ \text{edist}(f, g) = \sup_{b} \text{edist}(f(b), g(b)). \]

edist_le_pi_edist theorem

[∀ b, EDist (π b)] (f g : ∀ b, π b) (b : β) : edist (f b) (g b) ≤ edist f g

Full source

theorem edist_le_pi_edist [∀ b, EDist (π b)] (f g : ∀ b, π b) (b : β) :
    edist (f b) (g b) ≤ edist f g :=
  le_sup (f := fun b => edist (f b) (g b)) (Finset.mem_univ b)

Componentwise Extended Distance Bound in Product Space

Informal description

For any family of types $\pi_b$ indexed by $b$ where each $\pi_b$ is equipped with an extended distance structure, and for any two functions $f, g \colon \forall b, \pi_b$, the extended distance between $f(b)$ and $g(b)$ is less than or equal to the extended distance between $f$ and $g$ for any index $b$.

edist_pi_le_iff theorem

[∀ b, EDist (π b)] {f g : ∀ b, π b} {d : ℝ≥0∞} : edist f g ≤ d ↔ ∀ b, edist (f b) (g b) ≤ d

Full source

theorem edist_pi_le_iff [∀ b, EDist (π b)] {f g : ∀ b, π b} {d : ℝ≥0∞} :
    edistedist f g ≤ d ↔ ∀ b, edist (f b) (g b) ≤ d :=
  Finset.sup_le_iff.trans <| by simp only [Finset.mem_univ, forall_const]

Characterization of Extended Distance in Product Space via Componentwise Bounds

Informal description

Let $\{\pi_b\}_{b \in \beta}$ be a family of types, each equipped with an extended distance function $\text{edist}_b : \pi_b \times \pi_b \to \mathbb{R}_{\geq 0} \cup \{\infty\}$. For any two functions $f, g \in \prod_{b \in \beta} \pi_b$ and any extended nonnegative real number $d \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the extended distance between $f$ and $g$ satisfies \[ \text{edist}(f, g) \leq d \quad \text{if and only if} \quad \forall b \in \beta, \text{edist}_b(f(b), g(b)) \leq d. \]

edist_pi_const_le theorem

(a b : α) : (edist (fun _ : β => a) fun _ => b) ≤ edist a b

Full source

theorem edist_pi_const_le (a b : α) : (edist (fun _ : β => a) fun _ => b) ≤ edist a b :=
  edist_pi_le_iff.2 fun _ => le_rfl

Extended Distance Bound for Constant Functions in Product Space

Informal description

For any two elements $a$ and $b$ in a pseudo extended metric space $\alpha$, and for any index type $\beta$, the extended distance between the constant functions $\lambda \_, a$ and $\lambda \_, b$ from $\beta$ to $\alpha$ is bounded above by the extended distance between $a$ and $b$ in $\alpha$, i.e., \[ \text{edist}(\lambda \_, a, \lambda \_, b) \leq \text{edist}(a, b). \]

edist_pi_const theorem

[Nonempty β] (a b : α) : (edist (fun _ : β => a) fun _ => b) = edist a b

Full source

@[simp]
theorem edist_pi_const [Nonempty β] (a b : α) : (edist (fun _ : β => a) fun _ => b) = edist a b :=
  Finset.sup_const univ_nonempty (edist a b)

Extended Distance of Constant Functions in Product Space

Informal description

For any nonempty type $\beta$ and any two elements $a, b$ in a pseudo extended metric space $\alpha$, the extended distance between the constant functions $\lambda \_, a$ and $\lambda \_, b$ from $\beta$ to $\alpha$ is equal to the extended distance between $a$ and $b$ in $\alpha$, i.e., \[ \text{edist}(\lambda \_, a, \lambda \_, b) = \text{edist}(a, b). \]

pseudoEMetricSpacePi instance

[∀ b, PseudoEMetricSpace (π b)] : PseudoEMetricSpace (∀ b, π b)

Full source

/-- The product of a finite number of pseudoemetric spaces, with the max distance, is still
a pseudoemetric space.
This construction would also work for infinite products, but it would not give rise
to the product topology. Hence, we only formalize it in the good situation of finitely many
spaces. -/
instance pseudoEMetricSpacePi [∀ b, PseudoEMetricSpace (π b)] : PseudoEMetricSpace (∀ b, π b) where
  edist_self f := bot_unique <| Finset.sup_le <| by simp
  edist_comm f g := by simp [edist_pi_def, edist_comm]
  edist_triangle _ g _ := edist_pi_le_iff.2 fun b => le_trans (edist_triangle _ (g b) _)
    (add_le_add (edist_le_pi_edist _ _ _) (edist_le_pi_edist _ _ _))
  toUniformSpace := Pi.uniformSpace _
  uniformity_edist := by
    simp only [Pi.uniformity, PseudoEMetricSpace.uniformity_edist, comap_iInf, gt_iff_lt,
      preimage_setOf_eq, comap_principal, edist_pi_def]
    rw [iInf_comm]; congr; funext ε
    rw [iInf_comm]; congr; funext εpos
    simp [setOf_forall, εpos]

Pseudo Extended Metric Space Structure on Finite Products

Informal description

For any finite family of pseudo extended metric spaces $\{\pi_b\}_{b \in \beta}$, the product space $\prod_{b \in \beta} \pi_b$ equipped with the supremum of componentwise extended distances forms a pseudo extended metric space. This construction preserves the pseudo extended metric space properties (reflexivity, symmetry, and triangle inequality) but does not necessarily induce the product topology for infinite products.

emetricSpacePi instance

[∀ b, EMetricSpace (π b)] : EMetricSpace (∀ b, π b)

Full source

/-- The product of a finite number of emetric spaces, with the max distance, is still
an emetric space.
This construction would also work for infinite products, but it would not give rise
to the product topology. Hence, we only formalize it in the good situation of finitely many
spaces. -/
instance emetricSpacePi [∀ b, EMetricSpace (π b)] : EMetricSpace (∀ b, π b) :=
  .ofT0PseudoEMetricSpace _

Extended Metric Space Structure on Finite Products

Informal description

For any finite family of extended metric spaces $\{\pi_b\}_{b \in \beta}$, the product space $\prod_{b \in \beta} \pi_b$ equipped with the supremum of componentwise extended distances forms an extended metric space. This construction preserves the extended metric space properties (non-degeneracy, symmetry, and triangle inequality) and induces the product topology for finite products.