CoveringRegularization.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Weighted-degree regularization

The initial family is the actual family of high weighted-degree subsets. Double counting bounds its cost. An edge surviving this deletion has bounded weighted degree at every one of its subsets. Grouping surviving edges by their intersection with B gives the extension estimates used for pair sampling and for residual tuples. No regularity property is assumed separately.

theorem OAI.TalagrandDiscreteConvexity.Covering.incidence_count line 24

Source documentation

Count incidences between edges and subsets of cardinality at most r.

theorem incidence_count (H : Family V) (r : ℕ)
    (hH : ∀ e ∈ H, e.card = r) :
    (∑ I ∈ Finset.univ.filter (fun I : Finset V => I.card ≤ r),
      (H.filter (fun e => I ⊆ e)).card) = H.card * 2 ^ r := by
…

Mentions: OAI.TalagrandDiscreteConvexity.Family

theorem OAI.TalagrandDiscreteConvexity.Covering.weightedDegree_nonneg line 51

theorem OAI.TalagrandDiscreteConvexity.Covering.weighted_incidence_count line 57

Source documentation

The weighted incidence identity is valid even at rho = 0.

theorem weighted_incidence_count (H : Family V) (rho : ℝ) (r : ℕ)
    (hH : ∀ e ∈ H, e.card = r) :
    (∑ I ∈ Finset.univ.filter (fun I : Finset V => I.card ≤ r),
      weightedDegree H rho r I * rho ^ I.card) =
      (2 : ℝ) ^ r * (H.card : ℝ) * rho ^ r := by
…

Mentions: OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.Covering.weightedDegree

theorem OAI.TalagrandDiscreteConvexity.Covering.initial_cost_le line 82
Source documentation
The initial generators cost at most their weighted-incidence budget divided by the high-degree threshold.
```
theorem initial_cost_le {H : Family V} {rho T : ℝ} {r : ℕ}
    (hρ : 0 ≤ rho) (hT : 0 < T) (hH : ∀ e ∈ H, e.card = r) :
    cost rho (initialFamily H rho r T) ≤
      T⁻¹ * (2 : ℝ) ^ r * (H.card : ℝ) * rho ^ r := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.cost, OAI.TalagrandDiscreteConvexity.Covering.initialFamily
theorem OAI.TalagrandDiscreteConvexity.Covering.regular_weightedDegree_le line 120
Source documentation
Actual survival implies the weighted-degree bound at every subset of the surviving edge.
```
theorem regular_weightedDegree_le {H : Family V} {rho T : ℝ} {r : ℕ}
    (hH : ∀ e ∈ H, e.card = r) {e I : Finset V}
    (he : e ∈ regularEdges H rho r T) (hIe : I ⊆ e) :
    weightedDegree H rho r I ≤ T := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.Covering.regularEdges, OAI.TalagrandDiscreteConvexity.Covering.weightedDegree
theorem OAI.TalagrandDiscreteConvexity.Covering.regular_intersection_sum_le line 132
Source documentation
Each nonempty intersection class contributes at most T, and the empty classes contribute zero.
```
private theorem regular_intersection_sum_le {H : Family V} {rho T : ℝ} {r : ℕ}
    (hρ : 0 ≤ rho) (hT : 0 ≤ T) (hH : ∀ e ∈ H, e.card = r)
    (B I : Finset V) :
    (∑ e ∈ (regularEdges H rho r T).filter (fun e => e ∩ B = I),
      rho ^ (e \ B).card) ≤ T := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.Covering.regularEdges

theorem OAI.TalagrandDiscreteConvexity.Covering.regular_extension_le_card line 176

Source documentation

Extension cost for actual regular edges, with the exact number of possible intersections with B.

theorem regular_extension_le_card {H : Family V} {rho T : ℝ} {r : ℕ}
    (hρ : 0 ≤ rho) (hT : 0 ≤ T) (hH : ∀ e ∈ H, e.card = r) (B : Finset V) :
    (∑ e ∈ regularEdges H rho r T, rho ^ (e \ B).card) ≤
      T * ((B.powerset.filter (fun I => I.card ≤ r)).card : ℝ) := by
…

Mentions: OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.Covering.regularEdges

theorem OAI.TalagrandDiscreteConvexity.Covering.regular_extension_le_choose line 199

Source documentation

The exact binomial extension bound from the covering lemma.

theorem regular_extension_le_choose {H : Family V} {rho T : ℝ} {r : ℕ}
    (hρ : 0 ≤ rho) (hT : 0 ≤ T) (hH : ∀ e ∈ H, e.card = r) (B : Finset V) :
    (∑ e ∈ regularEdges H rho r T, rho ^ (e \ B).card) ≤
      T * (∑ i ∈ Finset.range (r + 1), (Nat.choose B.card i : ℝ)) := by
…

Mentions: OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.Covering.regularEdges

theorem OAI.TalagrandDiscreteConvexity.Covering.regular_extension_le_pow line 209

Source documentation

The polynomial version used for extending a residual tuple prefix.

theorem regular_extension_le_pow {H : Family V} {rho T : ℝ} {r : ℕ}
    (hρ : 0 ≤ rho) (hT : 0 ≤ T) (hH : ∀ e ∈ H, e.card = r) (B : Finset V) :
    (∑ e ∈ regularEdges H rho r T, rho ^ (e \ B).card) ≤
      T * (1 + (B.card : ℝ)) ^ r := by
…

Mentions: OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.Covering.regularEdges

theorem OAI.TalagrandDiscreteConvexity.Covering.regular_extension_le_two_pow line 222

Source documentation

An r-element prefix gives the sharper factor 2^r, used for pairs.

theorem regular_extension_le_two_pow {H : Family V} {rho T : ℝ} {r : ℕ}
    (hρ : 0 ≤ rho) (hT : 0 ≤ T) (hH : ∀ e ∈ H, e.card = r)
    {B : Finset V} (hB : B.card = r) :
    (∑ e ∈ regularEdges H rho r T, rho ^ (e \ B).card) ≤ (2 : ℝ) ^ r * T := by
…

Mentions: OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.Covering.regularEdges