TODO

theorem exists_radius_le {T : Type u_1} [PseudoEMetricSpace T] {a : ENNReal} (t : T) (V : Finset T) (ha : 1 < a) (c : ENNReal) : ∃ (r : ℕ), 1 ≤ r ∧ ↑{x ∈ V | edist t x ≤ ↑r * c}.card ≤ a ^ r

noncomputable def logSizeRadius {T : Type u_1} [PseudoEMetricSpace T] (t : T) (V : Finset T) (a c : ENNReal) : ℕ

Equations

• logSizeRadius t V a c = if h : 1 < a then Nat.find ⋯ else 0

theorem one_le_logSizeRadius {T : Type u_1} [PseudoEMetricSpace T] {a c : ENNReal} {V : Finset T} {t : T} (ha : 1 < a) : 1 ≤ logSizeRadius t V a c

theorem card_le_logSizeRadius_le {T : Type u_1} [PseudoEMetricSpace T] {a c : ENNReal} {V : Finset T} {t : T} (ha : 1 < a) : ↑{x ∈ V | edist t x ≤ ↑(logSizeRadius t V a c) * c}.card ≤ a ^ logSizeRadius t V a c

theorem card_le_logSizeRadius_ge {T : Type u_1} [PseudoEMetricSpace T] {a c : ENNReal} {V : Finset T} {t : T} (ha : 1 < a) (ht : t ∈ V) : a ^ (logSizeRadius t V a c - 1) ≤ ↑{x ∈ V | edist t x ≤ (↑(logSizeRadius t V a c) - 1) * c}.card

structure logSizeBallStruct (T : Type u_2) : Type u_2

• finset : Finset T
• point : T
• radius : ℕ

noncomputable def logSizeBallStruct.smallBall {T : Type u_1} [PseudoEMetricSpace T] (struct : logSizeBallStruct T) (c : ENNReal) : Finset T

Equations

• struct.smallBall c = {x ∈ struct.finset | edist struct.point x ≤ (↑struct.radius - 1) * c}

noncomputable def logSizeBallStruct.ball {T : Type u_1} [PseudoEMetricSpace T] (struct : logSizeBallStruct T) (c : ENNReal) : Finset T

Equations

• struct.ball c = {x ∈ struct.finset | edist struct.point x ≤ ↑struct.radius * c}

noncomputable def logSizeBallSeq {T : Type u_1} [PseudoEMetricSpace T] (J : Finset T) (hJ : J.Nonempty) (a c : ENNReal) : ℕ → logSizeBallStruct T

Equations

• One or more equations did not get rendered due to their size.

theorem finset_logSizeBallSeq_zero {T : Type u_1} [PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} (hJ : J.Nonempty) : (logSizeBallSeq J hJ a c 0).finset = J

theorem point_logSizeBallSeq_zero {T : Type u_1} [PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} (hJ : J.Nonempty) : (logSizeBallSeq J hJ a c 0).point = Exists.choose hJ

theorem radius_logSizeBallSeq_zero {T : Type u_1} [PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} (hJ : J.Nonempty) : (logSizeBallSeq J hJ a c 0).radius = logSizeRadius (Exists.choose hJ) J a c

theorem finset_logSizeBallSeq_add_one {T : Type u_1} [PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} (hJ : J.Nonempty) (i : ℕ) : (logSizeBallSeq J hJ a c (i + 1)).finset = (logSizeBallSeq J hJ a c i).finset \ (logSizeBallSeq J hJ a c i).smallBall c

theorem point_logSizeBallSeq_add_one {T : Type u_1} [PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} (hJ : J.Nonempty) (i : ℕ) : (logSizeBallSeq J hJ a c (i + 1)).point = if hV' : (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty then Exists.choose hV' else (logSizeBallSeq J hJ a c i).point

theorem radius_logSizeBallSeq_add_one {T : Type u_1} [PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} (hJ : J.Nonempty) (i : ℕ) : (logSizeBallSeq J hJ a c (i + 1)).radius = logSizeRadius (logSizeBallSeq J hJ a c (i + 1)).point (logSizeBallSeq J hJ a c (i + 1)).finset a c

theorem radius_logSizeBallSeq_le {T : Type u_1} [PseudoEMetricSpace T] {a c : ENNReal} {n : ℕ} {J : Finset T} (hJ : J.Nonempty) (hJ_card : ↑J.card ≤ a ^ n) (i : ℕ) : (logSizeBallSeq J hJ a c i).radius ≤ n

