Predecessor.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

Maximizing predecessors

The predecessor is chosen by maximization over the actual finite powerset, including its empty member. The graph application uses distinct group-orbit copies and the actual containment probability, not labeled embeddings.

theorem OAI.LeanBlast.SecondKahnKalai.choose_le_exp_div_pow line 27
Source documentation
The standard real binomial upper bound, derived directly from the exponential series and the factorial upper bound on choose.
```
theorem choose_le_exp_div_pow (h r : ℕ) (hr : 0 < r) :
    (h.choose r : ℝ) ≤ (Real.exp 1 * (h : ℝ) / (r : ℝ)) ^ r := by
…
```
theorem OAI.LeanBlast.SecondKahnKalai.two_choose_div_le_predecessor_power line 47
theorem OAI.LeanBlast.SecondKahnKalai.two_choose_div_lt_one line 67

theorem OAI.LeanBlast.SecondKahnKalai.normalized_count_score_bound line 73

Source documentation

Arithmetic form of the expectation constraint and internal-copy count bound.

theorem normalized_count_score_bound {a m h r : ℕ} {q : ℝ}
    (hq : 0 < q) (hm : 0 < m) (ha : a ≤ h.choose r)
    (he : (1 / 2 : ℝ) ≤ (m : ℝ) * q ^ r) :
    ((a : ℝ) / (m : ℝ)) / (128 * q) ^ r ≤
      2 * (h.choose r : ℝ) / (128 : ℝ) ^ r := by
…

theorem OAI.LeanBlast.SecondKahnKalai.exists_powerset_max line 94
def OAI.LeanBlast.SecondKahnKalai.maximizingSubset line 100
Source documentation
A deterministic classical choice of a maximizer over all subsets of I. The empty set is included, so this definition also applies to empty I.
```
def maximizingSubset (I : Finset X) (score : Finset X → ℝ) : Finset X :=
…
```
theorem OAI.LeanBlast.SecondKahnKalai.maximizingSubset_subset line 103
theorem OAI.LeanBlast.SecondKahnKalai.le_maximizingSubset line 107
def OAI.LeanBlast.SecondKahnKalai.predecessorScore line 118
def OAI.LeanBlast.SecondKahnKalai.maximizingPredecessor line 122
Source documentation
The actual maximizing predecessor; the finite choice includes the empty set.
```
def maximizingPredecessor (I : Finset X) (σ : ℝ) : Finset X :=
…
```
theorem OAI.LeanBlast.SecondKahnKalai.maximizingPredecessor_subset line 125
theorem OAI.LeanBlast.SecondKahnKalai.predecessorScore_le_max line 129
theorem OAI.LeanBlast.SecondKahnKalai.predecessorScore_empty line 135
theorem OAI.LeanBlast.SecondKahnKalai.one_le_predecessorScore_max line 139
theorem OAI.LeanBlast.SecondKahnKalai.predecessorScore_eq_of_mem_copyOrbit line 143
theorem OAI.LeanBlast.SecondKahnKalai.predecessorScore_le_max_all line 152
Source documentation
A positive observation pulls back to an actual subset of I; zero-probability observations cannot exceed the empty set's score. Thus the chosen finite maximum controls every observed set, not only subsets of the original copy.
```
theorem predecessorScore_le_max_all (I U : Finset X) (σ : ℝ) :
    predecessorScore G I σ U ≤ predecessorScore G I σ (maximizingPredecessor G I σ) := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.predecessorScore, OAI.LeanBlast.SecondKahnKalai.maximizingPredecessor
theorem OAI.LeanBlast.SecondKahnKalai.predecessorScore_le_two_choose line 163
theorem OAI.LeanBlast.SecondKahnKalai.maximizingPredecessor_small line 175
Source documentation
The maximizing predecessor is less than one seventeenth of the current set. The only probabilistic input is the actual expectation constraint for its nonempty edge subsets.
```
theorem maximizingPredecessor_small (I : Finset X) (hI : I.Nonempty)
    {q : ℝ} (hq : 0 < q)
    (hE : ∀ S : Finset X, S ⊆ I → S.Nonempty →
      (1 / 2 : ℝ) ≤ (orbitCount G S : ℝ) * q ^ S.card) :
    17 * (maximizingPredecessor G I (128 * q)).card < I.card := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.orbitCount, OAI.LeanBlast.SecondKahnKalai.maximizingPredecessor
theorem OAI.LeanBlast.SecondKahnKalai.predecessor_copy_prob_pos line 190
theorem OAI.LeanBlast.SecondKahnKalai.predecessor_conditional_ratio_le line 195