Basic definitions

This module contains the definitions mentioned in Chapter 2 of the ANTEDB blueprint.

When a blueprint convention already has a standard Mathlib representation, prefer using that representation directly, for example: -the notation e(θ) is 𝐞 θ after open scoped FourierTransform; -for indicator functions, use Set.indicator; -for suprema and infima, including those of empty sets, use Mathlib's sSup and sInf; -for finite cardinalities use Finset.card;

def Expdb.IsSeparatedFamily {ι : Type u_1} {α : Type u_2} [PseudoMetricSpace α] (δ : ℝ) (x : ι → α) : Prop

A family in a pseudo-metric space is δ-separated when distinct indices have values at least δ apart. This uses a non-strict inequality, unlike Metric.IsSeparated.

Equations

• Expdb.IsSeparatedFamily δ x = Pairwise fun (i j : ι) => δ ≤ dist (x i) (x j)

def Expdb.IsSeparated {α : Type u_1} [PseudoMetricSpace α] (δ : ℝ) (W : Finset α) : Prop

A finite set is δ-separated when distinct elements are at least δ apart.

Equations

• Expdb.IsSeparated δ W = Expdb.IsSeparatedFamily δ fun (t : ↥W) => ↑t

@[reducible, inline]

abbrev Expdb.IsOneSeparated {α : Type u_1} [PseudoMetricSpace α] (W : Finset α) : Prop

A finite set is 1-separated.

Equations

• Expdb.IsOneSeparated W = Expdb.IsSeparated 1 W

def Expdb.IsBoundedFamily {ι : Type u_1} {β : Type u_2} [Norm β] (C : ℝ) (a : ι → β) : Prop

A family in a normed type is C-bounded when every value has norm at most C.

Equations

• Expdb.IsBoundedFamily C a = ∀ (i : ι), ‖a i‖ ≤ C

@[reducible, inline]

abbrev Expdb.IsOneBounded {ι : Type u_1} {β : Type u_2} [Norm β] (a : ι → β) : Prop

A family in a normed type is 1-bounded.

Equations

• Expdb.IsOneBounded a = Expdb.IsBoundedFamily 1 a