TreePotential.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

The bad-node potential for simultaneous tree reduction

All nodes in a reduction use the same random set. The expectation argument uses an outside-coordinate change of measure, rather than independence of node outcomes.

def OAI.LeanBlast.SecondKahnKalai.nodePotential line 29
Source documentation
One step of the actual recursive bad-node potential.
```
def nodePotential {B : Type*} [Fintype B] (m : ℕ) (failure : ℝ)
    (target childPotential : B → ℝ) : ℝ :=
…
```
theorem OAI.LeanBlast.SecondKahnKalai.nodePotential_nonneg line 33

theorem OAI.LeanBlast.SecondKahnKalai.one_lt_nodePotential_of_bad line 42

Source documentation

A failed good-mass threshold forces the recursively defined potential above one. Children with zero target mass require no special treatment.

theorem one_lt_nodePotential_of_bad {B : Type*} [Fintype B]
    (m : ℕ) (failure : ℝ) (target childPotential : B → ℝ) (good : B → Prop)
    (ht : ∀ b, 0 ≤ target b) (hc : ∀ b, 0 ≤ childPotential b)
    (hmass : failure + ∑ b, target b = 1)
    (hchild : ∀ b, ¬good b → 1 < childPotential b)
    (hbad : (∑ b, if good b then target b else 0) < 1 - Real.exp (-(m : ℝ))) :
    1 < nodePotential m failure target childPotential := by
…

Mentions: OAI.LeanBlast.SecondKahnKalai.nodePotential

theorem OAI.LeanBlast.SecondKahnKalai.bernoulliExpectation_nodePotential line 68

theorem OAI.LeanBlast.SecondKahnKalai.bernoulliExpectation_nodePotential_le line 85

Source documentation

The expectation recursion uses one change-of-measure estimate per child; it does not factor a product of dependent random variables.

theorem bernoulliExpectation_nodePotential_le {X B : Type*} [Fintype X] [DecidableEq X]
    [Fintype B] (p : ℝ) (m : ℕ) (ν : FiniteLaw B) (failure : Finset X → ℝ)
    (target childPotential : B → Finset X → ℝ)
    (hfailure : bernoulliExpectation p failure ≤ Real.exp (-9 * (m : ℝ)))
    (hchild : ∀ b,
      bernoulliExpectation p (fun W => target b W * childPotential b W) ≤
        Real.exp (11 * (m : ℝ)) * ν.weight b * bernoulliExpectation p (childPotential b)) :
    bernoulliExpectation p (fun W => nodePotential m (failure W)
      (fun b => target b W) (fun b => childPotential b W)) ≤
      Real.exp (-8 * (m : ℝ)) + Real.exp (12 * (m : ℝ)) *
        ν.expectation (fun b => bernoulliExpectation p (childPotential b)) := by
…

Mentions: OAI.LeanBlast.SecondKahnKalai.FiniteLaw, OAI.LeanBlast.SecondKahnKalai.bernoulliExpectation, OAI.LeanBlast.SecondKahnKalai.nodePotential

def OAI.LeanBlast.SecondKahnKalai.potentialEnvelope line 123

Source documentation

Deterministic envelope obtained by iterating the expectation recursion.

def potentialEnvelope : ℕ → (ℕ → ℕ) → ℝ
  | 0, _ => 0
  | d + 1, m => Real.exp (-8 * (m 0 : ℝ)) + Real.exp (12 * (m 0 : ℝ)) *
      potentialEnvelope d (fun j => m (j + 1))

theorem OAI.LeanBlast.SecondKahnKalai.potentialEnvelope_eq_sum line 128
def OAI.LeanBlast.SecondKahnKalai.treePotential line 150
theorem OAI.LeanBlast.SecondKahnKalai.treePotential_nonneg line 161
theorem OAI.LeanBlast.SecondKahnKalai.one_lt_treePotential_of_not_good line 172
theorem OAI.LeanBlast.SecondKahnKalai.treePotential_dependsOnlyOn line 190
Source documentation
The potential only inspects the labels belonging to the fixed subtree.
```
theorem treePotential_dependsOnlyOn (p : ℝ) (m : ℕ → ℕ) {d : ℕ}
    (T : ProbabilityTree X d) : DependsOnlyOn T.support (fun W => treePotential p m W T) := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.ProbabilityTree, OAI.LeanBlast.SecondKahnKalai.DependsOnlyOn, OAI.LeanBlast.SecondKahnKalai.treePotential
theorem OAI.LeanBlast.SecondKahnKalai.child_treePotential_dependsOutside line 213
Source documentation
Path disjointness makes a descendant potential insensitive to its incoming label; this is the locality needed by the change of measure.
```
theorem child_treePotential_dependsOutside {d : ℕ} {B : Type} [Fintype B]
    (ν : FiniteLaw B) (hν : ν.IsPositive) (A : B → Finset X)
    (child : B → ProbabilityTree X d)
    (hdis : (ProbabilityTree.node B ν hν A child).IsDisjoint)
    (p : ℝ) (m : ℕ → ℕ) (b : B) :
    DependsOutside (A b) (fun W => treePotential p m W (child b)) :=
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.FiniteLaw, OAI.LeanBlast.SecondKahnKalai.ProbabilityTree, OAI.LeanBlast.SecondKahnKalai.DependsOutside, OAI.LeanBlast.SecondKahnKalai.treePotential
theorem OAI.LeanBlast.SecondKahnKalai.bad_probability_le_expected_treePotential line 221
theorem OAI.LeanBlast.SecondKahnKalai.localFailureMass_eq_probability line 230
theorem OAI.LeanBlast.SecondKahnKalai.successfulTargetMass_le_cutoff line 239
theorem OAI.LeanBlast.SecondKahnKalai.treePotential_expectation_node_le line 256
theorem OAI.LeanBlast.SecondKahnKalai.treePotential_expectation_le line 279

theorem OAI.LeanBlast.SecondKahnKalai.root_bad_probability_lt_one_quarter line 313

Source documentation

One simultaneous reduction fails with probability strictly below one quarter under the geometric level-capacity assumptions.

theorem root_bad_probability_lt_one_quarter {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (m : ℕ → ℕ) (a : ℕ → ℝ) {d : ℕ} (T : ProbabilityTree X d)
    (hdis : T.IsDisjoint) (hcap : T.HasCapacities m) (hspread : T.HasSpread a)
    (hm : ∀ j, j < d → 1 ≤ m j) (ha : ∀ j, j < d → 0 ≤ a j)
    (hsmall : ∀ j, j < d → a j / p ≤ Real.exp (-50))
    (hgrowth : ∀ j, j + 1 < d → 16 * m j ≤ m (j + 1)) :
    bernoulliProbability p (fun W => ¬Good p m W T) < 1 / 4 := by
…

Mentions: OAI.LeanBlast.SecondKahnKalai.ProbabilityTree, OAI.LeanBlast.SecondKahnKalai.bernoulliProbability, OAI.LeanBlast.SecondKahnKalai.Good

theorem OAI.LeanBlast.SecondKahnKalai.reduction_good_probability_ge line 325