Thresholds.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

Continuity and attainment of the graph thresholds

Every probability is a literal finite sum of Bernoulli products. The admissible parameter sets are closed subsets of [0,1]; endpoint feasibility therefore makes their infima admissible. No minimizer is postulated.

theorem OAI.LeanBlast.SecondKahnKalai.continuous_bernoulliWeight line 22
theorem OAI.LeanBlast.SecondKahnKalai.continuous_bernoulliExpectation line 29
theorem OAI.LeanBlast.SecondKahnKalai.continuous_bernoulliProbability line 36
theorem OAI.LeanBlast.SecondKahnKalai.continuous_expectedCopies line 46
theorem OAI.LeanBlast.SecondKahnKalai.continuous_containmentProbability line 51
theorem OAI.LeanBlast.SecondKahnKalai.isClosed_criticalFeasible line 56
theorem OAI.LeanBlast.SecondKahnKalai.isClosed_expectationFeasible line 61
theorem OAI.LeanBlast.SecondKahnKalai.criticalThreshold_attained_of_one line 74
Source documentation
Endpoint feasibility is enough to ensure that the containment infimum is attained; its probability need not be assumed monotone for this step.
```
theorem criticalThreshold_attained_of_one {V : Type*} (n : ℕ) (H : SimpleGraph V)
    (hone : (1 / 2 : ℝ) ≤ containmentProbability n 1 H) :
    criticalThreshold n H ∈ Set.Icc 0 1 ∧
      (1 / 2 : ℝ) ≤ containmentProbability n (criticalThreshold n H) H := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.containmentProbability, OAI.LeanBlast.SecondKahnKalai.criticalThreshold
theorem OAI.LeanBlast.SecondKahnKalai.expectationThreshold_attained_of_one line 90
Source documentation
All subgraph constraints hold at the expectation infimum. Arbitrary intersections of closed constraints suffice, so no enumeration is assumed.
```
theorem expectationThreshold_attained_of_one {V : Type*} (n : ℕ) (H : SimpleGraph V)
    (hone : ∀ F : H.Subgraph, (1 / 2 : ℝ) ≤ expectedCopies n 1 F.coe) :
    expectationThreshold n H ∈ Set.Icc 0 1 ∧
      ∀ F : H.Subgraph, (1 / 2 : ℝ) ≤
        expectedCopies n (expectationThreshold n H) F.coe := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.expectedCopies, OAI.LeanBlast.SecondKahnKalai.expectationThreshold
theorem OAI.LeanBlast.SecondKahnKalai.criticalThreshold_le_of_probability line 107
Source documentation
Any admissible parameter gives an upper bound on the actual critical threshold.
```
theorem criticalThreshold_le_of_probability {V : Type*} (n : ℕ) (H : SimpleGraph V)
    {p : ℝ} (hp : p ∈ Set.Icc 0 1)
    (hprob : (1 / 2 : ℝ) ≤ containmentProbability n p H) :
    criticalThreshold n H ≤ p := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.containmentProbability, OAI.LeanBlast.SecondKahnKalai.criticalThreshold
theorem OAI.LeanBlast.SecondKahnKalai.expectationThreshold_pos_of_zero_constraint line 120
Source documentation
A subgraph whose expectation vanishes at zero forces strict positivity of the attained expectation threshold.
```
theorem expectationThreshold_pos_of_zero_constraint {V : Type*}
    (n : ℕ) (H : SimpleGraph V)
    (hone : ∀ F : H.Subgraph, (1 / 2 : ℝ) ≤ expectedCopies n 1 F.coe)
    (F : H.Subgraph) (hzero : expectedCopies n 0 F.coe = 0) :
    0 < expectationThreshold n H := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.expectedCopies, OAI.LeanBlast.SecondKahnKalai.expectationThreshold
theorem OAI.LeanBlast.SecondKahnKalai.expectationFeasible_one line 133
theorem OAI.LeanBlast.SecondKahnKalai.criticalThreshold_attained line 141

theorem OAI.LeanBlast.SecondKahnKalai.expectationThreshold_attained line 150

Source documentation

Every actual subgraph expectation constraint holds at p_E.

theorem expectationThreshold_attained {V : Type*} [Fintype V]
    (n : ℕ) (H : SimpleGraph V) (hcard : Fintype.card V ≤ n) :
    expectationThreshold n H ∈ Set.Icc 0 1 ∧
      ∀ F : H.Subgraph, (1 / 2 : ℝ) ≤
        expectedCopies n (expectationThreshold n H) F.coe :=
…

Mentions: OAI.LeanBlast.SecondKahnKalai.expectationThreshold, OAI.LeanBlast.SecondKahnKalai.expectedCopies

theorem OAI.LeanBlast.SecondKahnKalai.criticalThreshold_mem_unitInterval line 157
theorem OAI.LeanBlast.SecondKahnKalai.expectationThreshold_mem_unitInterval line 162
theorem OAI.LeanBlast.SecondKahnKalai.expectationThreshold_pos line 169
Source documentation
Strict positivity follows from the constraint for an actual one-edge subgraph, whose expected number of copies at parameter zero vanishes.
```
theorem expectationThreshold_pos {V : Type*} [Fintype V]
    (n : ℕ) (H : SimpleGraph V) (hcard : Fintype.card V ≤ n)
    (hedge : 1 ≤ edgeCount H) : 0 < expectationThreshold n H := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.edgeCount, OAI.LeanBlast.SecondKahnKalai.expectationThreshold
theorem OAI.LeanBlast.SecondKahnKalai.expectationThreshold_constraint_self line 190