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 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 antitone_logSizeBallSeq_add_one_subset {T : Type u_1} [PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} (hJ : J.Nonempty) : Antitone fun (i : ℕ) => (logSizeBallSeq J hJ a c i).finset

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

theorem one_le_radius_logSizeBallSeq {T : Type u_1} [PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} (hJ : J.Nonempty) (ha : 1 < a) (i : ℕ) : 1 ≤ (logSizeBallSeq J hJ a c i).radius

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_mem_logSizeBallSeq_zero {T : Type u_1} [PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} (hJ : J.Nonempty) (i : ℕ) : (logSizeBallSeq J hJ a c i).point ∈ J

theorem point_notMem_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).point ∉ (logSizeBallSeq J hJ a c (i + 1)).finset

theorem finset_logSizeBallSeq_add_one_ssubset {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 ⊂ (logSizeBallSeq J hJ a c i).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_pairSetSeq_le_logSizeRadius {T : Type u_1} [PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} (hJ : J.Nonempty) (i : ℕ) (ha : 1 < a) : ↑(pairSetSeq J a c i).card ≤ (if (logSizeBallSeq J hJ a c i).finset.Nonempty then 1 else 0) * a ^ (logSizeBallSeq J hJ a c i).radius

theorem logSizeRadius_le_card_smallBall {T : Type u_1} [PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} (hJ : J.Nonempty) (i : ℕ) (ha : 1 < a) : (if (logSizeBallSeq J hJ a c i).finset.Nonempty then 1 else 0) * a ^ ((logSizeBallSeq J hJ a c i).radius - 1) ≤ ↑((logSizeBallSeq J hJ a c i).smallBall c).card

theorem card_pairSet_le {T : Type u_1} [PseudoEMetricSpace T] {a c : ENNReal} {n : ℕ} {J : Finset T} (ha : 1 < a) (hJ_card : ↑J.card ≤ a ^ n) : ↑(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} (ha : 1 < a) (hJ_card : ↑J.card ≤ a ^ n) {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] (ha : 1 < a) (f : T → E) : ⨆ (s : { x : T // x ∈ J }), ⨆ (t : { t : { x : T // x ∈ J } // edist s t ≤ c }), edist (f ↑s) (f ↑↑t) ≤ 2 * ⨆ (p : { x : T × T // x ∈ 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_card : ↑J.card ≤ a ^ n) (ha : 1 < a) (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 : { x : T // x ∈ J }), ⨆ (t : { t : { x : T // x ∈ J } // edist s t ≤ c }), edist (f ↑s) (f ↑↑t) ≤ 2 * ⨆ (p : { x : T × T // x ∈ K }), edist (f (↑p).1) (f (↑p).2)