StarBudget.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

def OAI.HyperbolicObstruction.SparsePattern.Pattern.branchCost line 18
Source documentation
Cost of the unconditioned entries of one star branch supported in A∪V.
```
def branchCost (U A V : Finset F) : ℤ :=
…
```
def OAI.HyperbolicObstruction.SparsePattern.Pattern.starExponent line 23
Source documentation
Exact critical exponent of a star-coordinate subset. Central coordinates are counted once, and outside coordinates separately in each branch.
```
def starExponent (U A : Finset F) (V : B → Finset F) : ℤ :=
…
```
lemma OAI.HyperbolicObstruction.SparsePattern.Pattern.branchCost_mono line 26
lemma OAI.HyperbolicObstruction.SparsePattern.Pattern.increment_eq line 38
lemma OAI.HyperbolicObstruction.SparsePattern.Pattern.starExponent_lower line 55
lemma OAI.HyperbolicObstruction.SparsePattern.Pattern.branchCost_empty line 65
lemma OAI.HyperbolicObstruction.SparsePattern.Pattern.starExponent_empty line 80

lemma OAI.HyperbolicObstruction.SparsePattern.Pattern.extension_margin line 96

Source documentation

Extension overlaps retain at least one full integer of critical margin.

lemma extension_margin {U : Finset F} {V : B → Finset F}
    (hd : ∀ j, Disjoint U (V j)) (ha : ∃ j, (V j).Nonempty)
    (gap : ∀ W, W.Nonempty → Disjoint U W → 1 ≤ P.exponent (U ∪ W) - P.exponent U) :
    1 ≤ ∑ j, ((V j).card - P.branchCost U U (V j)) := by
…

theorem OAI.HyperbolicObstruction.SparsePattern.Pattern.leaf_margin line 114

Source documentation

The leaf overlap margin, including the separate A=∅ case. The active assumption records that W is a union of supports of shared entries, rather than an arbitrary nonempty collection of coordinates.

theorem leaf_margin {U A : Finset F} {V : B → Finset F} {e : F}
    (hA : A ⊆ U) (hd : ∀ j, Disjoint U (V j))
    (budget : ∀ W : Finset F, (min 2 W.card : ℕ) ≤ P.exponent W)
    (supports : ∀ r, 3 ≤ (P.support r).card)
    (gap : ∀ W, W.Nonempty → Disjoint U W → 1 ≤ P.exponent (U ∪ W) - P.exponent U)
    (active : A = ∅ → (∃ j, (V j).Nonempty) ∧ ∀ j, (V j).Nonempty → 3 ≤ (V j).card) :
    1 ≤ P.starExponent U A V - ∑ j, if e ∈ V j then (1 : ℤ) else 0 := by
…