CoveringNumericalBounds.lean`

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

def OAI.TalagrandDiscreteConvexity.Covering.NumericalBounds.m line 11
Source documentation
Number of distinct edges in a residual tuple.
```
def m (h : ℕ) : ℕ := 2 ^ (12 * h)
```
def OAI.TalagrandDiscreteConvexity.Covering.NumericalBounds.T line 14
Source documentation
Threshold for a large weighted degree.
```
def T (h : ℕ) : ℝ := 2 ^ (4 * h)
```
def OAI.TalagrandDiscreteConvexity.Covering.NumericalBounds.p line 17
Source documentation
Independent sampling probability for each ordered pair.
```
noncomputable def p (h : ℕ) : ℝ := (2 ^ (8 * h))⁻¹
```
def OAI.TalagrandDiscreteConvexity.Covering.NumericalBounds.A line 20
Source documentation
Exponent bounding one regular extension factor.
```
def A (r h : ℕ) : ℕ := 4 * h + 13 * r * h
```
theorem OAI.TalagrandDiscreteConvexity.Covering.NumericalBounds.m_pos line 22
theorem OAI.TalagrandDiscreteConvexity.Covering.NumericalBounds.T_pos line 26
theorem OAI.TalagrandDiscreteConvexity.Covering.NumericalBounds.T_nonneg line 30
theorem OAI.TalagrandDiscreteConvexity.Covering.NumericalBounds.p_pos line 32
theorem OAI.TalagrandDiscreteConvexity.Covering.NumericalBounds.p_nonneg line 36
theorem OAI.TalagrandDiscreteConvexity.Covering.NumericalBounds.p_le_one line 38
theorem OAI.TalagrandDiscreteConvexity.Covering.NumericalBounds.extension_base_le_pow line 43
Source documentation
The count of possible padded extensions has this dyadic upper bound.
```
theorem extension_base_le_pow (r h : ℕ) (hrh : r ≤ h) :
    1 + r * m h ≤ 2 ^ (13 * h) := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Covering.NumericalBounds.m
theorem OAI.TalagrandDiscreteConvexity.Covering.NumericalBounds.extension_factor_le_pow line 59
Source documentation
The extension factor from the weighted-degree estimate is at most the stated natural power of two.
```
theorem extension_factor_le_pow (r h : ℕ) (hrh : r ≤ h) :
    T h * (1 + (r : ℝ) * (m h : ℝ)) ^ r ≤ (2 : ℝ) ^ A r h := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Covering.NumericalBounds.T, OAI.TalagrandDiscreteConvexity.Covering.NumericalBounds.m, OAI.TalagrandDiscreteConvexity.Covering.NumericalBounds.A
theorem OAI.TalagrandDiscreteConvexity.Covering.NumericalBounds.exponent_budget_nat line 74
Source documentation
The quadratic polynomial exponent is dominated by the sampling budget.
```
theorem exponent_budget_nat (r h : ℕ) (hrh : r ≤ h) (hh : 64 ≤ h) :
    A r h + 1 ≤ 2 ^ (4 * h) := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Covering.NumericalBounds.A
theorem OAI.TalagrandDiscreteConvexity.Covering.NumericalBounds.p_mul_m line 104
Source documentation
The chosen pair probability times the tuple length is exactly the weighted-degree threshold.
```
theorem p_mul_m (h : ℕ) : p h * (m h : ℝ) = T h := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Covering.NumericalBounds.p, OAI.TalagrandDiscreteConvexity.Covering.NumericalBounds.m, OAI.TalagrandDiscreteConvexity.Covering.NumericalBounds.T
theorem OAI.TalagrandDiscreteConvexity.Covering.NumericalBounds.exponent_budget line 109
theorem OAI.TalagrandDiscreteConvexity.Covering.NumericalBounds.dyadic_residual_bound line 117
Source documentation
A dyadic growth factor is dominated by independent avoidance when each block has one additional unit of exponential sampling budget.
```
theorem dyadic_residual_bound (a n : ℕ) (prob : ℝ)
    (hprob : prob ≤ 1)
    (hbudget : (a : ℝ) + 1 ≤ prob * (n : ℝ)) :
    ((2 : ℝ) ^ a) ^ n * (1 - prob) ^ (n * n) ≤ ((2 : ℝ) ^ n)⁻¹ := by
…
```
theorem OAI.TalagrandDiscreteConvexity.Covering.NumericalBounds.residual_cost_le_inv_pow line 154
Source documentation
The actual residual tuple-growth factor times its exact avoidance probability is at most the reciprocal dyadic tuple-length power.
```
theorem residual_cost_le_inv_pow (r h : ℕ) (hrh : r ≤ h) (hh : 64 ≤ h) :
    (T h * (1 + (r : ℝ) * (m h : ℝ)) ^ r) ^ m h *
        (1 - p h) ^ (m h * m h) ≤ ((2 : ℝ) ^ m h)⁻¹ := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Covering.NumericalBounds.T, OAI.TalagrandDiscreteConvexity.Covering.NumericalBounds.m, OAI.TalagrandDiscreteConvexity.Covering.NumericalBounds.p
theorem OAI.TalagrandDiscreteConvexity.Covering.NumericalBounds.initial_cost_le line 172
Source documentation
The initial weighted-degree generators have the required numerical cost after inserting the assumed upper bound on the total edge mass.
```
theorem initial_cost_le (r h : ℕ) (hrh : r ≤ h) :
    (T h)⁻¹ * (2 : ℝ) ^ r * (2 : ℝ) ^ (h + 1) ≤
      2 * ((2 : ℝ) ^ (2 * h))⁻¹ := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Covering.NumericalBounds.T
theorem OAI.TalagrandDiscreteConvexity.Covering.NumericalBounds.pair_cost_le line 194
Source documentation
The sampled-pair numerical cost has the same bound as the initial cost.
```
theorem pair_cost_le (r h : ℕ) (hrh : r ≤ h) :
    p h * (2 : ℝ) ^ (h + 1) * (2 : ℝ) ^ r * T h ≤
      2 * ((2 : ℝ) ^ (2 * h))⁻¹ := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Covering.NumericalBounds.p, OAI.TalagrandDiscreteConvexity.Covering.NumericalBounds.T
theorem OAI.TalagrandDiscreteConvexity.Covering.NumericalBounds.h_le_m line 209
theorem OAI.TalagrandDiscreteConvexity.Covering.NumericalBounds.final_cost_le line 217
Source documentation
The sum of the two initial-scale costs and the residual dyadic cost is at most the final covering budget.
```
theorem final_cost_le (h : ℕ) (hh : 64 ≤ h) :
    4 * ((2 : ℝ) ^ (2 * h))⁻¹ + ((2 : ℝ) ^ m h)⁻¹ ≤
      3 * ((2 : ℝ) ^ h)⁻¹ := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Covering.NumericalBounds.m