TopologyChargeBound.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DilutedSpinGlass.PrescribedTree.branch_budget line 12
Source documentation
Exact leaf budget, counting vertices with multiplicity and not merely branching depth values. Unary grid levels consume no budget.
```
lemma branch_budget {n : ℕ} (S : PrescribedTree n) :
    branchingCount S (fun _ => True)+branchExcess S+1=leaves S := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.branchingCount, OAI.DilutedSpinGlass.PrescribedTree.branchExcess, OAI.DilutedSpinGlass.PrescribedTree.leaves
lemma OAI.DilutedSpinGlass.PrescribedTree.branchingDepths_card_le line 28
lemma OAI.DilutedSpinGlass.PrescribedTree.shiftedPrefixDepths_card_le line 37
lemma OAI.DilutedSpinGlass.PrescribedTree.chargeBound_le_pow line 45
theorem OAI.DilutedSpinGlass.PrescribedTree.shiftedCharge_relative_uniform line 66
Source documentation
A topology-only constant for the genuine relative signed-history cost. The grid size is absent. Its hypotheses are just leaf/depth counts, not a covariance estimate or any desired limiting conclusion.
```
theorem shiftedCharge_relative_uniform {L : ℕ} (hL : 0<L) (Q : Finset ℕ)
    (T S : PrescribedTree L) (k R : ℕ) (hQ : Q.card≤R)
    (hS : leaves S+k≤R) (hT : leaves T≤R)
    (a b : T.Leaf) (hab : a≠b) (η : ℝ) (hη : 0<η)
    (hr : BranchRegular T (grid L 0 L) η)
    (hb : branchingCount T (fun _ => True)=branchingCount T (· ∈ Q)+1) :
    shiftedCharge Q T S k /
      |partialKappa T (grid L 0 L) Finset.univ/partialKappa T (grid L 0 L) {b,a}| ≤
      (((2+(R:ℝ))*(R:ℝ))^k)/(min η 1)^R := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.leaves, OAI.DilutedSpinGlass.PrescribedTree.BranchRegular, OAI.DilutedSpinGlass.PrescribedTree.grid, OAI.DilutedSpinGlass.PrescribedTree.branchingCount, OAI.DilutedSpinGlass.PrescribedTree.shiftedCharge, OAI.DilutedSpinGlass.PrescribedTree.partialKappa