Anchored families and their positive witness geometry

@[reducible, inline]

abbrev GenLimit.FiniteWitness.Anchored.Point : Type

Two disjoint copies of the natural numbers for the anchored hierarchy examples.

Equations

• GenLimit.FiniteWitness.Anchored.Point = (ℕ ⊕ ℕ)

def GenLimit.FiniteWitness.Anchored.leftTarget {k : ℕ} (i : Fin k) (D : Set ℕ) : Set Point

A full left copy, all right anchors except one, and an arbitrary right tail.

Equations

• GenLimit.FiniteWitness.Anchored.leftTarget i D = Sum.elim (fun (x : ℕ) => True) fun (n : ℕ) => if n < k then n ≠ ↑i else n - k ∈ D

def GenLimit.FiniteWitness.Anchored.rightTarget {k : ℕ} (j : Fin k) (E : Set ℕ) : Set Point

A full right copy, all left anchors except one, and an arbitrary left tail.

Equations

• GenLimit.FiniteWitness.Anchored.rightTarget j E = Sum.elim (fun (n : ℕ) => if n < k then n ≠ ↑j else n - k ∈ E) fun (x : ℕ) => True

def GenLimit.FiniteWitness.Anchored.family (k : ℕ) : Set (Set Point)

The union of the left and right anchored target families with k anchors.

Equations

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

@[simp]

theorem GenLimit.FiniteWitness.Anchored.inl_mem_left {k : ℕ} (i : Fin k) (D : Set ℕ) (n : ℕ) : Sum.inl n ∈ leftTarget i D

@[simp]

theorem GenLimit.FiniteWitness.Anchored.inr_mem_right {k : ℕ} (j : Fin k) (E : Set ℕ) (n : ℕ) : Sum.inr n ∈ rightTarget j E

@[simp]

theorem GenLimit.FiniteWitness.Anchored.inr_mem_left_iff {k : ℕ} (i : Fin k) (D : Set ℕ) (n : ℕ) : Sum.inr n ∈ leftTarget i D ↔ if n < k then n ≠ ↑i else n - k ∈ D

@[simp]

theorem GenLimit.FiniteWitness.Anchored.inl_mem_right_iff {k : ℕ} (j : Fin k) (E : Set ℕ) (n : ℕ) : Sum.inl n ∈ rightTarget j E ↔ if n < k then n ≠ ↑j else n - k ∈ E

theorem GenLimit.FiniteWitness.Anchored.anchor_mem_left {k : ℕ} (i j : Fin k) (D : Set ℕ) : Sum.inr ↑j ∈ leftTarget i D ↔ j ≠ i

theorem GenLimit.FiniteWitness.Anchored.anchor_mem_right {k : ℕ} (i j : Fin k) (E : Set ℕ) : Sum.inl ↑i ∈ rightTarget j E ↔ i ≠ j

theorem GenLimit.FiniteWitness.Anchored.tail_mem_left {k : ℕ} (i : Fin k) (D : Set ℕ) (n : ℕ) : Sum.inr (k + n) ∈ leftTarget i D ↔ n ∈ D

theorem GenLimit.FiniteWitness.Anchored.tail_mem_right {k : ℕ} (j : Fin k) (E : Set ℕ) (n : ℕ) : Sum.inl (k + n) ∈ rightTarget j E ↔ n ∈ E

theorem GenLimit.FiniteWitness.Anchored.left_mem_family {k : ℕ} (i : Fin k) (D : Set ℕ) : leftTarget i D ∈ family k

theorem GenLimit.FiniteWitness.Anchored.right_mem_family {k : ℕ} (j : Fin k) (E : Set ℕ) : rightTarget j E ∈ family k

theorem GenLimit.FiniteWitness.Anchored.family_uus (k : ℕ) : Generic.UUS (family k)

theorem GenLimit.FiniteWitness.Anchored.left_injective {k : ℕ} : Function.Injective fun (p : Fin k × Set ℕ) => leftTarget p.1 p.2

