GraphHierarchy.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

The finite hierarchy and the actual tree of extensions used in the graph application. Histories are represented by the probability tree's dependent paths; equal set labels do not identify distinct histories.

structure OAI.LeanBlast.SecondKahnKalai.SetHierarchy line 22
Source documentation
A reversed predecessor chain, with its first term empty and last term the given set. The relation records the actual rule used to select predecessors.
```
structure SetHierarchy {X : Type*} [DecidableEq X]
    (R : Finset X → Finset X → Prop) (H : Finset X) where
…
```
theorem OAI.LeanBlast.SecondKahnKalai.SetHierarchy.stage_subset_stage line 37
theorem OAI.LeanBlast.SecondKahnKalai.SetHierarchy.stage_subset line 44
theorem OAI.LeanBlast.SecondKahnKalai.SetHierarchy.depth_pos line 48
def OAI.LeanBlast.SecondKahnKalai.SetHierarchy.capacity line 55
Source documentation
The number of new elements on a level of the hierarchy.
```
def capacity (h : SetHierarchy R H) (i : ℕ) : ℕ :=
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.SetHierarchy
theorem OAI.LeanBlast.SecondKahnKalai.SetHierarchy.capacity_pos line 58
theorem OAI.LeanBlast.SecondKahnKalai.SetHierarchy.capacity_growth line 64
theorem OAI.LeanBlast.SecondKahnKalai.SetHierarchy.capacity_le line 70
theorem OAI.LeanBlast.SecondKahnKalai.exists_setHierarchy line 78
Source documentation
Strict cardinal descent constructs a finite hierarchy; no chain or tree is assumed as an input. The predecessor hypotheses are needed only inside H.
```
theorem exists_setHierarchy {X : Type*} [DecidableEq X]
    (R : Finset X → Finset X → Prop) (H : Finset X)
    (hpred : ∀ I, I ⊆ H → I.Nonempty →
      ∃ S, S ⊆ I ∧ 17 * S.card < I.card ∧ R S I) :
    Nonempty (SetHierarchy R H) := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.SetHierarchy
theorem OAI.LeanBlast.SecondKahnKalai.extensionLaw_isSpread_of_ratio line 143
Source documentation
A conditional containment-ratio estimate is exactly spreadness of the added set. Requests intersecting the existing set have probability zero.
```
theorem extensionLaw_isSpread_of_ratio (I S : Finset X)
    (hp : 0 < containmentProb G I S) (σ : ℝ) (hσ : 0 ≤ σ)
    (hratio : ∀ J : Finset X, J.Nonempty → Disjoint S J →
      containmentProb G I (S ∪ J) / containmentProb G I S ≤ σ ^ J.card) :
    IsSpread (extensionLaw G I S hp) (fun b => b.val.val \ S) σ := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.containmentProb, OAI.LeanBlast.SecondKahnKalai.IsSpread, OAI.LeanBlast.SecondKahnKalai.extensionLaw
def OAI.LeanBlast.SecondKahnKalai.orbitExtensionTree line 158
Source documentation
The actual extension tree. At each node its children are all distinct copies of the next set containing the current copy, with their uniform law. The dependent path type retains the entire sequence of choices.
```
def orbitExtensionTree : (d : ℕ) → (A : ℕ → Finset X) →
    (∀ i, i < d → A i ⊆ A (i + 1)) →
    (S0 : Finset X) → S0 ∈ copyOrbit G (A 0) → ProbabilityTree X d
  | 0, _, _, _, _ => .leaf
  | d + 1, A, hnested, S0, hS0 =>
      let hp := containmentProb_pos_of_copy_subset G (hnested 0 (by omega)) hS0
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.copyOrbit, OAI.LeanBlast.SecondKahnKalai.ProbabilityTree, OAI.LeanBlast.SecondKahnKalai.containmentProb_pos_of_copy_subset
theorem OAI.LeanBlast.SecondKahnKalai.orbitExtensionTree_support_disjoint line 172
Source documentation
No element already present at a node occurs anywhere below it.
```
theorem orbitExtensionTree_support_disjoint (d : ℕ) (A : ℕ → Finset X)
    (hnested : ∀ i, i < d → A i ⊆ A (i + 1))
    (S0 : Finset X) (hS0 : S0 ∈ copyOrbit G (A 0)) :
    Disjoint S0 (orbitExtensionTree G d A hnested S0 hS0).support := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.copyOrbit, OAI.LeanBlast.SecondKahnKalai.orbitExtensionTree
theorem OAI.LeanBlast.SecondKahnKalai.orbitExtensionTree_isDisjoint line 190
Source documentation
Every constructed tree has the strong recursive disjointness property.
```
theorem orbitExtensionTree_isDisjoint (d : ℕ) (A : ℕ → Finset X)
    (hnested : ∀ i, i < d → A i ⊆ A (i + 1))
    (S0 : Finset X) (hS0 : S0 ∈ copyOrbit G (A 0)) :
    (orbitExtensionTree G d A hnested S0 hS0).IsDisjoint := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.copyOrbit, OAI.LeanBlast.SecondKahnKalai.orbitExtensionTree