theorem finset_logSizeBallSeq_add_one_subset {T : Type u_1} [PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} (hJ : J.Nonempty) (i : ℕ) : (logSizeBallSeq J hJ a c (i + 1)).finset ⊆ (logSizeBallSeq J hJ a c i).finset

theorem point_mem_finset_logSizeBallSeq {T : Type u_1} [PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} (hJ : J.Nonempty) (i : ℕ) (h : (logSizeBallSeq J hJ a c i).finset.Nonempty) : (logSizeBallSeq J hJ a c i).point ∈ (logSizeBallSeq J hJ a c i).finset

theorem point_notMem_finset_logSizeBallSeq_add_one {T : Type u_1} [PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} (hJ : J.Nonempty) (i : ℕ) (h : (logSizeBallSeq J hJ a c i).finset.Nonempty) : (logSizeBallSeq J hJ a c i).point ∉ (logSizeBallSeq J hJ a c (i + 1)).finset

theorem card_finset_logSizeBallSeq_add_one_lt {T : Type u_1} [PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} (hJ : J.Nonempty) (i : ℕ) (h : (logSizeBallSeq J hJ a c i).finset.Nonempty) : (logSizeBallSeq J hJ a c (i + 1)).finset.card < (logSizeBallSeq J hJ a c i).finset.card

theorem card_finset_logSizeBallSeq_le {T : Type u_1} [PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} (hJ : J.Nonempty) (i : ℕ) : (logSizeBallSeq J hJ a c i).finset.card ≤ J.card - i

theorem card_finset_logSizeBallSeq_card_eq_zero {T : Type u_1} [PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} (hJ : J.Nonempty) : (logSizeBallSeq J hJ a c J.card).finset.card = 0

theorem disjoint_smallBall_logSizeBallSeq {T : Type u_1} [PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} (hJ : J.Nonempty) (i j : ℕ) (hij : i ≠ j) : Disjoint ((logSizeBallSeq J hJ a c i).smallBall c) ((logSizeBallSeq J hJ a c j).smallBall c)

noncomputable def pairSetSeq {T : Type u_1} [PseudoEMetricSpace T] (J : Finset T) (a c : ENNReal) (n : ℕ) : Finset (T × T)

Equations

• pairSetSeq J a c n = if hJ : J.Nonempty then {(logSizeBallSeq J hJ a c n).point}.product ((logSizeBallSeq J hJ a c n).ball c) else ∅

noncomputable def pairSet {T : Type u_1} [PseudoEMetricSpace T] (J : Finset T) (a c : ENNReal) : Finset (T × T)

Equations

• pairSet J a c = (Finset.range J.card).biUnion (pairSetSeq J a c)

theorem pairSet_subset {T : Type u_1} [PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} : pairSet J a c ⊆ J.product J

theorem card_pairSet_le {T : Type u_1} [PseudoEMetricSpace T] {a c : ENNReal} {n : ℕ} {J : Finset T} (hJ_card : ↑J.card ≤ a ^ n) (ha : 1 < a) : ↑(pairSet J a c).card ≤ a * ↑J.card

theorem edist_le_of_mem_pairSet {T : Type u_1} [PseudoEMetricSpace T] {a c : ENNReal} {n : ℕ} {J : Finset T} (hJ_card : ↑J.card ≤ a ^ n) (ha : 1 < a) (hc : c ≠ 0) {s t : T} (h : (s, t) ∈ pairSet J a c) : edist s t ≤ ↑n * c

theorem iSup_edist_pairSet {T : Type u_1} [PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} {E : Type u_2} [PseudoEMetricSpace E] (f : T → E) : ⨆ (s : T), ⨆ (t : T), ⨆ (_ : s ∈ J), ⨆ (_ : t ∈ J), ⨆ (_ : edist s t ≤ c), edist (f s) (f t) ≤ 2 * ⨆ p ∈ pairSet J a c, edist (f p.1) (f p.2)

theorem pair_reduction {T : Type u_1} [PseudoEMetricSpace T] {a c : ENNReal} {n : ℕ} (J : Finset T) (hJ : ↑J.card ≤ a ^ n) (ha : 1 < a) (hc : c ≠ 0) (E : Type u_2) [PseudoEMetricSpace E] : ∃ K ⊆ J.product J, ↑K.card ≤ a * ↑J.card ∧ (∀ (s t : T), (s, t) ∈ K → edist s t ≤ ↑n * c) ∧ ∀ (f : T → E), ⨆ (s : T), ⨆ (t : T), ⨆ (_ : s ∈ J), ⨆ (_ : t ∈ J), ⨆ (_ : edist s t ≤ c), edist (f s) (f t) ≤ 2 * ⨆ p ∈ K, edist (f p.1) (f p.2)