theorem GenLimit.FiniteWitness.Anchored.right_injective {k : ℕ} : Function.Injective fun (p : Fin k × Set ℕ) => rightTarget p.1 p.2

theorem GenLimit.FiniteWitness.Anchored.left_ne_right {k : ℕ} (i j : Fin k) (D E : Set ℕ) : leftTarget i D ≠ rightTarget j E

noncomputable def GenLimit.FiniteWitness.Anchored.rightTail (k : ℕ) (S : Finset Point) : Finset ℕ

The indices of observed right-copy elements beyond the first k anchors.

Equations

• GenLimit.FiniteWitness.Anchored.rightTail k S = S.preimage (fun (n : ℕ) => Sum.inr (k + n)) ⋯

@[simp]

theorem GenLimit.FiniteWitness.Anchored.mem_rightTail (k : ℕ) (S : Finset Point) (n : ℕ) : n ∈ rightTail k S ↔ Sum.inr (k + n) ∈ S

theorem GenLimit.FiniteWitness.Anchored.card_rightTail_le (k : ℕ) (S : Finset Point) : (rightTail k S).card ≤ S.card

noncomputable def GenLimit.FiniteWitness.Anchored.leftAnchors (k : ℕ) (S : Finset Point) : Finset (Fin k)

The left anchors present in a finite sample.

Equations

• GenLimit.FiniteWitness.Anchored.leftAnchors k S = S.preimage (fun (i : Fin k) => Sum.inl ↑i) ⋯

noncomputable def GenLimit.FiniteWitness.Anchored.rightAnchors (k : ℕ) (S : Finset Point) : Finset (Fin k)

The right anchors present in a finite sample.

Equations

• GenLimit.FiniteWitness.Anchored.rightAnchors k S = S.preimage (fun (i : Fin k) => Sum.inr ↑i) ⋯

@[simp]

theorem GenLimit.FiniteWitness.Anchored.mem_leftAnchors {k : ℕ} (S : Finset Point) (i : Fin k) : i ∈ leftAnchors k S ↔ Sum.inl ↑i ∈ S

@[simp]

theorem GenLimit.FiniteWitness.Anchored.mem_rightAnchors {k : ℕ} (S : Finset Point) (i : Fin k) : i ∈ rightAnchors k S ↔ Sum.inr ↑i ∈ S

theorem GenLimit.FiniteWitness.Anchored.card_leftAnchors_le (k : ℕ) (S : Finset Point) : (leftAnchors k S).card ≤ S.card

theorem GenLimit.FiniteWitness.Anchored.card_rightAnchors_le (k : ℕ) (S : Finset Point) : (rightAnchors k S).card ≤ S.card

def GenLimit.FiniteWitness.Anchored.leftCore {k : ℕ} (T : Set Point → Finset Point) (i : Fin k) (S : Finset Point) : Set ℕ

The common tail of all active left targets with a fixed missing anchor.

Equations

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

theorem GenLimit.FiniteWitness.Anchored.shift_infinite {C : Set ℕ} (hC : C.Infinite) (k : ℕ) : {n : ℕ | k + n ∈ C}.Infinite

theorem GenLimit.FiniteWitness.Anchored.right_part_infinite {J : Set Point} (hJ : J.Infinite) (hf : {n : ℕ | Sum.inl n ∈ J}.Finite) : {n : ℕ | Sum.inr n ∈ J}.Infinite

theorem GenLimit.FiniteWitness.Anchored.right_target_left_finite {k : ℕ} (j : Fin k) {E : Set ℕ} (hE : E.Finite) : {n : ℕ | Sum.inl n ∈ rightTarget j E}.Finite

theorem GenLimit.FiniteWitness.Anchored.leftCore_infinite_of_active_right {k : ℕ} {T : Set Point → Finset Point} (hT : Valid (family k) T) {S : Finset Point} (hS : (active (family k) T S).Nonempty) (i j : Fin k) {E : Set ℕ} (hE : E.Finite) (hR : rightTarget j E ∈ active (family k) T S) : (leftCore T i S).Infinite