theorem OAI.LeanBlast.SecondKahnKalai.orbitExtensionTree_pathUnion line 209

Source documentation

Adding a path's labels to its starting copy recovers an actual terminal copy. In particular an empty root gives an actual copy as its path union.

theorem orbitExtensionTree_pathUnion (d : ℕ) (A : ℕ → Finset X)
    (hnested : ∀ i, i < d → A i ⊆ A (i + 1))
    (S0 : Finset X) (hS0 : S0 ∈ copyOrbit G (A 0))
    (p : (orbitExtensionTree G d A hnested S0 hS0).Path) :
    S0 ∪ (orbitExtensionTree G d A hnested S0 hS0).pathUnion p ∈
      copyOrbit G (A d) := by
…

Mentions: OAI.LeanBlast.SecondKahnKalai.copyOrbit, OAI.LeanBlast.SecondKahnKalai.orbitExtensionTree

theorem OAI.LeanBlast.SecondKahnKalai.orbitExtensionTree_hasCapacities line 226
Source documentation
Every arc has exactly the cardinal difference of its two abstract stages, so these differences are valid capacities at every node of the tree.
```
theorem orbitExtensionTree_hasCapacities (d : ℕ) (A : ℕ → Finset X)
    (hnested : ∀ i, i < d → A i ⊆ A (i + 1))
    (S0 : Finset X) (hS0 : S0 ∈ copyOrbit G (A 0)) :
    (orbitExtensionTree G d A hnested S0 hS0).HasCapacities
      (fun i => (A (i + 1)).card - (A i).card) := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.copyOrbit, OAI.LeanBlast.SecondKahnKalai.orbitExtensionTree

theorem OAI.LeanBlast.SecondKahnKalai.orbitExtensionTree_hasSpread line 245

Source documentation

Local conditional containment ratios give spread at every node, including nodes reached through different histories with the same current copy.

theorem orbitExtensionTree_hasSpread (σ : ℝ) (hσ : 0 ≤ σ)
    (d : ℕ) (A : ℕ → Finset X)
    (hnested : ∀ i, i < d → A i ⊆ A (i + 1))
    (hratio : ∀ i, i < d → ∀ S0 ∈ copyOrbit G (A i),
      ∀ J : Finset X, J.Nonempty → Disjoint S0 J →
        containmentProb G (A (i + 1)) (S0 ∪ J) /
          containmentProb G (A (i + 1)) S0 ≤ σ ^ J.card)
    (S0 : Finset X) (hS0 : S0 ∈ copyOrbit G (A 0)) :
    (orbitExtensionTree G d A hnested S0 hS0).HasSpread (fun _ => σ) := by
…

Mentions: OAI.LeanBlast.SecondKahnKalai.copyOrbit, OAI.LeanBlast.SecondKahnKalai.containmentProb, OAI.LeanBlast.SecondKahnKalai.orbitExtensionTree

theorem OAI.LeanBlast.SecondKahnKalai.exists_spread_orbit_tree_of_predecessors line 269

Source documentation

The constructive assembly from a strict predecessor rule. In particular, the tree and its chain are outputs, not hypotheses. The concrete maximizing rule below discharges the two local predecessor requirements.

theorem exists_spread_orbit_tree_of_predecessors
    (H : Finset X) (hH : H.Nonempty) (σ : ℝ) (hσ : 0 ≤ σ)
    (R : Finset X → Finset X → Prop)
    (hpred : ∀ I, I ⊆ H → I.Nonempty →
      ∃ S, S ⊆ I ∧ 17 * S.card < I.card ∧ R S I)
    (hratio : ∀ I, I ⊆ H → ∀ S, R S I →
      ∀ S0 ∈ copyOrbit G S, ∀ J : Finset X, J.Nonempty → Disjoint S0 J →
        containmentProb G I (S0 ∪ J) / containmentProb G I S0 ≤ σ ^ J.card) :
    ∃ k : ℕ, ∃ m : ℕ → ℕ, ∃ T : ProbabilityTree X k,
      0 < k ∧ T.IsDisjoint ∧ T.HasCapacities m ∧ T.HasSpread (fun _ => σ) ∧
      (∀ i, i < k → 0 < m i) ∧
      (∀ i, i + 1 < k → 16 * m i ≤ m (i + 1)) ∧
…

Mentions: OAI.LeanBlast.SecondKahnKalai.copyOrbit, OAI.LeanBlast.SecondKahnKalai.containmentProb, OAI.LeanBlast.SecondKahnKalai.ProbabilityTree

theorem OAI.LeanBlast.SecondKahnKalai.exists_spread_orbit_tree line 302