CoveringResidualTuples.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

The total weight of residual tuples

We bound the sum over injective edge tuples by the sum over all edge tuples. Splitting an unrestricted tuple into its first edge and its tail gives an exact weighted recurrence. The per-union extension bound then controls every step. No nonemptiness assumption on the edge family is needed.

def OAI.TalagrandDiscreteConvexity.Covering.allTupleUnion line 27
Source documentation
The union of an unrestricted ordered edge tuple.
```
def allTupleUnion {H : Family V} {t : ℕ} (f : Fin t → ↥H) : Finset V :=
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family
def OAI.TalagrandDiscreteConvexity.Covering.tupleWeight line 31
Source documentation
Weight of the union of an injective tuple.
```
def tupleWeight {H : Family V} {t : ℕ} (rho : ℝ) (f : EdgeTuple H t) : ℝ :=
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.Covering.EdgeTuple
def OAI.TalagrandDiscreteConvexity.Covering.tupleWeightSum line 34
def OAI.TalagrandDiscreteConvexity.Covering.allTupleWeightSum line 38
Source documentation
The larger sum in which repeated edges are allowed.
```
def allTupleWeightSum (H : Family V) (rho : ℝ) (t : ℕ) : ℝ :=
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family
theorem OAI.TalagrandDiscreteConvexity.Covering.tupleWeight_nonneg line 41
theorem OAI.TalagrandDiscreteConvexity.Covering.allTupleUnion_zero line 45
theorem OAI.TalagrandDiscreteConvexity.Covering.allTupleWeightSum_zero line 49
theorem OAI.TalagrandDiscreteConvexity.Covering.tupleWeightSum_zero line 54
theorem OAI.TalagrandDiscreteConvexity.Covering.allTupleUnion_card_le line 63
Source documentation
An unrestricted t-tuple of r-element edges uses at most r * t vertices.
```
theorem allTupleUnion_card_le {H : Family V} {r t : ℕ}
    (uniform : ∀ e ∈ H, (e : Finset V).card = r) (f : Fin t → ↥H) :
    (allTupleUnion f).card ≤ r * t := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.Covering.allTupleUnion
theorem OAI.TalagrandDiscreteConvexity.Covering.tupleUnion_card_le line 74
theorem OAI.TalagrandDiscreteConvexity.Covering.allTupleUnion_cons line 80
Source documentation
Splitting a tuple separates its old union from the newly chosen edge.
```
theorem allTupleUnion_cons {H : Family V} {t : ℕ}
    (e : ↥H) (f : Fin t → ↥H) :
    allTupleUnion (Fin.cons e f) = allTupleUnion f ∪ e.val := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.Covering.allTupleUnion
theorem OAI.TalagrandDiscreteConvexity.Covering.allTupleWeight_cons line 87
Source documentation
Union weight factors exactly into the prefix weight and its extension cost.
```
theorem allTupleWeight_cons {H : Family V} {t : ℕ} (rho : ℝ)
    (e : ↥H) (f : Fin t → ↥H) :
    rho ^ (allTupleUnion (Fin.cons e f)).card =
      rho ^ (allTupleUnion f).card * rho ^ (e.val \ allTupleUnion f).card := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.Covering.allTupleUnion
theorem OAI.TalagrandDiscreteConvexity.Covering.allTupleWeightSum_succ line 95
Source documentation
Exact recurrence for the unrestricted sum, obtained by reindexing with Fin.cons.
```
theorem allTupleWeightSum_succ (H : Family V) (rho : ℝ) (t : ℕ) :
    allTupleWeightSum H rho (t + 1) =
      ∑ f : Fin t → ↥H, rho ^ (allTupleUnion f).card *
        (∑ e ∈ H, rho ^ (e \ allTupleUnion f).card) := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.Covering.allTupleWeightSum, OAI.TalagrandDiscreteConvexity.Covering.allTupleUnion
theorem OAI.TalagrandDiscreteConvexity.Covering.tupleWeightSum_le_allTupleWeightSum line 118
Source documentation
Discarding the injectivity restriction increases the sum of nonnegative weights.
```
theorem tupleWeightSum_le_allTupleWeightSum (H : Family V) {rho : ℝ}
    (hrho : 0 ≤ rho) (t : ℕ) :
    tupleWeightSum H rho t ≤ allTupleWeightSum H rho t := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.Covering.tupleWeightSum, OAI.TalagrandDiscreteConvexity.Covering.allTupleWeightSum

theorem OAI.TalagrandDiscreteConvexity.Covering.allTupleWeightSum_succ_le line 135

Source documentation

The extension estimate yields the unrestricted recurrence up to a fixed length.

theorem allTupleWeightSum_succ_le (H : Family V) {rho T : ℝ} {r m t : ℕ}
    (hrho : 0 ≤ rho) (hT : 0 ≤ T)
    (uniform : ∀ e ∈ H, (e : Finset V).card = r)
    (extension : ∀ B : Finset V,
      (∑ e ∈ H, rho ^ (e \ B).card) ≤ T * (1 + (B.card : ℝ)) ^ r)
    (ht : t ≤ m) :
    allTupleWeightSum H rho (t + 1) ≤
      (T * (1 + ((r * m : ℕ) : ℝ)) ^ r) * allTupleWeightSum H rho t := by
…

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

theorem OAI.TalagrandDiscreteConvexity.Covering.allTupleWeightSum_le line 162

Source documentation

Iteration of the actual recurrence bounds every unrestricted sum up to m.

theorem allTupleWeightSum_le (H : Family V) {rho T : ℝ} {r m : ℕ}
    (hrho : 0 ≤ rho) (hT : 0 ≤ T)
    (uniform : ∀ e ∈ H, (e : Finset V).card = r)
    (extension : ∀ B : Finset V,
      (∑ e ∈ H, rho ^ (e \ B).card) ≤ T * (1 + (B.card : ℝ)) ^ r)
    (t : ℕ) (ht : t ≤ m) :
    allTupleWeightSum H rho t ≤ (T * (1 + ((r * m : ℕ) : ℝ)) ^ r) ^ t := by
…

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

theorem OAI.TalagrandDiscreteConvexity.Covering.tupleWeightSum_le line 187